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.
ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Primitive.Cubical.Id
Implementation of the primitives relating to Cubical identity types.
- 5 values
- PackageAgda-2.7.0.1
- Exports5
- LanguageHaskell2010
- LicenceMIT
- SourceId.hs
General elimination form
1 declarationIntroduction form
1 declarationIntroduction form for the cubical identity types.
Projection maps (primarily used internally)
2 declarationsExtract 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.
Extract the underlying path from an inhabitant of the cubical identity types.