Agda.TypeChecking.Primitive.Cubical.Glue

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)

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".

doGlueKanOp

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 A and T, A itself, the extent of T, T itself, and the family of equivalences.

-> TermPosition

Are we computing a plain hcomp/transp or are we computing under unglue?

-> m (Maybe Term)

Perform the Kan operations for a Glue φ A (T , e) type.

primGlue' :: TCM PrimitiveImpl

prim_glue' :: TCM PrimitiveImpl

The implementation of prim_glue, the introduction form for Glue types.

prim_unglue' :: TCM PrimitiveImpl

The implementation of prim_unglue, the elimination form for Glue types.