Perform the Kan operations for an hcomp {A = Type} {φ} u u0 type.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Primitive.Cubical.HCompU
Synopsis
- value doHCompUKanOp
- value prim_glueU'
- value prim_unglueU'
- PackageAgda-2.8.0.2
- 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.