Agda-2.6.4.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Primitive.Cubical

Synopsis

Documentation

primComp :: TCM PrimitiveImpl Source #

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

mkComp :: 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 #

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

mkCompLazy :: 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 #

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

doPiKanOp Source #

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

Compute Kan operations in a type of dependent paths.

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

transpTel :: 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.

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

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

type LM (m :: Type -> Type) a = NamesT (ExceptT (Closure (Abs Type)) m) a Source #

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

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

Like transpTel but performing a transpFill.

transpPathPTel' Source #

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

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

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

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] 

expS :: Nat -> Substitution Source #

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

data LType Source #

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

Constructors

LEl Level Term 

Instances

Instances details
Subst LType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg LType 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Show LType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> LType -> ShowS #

show :: LType -> String #

showList :: [LType] -> ShowS #

Eq LType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

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

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

type SubstArg LType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

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

Instances

Instances details
Pretty CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Subst CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg CType 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Show CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> CType -> ShowS #

show :: CType -> String #

showList :: [CType] -> ShowS #

Eq CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

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

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

type SubstArg CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

transpSys :: forall (m :: Type -> Type). (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 Source #