Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Primitive.Cubical.HCompU

Synopsis

- doHCompUKanOp :: 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 :: 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.