Agda-2.6.3: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Primitive.Cubical.Base

Description

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

Synopsis

Documentation

requireCubical Source #

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

Our good friend the interval type.

primIMin' :: TCM PrimitiveImpl Source #

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

primIMax' :: TCM PrimitiveImpl Source #

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

primDepIMin' :: TCM PrimitiveImpl Source #

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

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

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

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

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

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

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

data Command Source #

Constructors

DoTransp 
DoHComp 

Instances

Instances details
Show Command Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Eq Command Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Methods

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

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

data KanOperation Source #

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

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

data TermPosition Source #

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 

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

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

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

Constructors

IsFam 

Fields

IsNot 

Fields

Instances

Instances details
Foldable FamilyOrNot Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

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

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Show a => Show (FamilyOrNot a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Eq a => Eq (FamilyOrNot a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Helper functions for building terms

combineSys Source #

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

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

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

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

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

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

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

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

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.