| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Primitive.Cubical.Id
Description
Implementation of the primitives relating to Cubical identity types.
Synopsis
- primIdElim' :: TCM PrimitiveImpl
- primConId' :: TCM PrimitiveImpl
- primIdFace' :: TCM PrimitiveImpl
- primIdPath' :: TCM PrimitiveImpl
- doIdKanOp :: KanOperation -> FamilyOrNot (Arg Term) -> FamilyOrNot (Arg Term, Arg Term, Arg Term) -> ReduceM (Maybe (Reduced t Term))
General elimination form
primIdElim' :: TCM PrimitiveImpl Source #
Primitive elimination rule for the cubical identity types. Unlike
J, idElim makes explicit the structure of Swan's identity types as
being pairs of a cofibration and a path. Moreover, it records that
the path is definitionally refl under that cofibration.
Introduction form
primConId' :: TCM PrimitiveImpl Source #
Introduction form for the cubical identity types.
Projection maps (primarily used internally)
primIdFace' :: TCM PrimitiveImpl Source #
Extract the underlying cofibration from an inhabitant of the cubical identity types.
TODO (Amy, 2022-08-17): Projecting a cofibration from a Kan type violates the cubical phase distinction.
primIdPath' :: TCM PrimitiveImpl Source #
Extract the underlying path from an inhabitant of the cubical identity types.