Agda.TypeChecking.Primitive.Cubical.Base

Implementations of the basic primitives of Cubical Agda: The interval and its operations.

Documentation

requireCubical

Arguments

:: Cubical

Which variant of Cubical Agda is required?

-> String

Why, exactly, do we need Cubical to be enabled?

-> TCM ()

Checks that the correct variant of Cubical Agda is activated. Note that --erased-cubical "counts as" --cubical in erased contexts.

primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type

Our good friend the interval type.

primIMin' :: TCM PrimitiveImpl

Implements both the min connection and conjunction on the cofibration classifier.

primIMax' :: TCM PrimitiveImpl

Implements both the max connection and disjunction on the cofibration classifier.

primDepIMin' :: TCM PrimitiveImpl

primDepIMin expresses that cofibrations are closed under Σ. Thus, it serves as a dependent version of primIMin (which, recall, implements _∧_). This is required for the construction of the Kan operations in Id.

primINeg' :: TCM PrimitiveImpl

Negation on the interval. Negation satisfies De Morgan's laws, and their implementation is handled here.

imax :: HasBuiltins m => m Term -> m Term -> m Term

A helper for evaluating max on the interval in TCM&co.

imin :: HasBuiltins m => m Term -> m Term -> m Term

A helper for evaluating min on the interval in TCM&co.

ineg :: HasBuiltins m => m Term -> m Term

A helper for evaluating neg on the interval in TCM&co.

data Command

Constructors

DoTransp

DoHComp

Instances

Show Command

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

showsPrec :: Int -> Command -> ShowS

show :: Command -> String

showList :: [Command] -> ShowS

Eq Command

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

(==) :: Command -> Command -> Bool

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

data KanOperation

Our Kan operations are transp and hcomp. The KanOperation record stores the data associated with a Kan operation on arbitrary types: A cofibration and an element of that type.

Constructors

TranspOp

A transport problem consists of a cofibration, marking where the transport is constant, and a term to move from the fibre over i0 to the fibre over i1.

Fields

• kanOpCofib :: Blocked (Arg Term)

  When this cofibration holds, the transport must definitionally be the identity. This is handled generically by primTransHComp but specific Kan operations may still need it.

• kanOpBase :: Arg Term

  This is the term in A i0 which we are transporting.

HCompOp

A composition problem consists of a partial element and a base. Semantically, this is justified by the types being Kan fibrations, i.e., having the lifting property against trivial cofibrations. While the specified cofibration may not be trivial, (φ ∨ ~ r) for r ∉ φ is *always* a trivial cofibration.

Fields

• kanOpCofib :: Blocked (Arg Term)

  When this cofibration holds, the transport must definitionally be the identity. This is handled generically by primTransHComp but specific Kan operations may still need it.

• kanOpSides :: Arg Term

  The partial element itself

• kanOpBase :: Arg Term

  This is the term in A i0 which we are transporting.

kanOpName :: KanOperation -> String

The built-in name associated with a particular Kan operation.

data TermPosition

For the Kan operations in Glue and hcomp {Type}, we optimise evaluation a tiny bit by differentiating the term produced when evaluating a Kan operation by itself vs evaluating it under unglue.

Constructors

Head

Eliminated

Instances

Show TermPosition

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

showsPrec :: Int -> TermPosition -> ShowS

show :: TermPosition -> String

showList :: [TermPosition] -> ShowS

Eq TermPosition

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

(==) :: TermPosition -> TermPosition -> Bool

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

headStop :: PureTCM m => TermPosition -> m Term -> m Bool

If we're computing a Kan operation for one of the "unstable" type formers (Glue, hcomp {Type}), this tells us whether the type will reduce further, and whether we should care.

When should we care? When we're in the Head TermPosition. When will the type reduce further? When φ, its formula, is not i1.

data FamilyOrNot a

Are we looking at a family of things, or at a single thing?

Constructors

IsFam

Fields

• famThing :: a

