Agda-2.6.4.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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. (See headStop below.)

Constructors

Head 
Eliminated 

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

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

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

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

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