Agda.TypeChecking.Primitive.Cubical

Documentation

transpTel :: Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) TCM Args

Tries to primTransp a whole telescope of arguments, following the rule for Σ types. If a type in the telescope does not support transp, transpTel throws it as an exception.

trFillTel :: Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) TCM Args

Like transpTel but performing a transpFill.