Perform the Kan operations for an hcomp {A = Type} {φ} u u0 type.
ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Primitive.Cubical.HCompU
- 3 values
- PackageAgda-2.7.0.1
- Exports3
- LanguageHaskell2010
- LicenceMIT
- SourceHCompU.hs
The implementation of prim_glueU, the introduction form for
hcomp types.
The implementation of prim_unglueU, the elimination form for
hcomp types.