IsNot

Fields

• famThing :: a

Instances

Foldable FamilyOrNot

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

fold :: Monoid m => FamilyOrNot m -> m

foldMap :: Monoid m => (a -> m) -> FamilyOrNot a -> m

foldMap' :: Monoid m => (a -> m) -> FamilyOrNot a -> m

foldr :: (a -> b -> b) -> b -> FamilyOrNot a -> b

foldr' :: (a -> b -> b) -> b -> FamilyOrNot a -> b

foldl :: (b -> a -> b) -> b -> FamilyOrNot a -> b

foldl' :: (b -> a -> b) -> b -> FamilyOrNot a -> b

foldr1 :: (a -> a -> a) -> FamilyOrNot a -> a

foldl1 :: (a -> a -> a) -> FamilyOrNot a -> a

toList :: FamilyOrNot a -> [a]

null :: FamilyOrNot a -> Bool

length :: FamilyOrNot a -> Int

elem :: Eq a => a -> FamilyOrNot a -> Bool

maximum :: Ord a => FamilyOrNot a -> a

minimum :: Ord a => FamilyOrNot a -> a

sum :: Num a => FamilyOrNot a -> a

product :: Num a => FamilyOrNot a -> a

Traversable FamilyOrNot

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

traverse :: Applicative f => (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)

sequenceA :: Applicative f => FamilyOrNot (f a) -> f (FamilyOrNot a)

mapM :: Monad m => (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)

sequence :: Monad m => FamilyOrNot (m a) -> m (FamilyOrNot a)

Functor FamilyOrNot

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

fmap :: (a -> b) -> FamilyOrNot a -> FamilyOrNot b

(<$) :: a -> FamilyOrNot b -> FamilyOrNot a

Reduce a => Reduce (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a)

reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a))

Show a => Show (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

showsPrec :: Int -> FamilyOrNot a -> ShowS

show :: FamilyOrNot a -> String

showList :: [FamilyOrNot a] -> ShowS

Eq a => Eq (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

(==) :: FamilyOrNot a -> FamilyOrNot a -> Bool

(/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool

familyOrNot :: IsString p => FamilyOrNot a -> p

Helper functions for building terms

combineSys

Arguments

:: forall (m :: Type -> Type). HasBuiltins m

=> NamesT m Term

-> NamesT m Term

-> [(NamesT m Term, NamesT m Term)]

A list of (ψ, PartialP ψ λ o → A (... o ...)) mappings. Note that by definitional proof-irrelevance of IsOne, the actual injection can not matter here.

-> NamesT m Term

Build a partial element. The type of the resulting partial element can depend on the computed extent, which we denote by φ here. Note that φ is the n-ary disjunction of all the ψs.

combineSys' :: forall (m :: Type -> Type). HasBuiltins m => NamesT m Term -> NamesT m Term -> [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)

Build a partial element, and compute its extent. See combineSys for the details.

fiber :: forall (m :: Type -> Type). (HasBuiltins m, HasConstInfo m) => NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term

Helper function for constructing the type of fibres of a function over a given point.

hfill :: forall (m :: Type -> Type). (HasBuiltins m, HasConstInfo m) => NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term

Helper function for constructing the filler of a given composition problem.

decomposeInterval' :: HasBuiltins m => Term -> m [(IntMap BoolSet, [Term])]

Decompose an interval expression φ : I into a set of possible assignments for the variables mentioned in φ, together any leftover neutral terms that could not be put into IntervalView form.

decomposeInterval :: HasBuiltins m => Term -> m [(IntMap Bool, [Term])]

Decompose an interval expression i : I as in decomposeInterval', but discard any inconsistent mappings.

reduce2Lam :: Term -> ReduceM (Blocked Term)

isCubicalSubtype :: PureTCM m => Type -> m (Maybe (Term, Term, Term, Term))

Are we looking at an application of the Sub type? If so, return: * The type we're an extension of * The extent * The partial element.