Agda.TypeChecking.Primitive.Cubical.Base

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

Our good friend the interval type.

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

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

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.

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

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

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

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

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.

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

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

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.

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

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.

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

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

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

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.

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

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.