| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Primitive.Cubical.Glue
Synopsis
- mkGComp :: forall (m :: Type -> Type). HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
- doGlueKanOp :: PureTCM m => KanOperation -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term)
- primGlue' :: TCM PrimitiveImpl
- prim_glue' :: TCM PrimitiveImpl
- prim_unglue' :: TCM PrimitiveImpl
Documentation
mkGComp :: forall (m :: Type -> Type). HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term) Source #
Define a "ghcomp" version of gcomp. Normal comp looks like:
comp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u ] (forward A 0 u0)
So for "gcomp" we compute:
gcomp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u, ~ phi -> forward A 0 u0 ] (forward A 0 u0)
The point of this is that gcomp does not produce any empty systems (if phi = 0 it will reduce to "forward A 0 u".
Arguments
| :: PureTCM m | |
| => KanOperation | Are we composing or transporting? |
| -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) | The data of the Glue operation: The levels of |
| -> TermPosition | Are we computing a plain hcomp/transp or are we computing under
|
| -> m (Maybe Term) |
Perform the Kan operations for a Glue φ A (T , e) type.
prim_glue' :: TCM PrimitiveImpl Source #
The implementation of prim_glue, the introduction form for Glue
types.
prim_unglue' :: TCM PrimitiveImpl Source #
The implementation of prim_unglue, the elimination form for
Glue types.