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

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

doGlueKanOp Source #

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 Source #

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.