Agda.TypeChecking.Primitive.Cubical.Id

Implementation of the primitives relating to Cubical identity types.

General elimination form

primIdElim' :: TCM PrimitiveImpl

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

Introduction form for the cubical identity types.

Projection maps (primarily used internally)

primIdFace' :: TCM PrimitiveImpl

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

Extract the underlying path from an inhabitant of the cubical identity types.

Kan operations

doIdKanOp

Arguments

:: KanOperation

Are we composing or transporting?

-> FamilyOrNot (Arg Term)

Level argument

-> FamilyOrNot (Arg Term, Arg Term, Arg Term)

Domain, left and right endpoints of the identity type

-> ReduceM (Maybe (Reduced t Term))