ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Primitive.Cubical

Synopsis

value debugClause
value doPathPKanOp
value doPiKanOp
value expS
value expTelescope
value fromCType
value fromLType
value hcomp
value lTypeLevel
value mkComp
value mkCompLazy
value pathTelescope
value pathTelescope'
value primComp
value primFaceForall'
value primHComp'
value primPOr
value primPartial'
value primPartialP'
value primSubOut'
value primTrans'
value primTransHComp
value redReturnNoSimpl
value toCType
value toLType
value trFillPathPTel'
value trFillPathTel'
value trFillTel
value trFillTel'
value transpPathPTel'
value transpPathTel'
value transpSys
value transpSysTel'
value transpTel
value transpTel'
value tryTranspError
data CType
type LM
data LType
data TranspError

PackageAgda-2.8.0.2
Exports40
LanguageHaskell2010
LicenceMIT
SourceCubical.hs

valuedebugClause :: String -> Clause -> TCM ()

valuedoPathPKanOp

:: KanOperation
-> FamilyOrNot (Arg Term)
-> FamilyOrNot (Arg Term, Arg Term, Arg Term)
-> ReduceM (Reduced MaybeReducedArgs Term)

Source#

Compute Kan operations in a type of dependent paths.

valuedoPiKanOp

:: KanOperation
Are we composing or transporting?
-> ArgName
Name of the binder
-> FamilyOrNot (Dom Type, Abs Type)
The domain and codomain of the Pi type.
-> ReduceM (Maybe Term)

Source#

Implementation of Kan operations for Pi types. The implementation of transp and hcomp for Pi types has many commonalities, so most of it is shared between the two cases.

valueexpS :: Nat -> Substitution

Source#

Γ, Δ^I, i : I |- expS |Δ| : Γ, Δ

valueexpTelescope :: Type -> Telescope -> Telescope

valuefromCType :: CType -> Type

valuefromLType :: LType -> Type

valuehcomp

:: (HasBuiltins m, MonadError TCErr m, MonadReduce m, MonadPretty m)
=> NamesT m Type
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
-> NamesT m Term

valuelTypeLevel :: LType -> Level

valuemkComp

:: HasBuiltins m
=> String
-> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)

Source#

Construct a helper for CCHM composition, with a string indicating what function uses it.

valuemkCompLazy

:: HasBuiltins m
=> String
-> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)

Source#

Construct an application of buitlinComp. Use instead of mkComp if reducing directly to hcomp + transport would be problematic.

valuepathTelescope

:: (PureTCM m, MonadError TCErr m)
=> Telescope
Δ
-> [Arg Term]
lhs : Δ
-> [Arg Term]
rhs : Δ
-> m Telescope

valuepathTelescope'

:: (PureTCM m, MonadError (Closure Type) m)
=> Telescope
Δ
-> [Arg Term]
lhs : Δ
-> [Arg Term]
rhs : Δ
-> m Telescope

valueprimComp :: TCM PrimitiveImpl

Source#

CCHM primComp is implemented in terms of hcomp and transport. The definition of it comes from mkComp.

valueprimFaceForall' :: TCM PrimitiveImpl

valueprimHComp' :: TCM PrimitiveImpl

valueprimPOr :: TCM PrimitiveImpl

valueprimPartial' :: TCM PrimitiveImpl

valueprimPartialP' :: TCM PrimitiveImpl

valueprimSubOut' :: TCM PrimitiveImpl

valueprimTrans' :: TCM PrimitiveImpl

valueprimTransHComp

:: Command
-> [Arg Term]
-> Int
-> ReduceM (Reduced MaybeReducedArgs Term)

