Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Primitive.Cubical.Base

Contents

Helper functions for building terms

Description

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

Synopsis

requireCubical :: Cubical -> String -> TCM ()
primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type
primIMin' :: TCM PrimitiveImpl
primIMax' :: TCM PrimitiveImpl
primDepIMin' :: TCM PrimitiveImpl
primINeg' :: TCM PrimitiveImpl
imax :: HasBuiltins m => m Term -> m Term -> m Term
imin :: HasBuiltins m => m Term -> m Term -> m Term
ineg :: HasBuiltins m => m Term -> m Term
data Command
- = DoTransp
- | DoHComp
data KanOperation
- = TranspOp {
  - kanOpCofib :: Blocked (Arg Term)
  - kanOpBase :: Arg Term
  }
- | HCompOp {
  - kanOpCofib :: Blocked (Arg Term)
  - kanOpSides :: Arg Term
  - kanOpBase :: Arg Term
  }
kanOpName :: KanOperation -> String
data TermPosition
- = Head
- | Eliminated
headStop :: PureTCM m => TermPosition -> m Term -> m Bool
data FamilyOrNot a
- = IsFam {
  - famThing :: a
  }
- | IsNot {
  - famThing :: a
  }
familyOrNot :: IsString p => FamilyOrNot a -> p
combineSys :: forall (m :: Type -> Type). HasBuiltins m => NamesT m Term -> NamesT m Term -> [(NamesT m Term, NamesT m Term)] -> NamesT m Term
combineSys' :: forall (m :: Type -> Type). HasBuiltins m => NamesT m Term -> NamesT m Term -> [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
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
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
decomposeInterval' :: HasBuiltins m => Term -> m [(IntMap BoolSet, [Term])]
decomposeInterval :: HasBuiltins m => Term -> m [(IntMap Bool, [Term])]
reduce2Lam :: Term -> ReduceM (Blocked Term)
isCubicalSubtype :: PureTCM m => Type -> m (Maybe (Term, Term, Term, Term))

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 Methods showsPrec :: Int -> Command -> ShowS # show :: Command -> String # showList :: [Command] -> ShowS #
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

Instances

Instances details

Show TermPosition Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods showsPrec :: Int -> TermPosition -> ShowS # show :: TermPosition -> String # showList :: [TermPosition] -> ShowS #
Eq TermPosition Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods (==) :: TermPosition -> TermPosition -> Bool # (/=) :: TermPosition -> TermPosition -> Bool #

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 famThing :: a
IsNot
Fields famThing :: a

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 Methods reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a) Source # reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a)) Source #
Show a => Show (FamilyOrNot a) Source #
Instance details 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) Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods (==) :: FamilyOrNot a -> FamilyOrNot a -> Bool # (/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool #

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

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.

reduce2Lam :: Term -> ReduceM (Blocked Term) Source #

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.