Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Primitive.Cubical.HCompU

Synopsis

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.