valueredReturnNoSimpl :: a -> ReduceM (Reduced a' a)

valuetoCType :: MonadReduce m => Type -> m (Maybe CType)

valuetoLType :: MonadReduce m => Type -> m (Maybe LType)

valuetrFillPathPTel'

:: NamesT TCM (Abs (Abs Telescope))
j.i.Δ const on φ
-> [NamesT TCM Term]
x : (i : I) → Δ[0,i] const on φ
-> [NamesT TCM Term]
y : (i : I) → Δ[1,i] const on φ
-> NamesT TCM Term
φ
-> [NamesT TCM Term]
p : Path ( j -> Δ[j,0]) (x 0) (y 0)
-> NamesT TCM Term
r
-> NamesT TCM [Arg Term]

valuetrFillPathTel'

:: NamesT TCM (Abs Telescope)
i.Δ const on φ
-> [NamesT TCM Term]
x : (i : I) → Δ[i] const on φ
-> [NamesT TCM Term]
y : (i : I) → Δ[i] const on φ
-> NamesT TCM Term
φ
-> [NamesT TCM Term]
p : Path (Δ[0]) (x 0) (y 0)
-> NamesT TCM Term
r
-> NamesT TCM [Arg Term]

valuetrFillTel

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

Source#

Like transpTel but performing a transpFill.

valuetrFillTel'

:: (PureTCM m, MonadError TCErr m)
=> Bool
-> Abs Telescope
-> Term
-> Args
-> Term
-> ExceptT (Closure (Abs Type)) m Args

valuetranspPathPTel'

:: NamesT TCM (Abs (Abs Telescope))
j.i.Δ const on φ
-> [NamesT TCM Term]
x : (i : I) → Δ[0,i] const on φ
-> [NamesT TCM Term]
y : (i : I) → Δ[1,i] const on φ
-> NamesT TCM Term
φ
-> [NamesT TCM Term]
p : PathP (λ j → Δ[j,0]) (x 0) (y 0)
-> NamesT TCM [Arg Term]

valuetranspPathTel'

:: NamesT TCM (Abs Telescope)
i.Δ const on φ
-> [NamesT TCM Term]
x : (i : I) → Δ[i] const on φ
-> [NamesT TCM Term]
y : (i : I) → Δ[i] const on φ
-> NamesT TCM Term
φ
-> [NamesT TCM Term]
p : Path (Δ[0]) (x 0) (y 0)
-> NamesT TCM [Arg Term]

valuetranspSys

:: (HasBuiltins m, MonadError TCErr m, MonadReduce m)
=> NamesT m (Abs Type)
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term

valuetranspSysTel'

:: (PureTCM m, MonadError TCErr m)
=> Bool
-> Abs Telescope
-> [(Term, Abs [Term])]
-> Term
-> Args
-> ExceptT (Closure (Abs Type)) m Args

valuetranspTel

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

Source#

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.

valuetranspTel'

:: (PureTCM m, MonadError TCErr m)
=> Bool
-> Abs Telescope
-> Term
-> Args
-> ExceptT (Closure (Abs Type)) m Args

valuetryTranspError :: TCM a -> TCM (Either (Closure (Abs Type)) a)

datadata CType

Source#

A Type that either has sort Type l or is a closed definition. Such a type supports some version of transp. In particular we want to allow the Interval as a ClosedType.

Constructors

ClosedType Sort QName
LType LType

Instances5Eq, Show, Pretty, Subst, SubstArg

Eq CTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
Show CTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
Pretty CTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
Subst CTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
type SubstArg CType = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical

typetype LM (m :: Type -> Type) a = NamesT (ExceptT (Closure (Abs Type)) m) a

datadata LType

Source#

A Type with sort Type l Such a type supports both hcomp and transp.

Constructors

LEl Level Term

Instances4Eq, Show, Subst, SubstArg

Eq LTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
Show LTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
Subst LTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
type SubstArg LType = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical

datadata TranspError

Constructors

CannotTransp
- errorType :: Closure (Abs Type)

Instances2Show, Exception

Show TranspErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical
Exception TranspErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Cubical

module Agda.TypeChecking.Primitive.Cubical.Base

module Agda.TypeChecking.Primitive.Cubical.Glue

module Agda.TypeChecking.Primitive.Cubical.HCompU