Agda.TypeChecking.Primitive.Cubical

Documentation

data CType

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

Instances

Subst CType

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg CType

Methods

applySubst :: Substitution' (SubstArg CType) -> CType -> CType

Pretty CType

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

pretty :: CType -> Doc

prettyPrec :: Int -> CType -> Doc

prettyList :: [CType] -> Doc

Show CType

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> CType -> ShowS

show :: CType -> String

showList :: [CType] -> ShowS

Eq CType

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

(==) :: CType -> CType -> Bool

(/=) :: CType -> CType -> Bool

type SubstArg CType

Defined in Agda.TypeChecking.Primitive.Cubical

type SubstArg CType = Term

data LType

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

Constructors

LEl Level Term

Instances

Subst LType

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg LType

Methods

applySubst :: Substitution' (SubstArg LType) -> LType -> LType

Show LType

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> LType -> ShowS

show :: LType -> String

showList :: [LType] -> ShowS

Eq LType

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

(==) :: LType -> LType -> Bool

(/=) :: LType -> LType -> Bool

type SubstArg LType

Defined in Agda.TypeChecking.Primitive.Cubical

type SubstArg LType = Term

data TranspError

Constructors

CannotTransp

Fields

• errorType :: Closure (Abs Type)

Instances

Exception TranspError

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

toException :: TranspError -> SomeException

fromException :: SomeException -> Maybe TranspError

displayException :: TranspError -> String

Show TranspError

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> TranspError -> ShowS

show :: TranspError -> String

showList :: [TranspError] -> ShowS

type LM m a = NamesT (ExceptT (Closure (Abs Type)) m) a

primPOr :: TCM PrimitiveImpl

primPartial' :: TCM PrimitiveImpl

primPartialP' :: TCM PrimitiveImpl

primSubOut' :: TCM PrimitiveImpl

primTrans' :: TCM PrimitiveImpl

primHComp' :: TCM PrimitiveImpl

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

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

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

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

doPiKanOp

Arguments

:: 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)

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.

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

Compute Kan operations in a type of dependent paths.

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

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

primComp :: TCM PrimitiveImpl

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

primFaceForall' :: TCM PrimitiveImpl

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.

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

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

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

Like transpTel but performing a transpFill.

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

pathTelescope :: forall m. (PureTCM m, MonadError TCErr m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope

pathTelescope' :: forall m. (PureTCM m, MonadError (Closure Type) m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope

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

transpPathPTel'

Arguments

:: 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]

transpPathTel'

Arguments

:: 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]

trFillPathTel'

Arguments

:: 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]

trFillPathPTel'

Arguments

:: 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]

expTelescope :: Type -> Telescope -> Telescope

expS :: Nat -> Substitution

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

fromLType :: LType -> Type

lTypeLevel :: LType -> Level

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

fromCType :: CType -> Type

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

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

transpSys :: (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

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

module Agda.TypeChecking.Primitive.Cubical.Id

module Agda.TypeChecking.Primitive.Cubical.Base

module Agda.TypeChecking.Primitive.Cubical.Glue

module Agda.TypeChecking.Primitive.Cubical.HCompU