| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Primitive.Cubical.HCompU
Synopsis
- doHCompUKanOp :: forall m. PureTCM m => KanOperation -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term)
- prim_glueU' :: TCM PrimitiveImpl
- prim_unglueU' :: TCM PrimitiveImpl
Documentation
doHCompUKanOp :: forall m. PureTCM m => KanOperation -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term) Source #
Perform the Kan operations for an hcomp {A = Type} {φ} u u0 type.
prim_glueU' :: TCM PrimitiveImpl Source #
The implementation of prim_glueU, the introduction form for
hcomp types.
prim_unglueU' :: TCM PrimitiveImpl Source #
The implementation of prim_unglueU, the elimination form for
hcomp types.