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. (See headStop below.)

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

Kan operations for the "unstable" type formers (Glue, hcomp {Type}) are computed "negatively": they never actually produce a glue φ t a term. Instead, we block the computation unless such a term would reduce further, which happens in two cases:

• when the formula φ is i1, in which case we reduce to t;
• when we're under an unglue, i.e. in Eliminated TermPosition, in which case we reduce to a.

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

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