Cubical Syntax for Reflection-Free Extensional Equality
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
TL;DR
This paper introduces XTT, a cubical reconstruction of Observational Type Theory that supports function extensionality and UIP, with a focus on algebraic canonicity and practical decidability of typing.
Contribution
It presents a novel cubical extension of type theory with a canonicity theorem and conjectures practical decidability of the typing relation.
Findings
Establishes an algebraic canonicity theorem for boolean types.
Introduces a cubical reconstruction of Observational Type Theory.
Conjectures practical decidability of the typing relation.
Abstract
We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-L\"of's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity types principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel cubical extension (independently proposed by Awodey) of the logical families or categorical gluing argument inspired by Coquand and Shulman: every closed element of boolean type is derivably equal to either 'true' or 'false'.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Carnegie Mellon University and http://cs.cmu.edu/~jmsterli[email protected]://orcid.org/0000-0002-0585-5564 Carnegie Mellon University and http://cs.cmu.edu/~cangiuli[email protected]://orcid.org/0000-0002-9590-3303 Aarhus University and http://jozefg.github.io [email protected]://orcid.org/0000-0003-1944-0789
\CopyrightJonathan Sterling, Carlo Angiuli, and Daniel Gratzer {CCSXML} <ccs2012> <concept> <concept_id>10003752.10003790.10011740</concept_id> <concept_desc>Theory of computation Type theory</concept_desc> <concept_significance>500</concept_significance> </concept> <concept> <concept_id>10003752.10010124.10010131.10010132</concept_id> <concept_desc>Theory of computation Algebraic semantics</concept_desc> <concept_significance>500</concept_significance> </concept> <concept> <concept_id>10003752.10010124.10010131.10010133</concept_id> <concept_desc>Theory of computation Denotational semantics</concept_desc> <concept_significance>500</concept_significance> </concept> </ccs2012>
\ccsdesc[500]Theory of computation Type theory \ccsdesc[500]Theory of computation Algebraic semantics \ccsdesc[500]Theory of computation Denotational semantics \fundingThe authors gratefully acknowledge the support of the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR.
Acknowledgements.
We thank Steve Awodey, Lars Birkedal, Evan Cavallo, David Thrane Christiansen, Thierry Coquand, Kuen-Bang Hou (Favonia), Marcelo Fiore, Jonas Frey, Krzysztof Kapulkin, András Kovács, Dan Licata, Conor McBride, Darin Morrison, Anders Mörtberg, Michael Shulman, Bas Spitters, and Thomas Streicher for helpful conversations about extensional equality, algebraic type theory, and categorical gluing. We thank our anonymous reviewers for their insightful comments, and especially thank Robert Harper for valuable conversations throughout the development of this work. We also thank Paul Taylor for his diagrams package, which we have used to typeset the commutative diagrams in this paper.
\hideLIPIcs\EventEditorsHerman Geuvers \EventNoEds1 \EventLongTitle4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) \EventShortTitleFSCD 2019 \EventAcronymFSCD \EventYear2019 \EventDateJune 24–30, 2019 \EventLocationDortmund, Germany \EventLogo \SeriesVolume131 \ArticleNo32
Cubical Syntax for Reflection-Free Extensional Equality
Jonathan Sterling
Carlo Angiuli
Daniel Gratzer
Abstract
We contribute XTT, a cubical reconstruction of Observational Type Theory [7] which extends Martin-Löf’s intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel cubical extension (independently proposed by Awodey) of the logical families or categorical gluing argument inspired by Coquand and Shulman [28, 52]: every closed element of boolean type is derivably equal to either or .
keywords:
Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity
category:
\supplement
1 Introduction
The past fifty years of constructive type theory can be summed up as the search for a scientific understanding of equality, punctuated by moments of qualitative change in our perception of the boundary between semantics (actual construction) and syntax (proof theory) from a type-theoretic point of view. Computation is critical to both the semantics and syntax of type theory—from Martin-Löf’s meaning explanations [47], supplying type theory with its direct semantics and intuitionistic grounding, to syntactic properties such as closed and open canonicity which establish computation as the indispensible method for deriving equations.
For too long, a limiting perspective on extensional type theory has prevailed, casting it as a particular syntactic artifact (for instance, the formalism obtained by stripping of their meaning the rules which incidentally appear in Martin-Löf’s monograph [47]), a formal system which enjoys precious few desirable syntactic properties and is distinguished primarily by its equality reflection rule.
We insist on the contrary that the importance of extensional type theory lies not in the specific choice of syntactic presentation (historically, via equality reflection), but rather in the semantic characteristics of its equality connective, which are invariant under choice of syntax. The specifics of how such an equality construct is presented syntactically are entirely negotiable (the internal language of a doctrine is determined only up to equivalence), and therefore has an empirical component.
1.1 Internalizing equality: from judgments to types
Equality in type theory begins with a form of judgment , which expresses that and are exactly the same type; because types can depend on terms, one also includes a form of judgment to express that and are exactly the same element of . This kind of equality, called judgmental equality, is silent in the sense that if holds and holds, then without further ado.
Judgmental equality in type theory is a completely top-level affair: it cannot be assumed or negated. On the other hand, both programming and mathematics require one to establish equations under the assumption of other equations (for instance, as part of an induction hypothesis). For this reason, it is necessary to internalize the judgmental equality as a type which can be assumed, negated, or inhabited by induction.
The simplest way to internalize judgmental equality as a type is to provide introduction and elimination rules which make the existence of a proof of equivalent to the judgment :
[TABLE]
The elimination rule above is usually called equality reflection, and is characteristic of extensional versions of Martin-Löf’s type theory. This presentation of the equality type is very strong, and broadens the reach of judgmental equality into assertions of higher-level.
A consequence of the equality reflection rule is that judgmental equality is no longer decidable, a pragmatic concern which affects implementation and usability. On the other hand, equality reflection implies numerous critical reasoning principles, including function extensionality (if two functions agree on all inputs, then they are equal), a judgmental version of the famous unicity of identity proofs (UIP) principle (any two elements of the equality type are equal), and perhaps the most crucial consequence of internalized equality, coercion (if and , then there is some term ; in this case, ).
1.2 Extensional equality via equality reflection
The earliest type-theoretic proof assistants employed the equality reflection rule (or equivalent formulations) in order to internalize the judgmental equality, a method most famously represented by Nuprl [26] and its descendents, including RedPRL [10]. The Nuprl-style formalisms act as a “window on the truth” for a single intended semantics inspired by Martin-Löf’s computational meaning explanations [2]; semantic justification in the computational ontology is the only consideration when extending the Nuprl formalism with a new rule, in contrast to other traditions in which global properties (e.g. admissibility of structural rules, decidability of typing, interpretability in multiple models, etc.) are treated as definitive.
Rather than supporting type checking, proof assistants in this style rely heavily on interactive development of typing derivations using tactics and partial decision procedures. A notable aspect of the Nuprl family is that their formal sequents range not over typed terms (proofs), but over untyped raw terms (realizers); a consequence is that during the proof process, one must repeatedly establish numerous type functionality subgoals, which restore the information that is lost when passing from a proof to a realizer. To mitigate the corresponding blow-up in proof size, Nuprl relies heavily on untyped computational reasoning via pointwise functionality, a non-standard semantics for dependently typed sequents which has some surprising consequences, such as refuting the principle of dependent cut [42].
Another approach to implementing type theory with equality reflection is exemplified in the experimental Andromeda proof assistant [16], in which proofs are also built interactively using tactics, but judgments range over abstract proof derivations rather than realizers. This approach mitigates to some degree the practical problems caused by erasing information prematurely, and also enables interpretation into a broad class of semantic models.
Although Nuprl/RedPRL and Andromeda illustrate that techniques beyond mere type checking are profitable to explore, the authors’ experiences building and using RedPRL for concrete formalization of mathematics underscored the benefits of having a practical algorithm to check types, particularly in the setting of cubical type theory (Section 1.6), whose higher-dimensional structure significantly reduces the applicability of Nuprl-style untyped reasoning.
In particular, whereas it is possible to treat all -rules and many -rules in non-cubical type theory as untyped rewrites, such an approach is unsound for the cubical account of higher inductive types and univalence [11]; consequently, in RedPRL many / rewrites must emit auxiliary proof obligations. Synthesizing these experiences and challenges led to the creation of the redtt proof assistant for Cartesian cubical type theory [9].
1.3 Equality in intensional type theory
Martin-Löf’s Intensional Type Theory (ITT) [45, 50] represents another extremal point in the internalization of judgmental equality. ITT underapproximates the equality judgment via its identity type, characterized by rules like the following:
[TABLE]
Symmetry, transitivity and coercion follow from the elimination rule of the identity type. Other properties which follow directly from equality reflection, such as the unicity of identity proofs and function extensionality, are not validated by ITT; indeed, there are sufficiently intensional models of the identity type to refute both properties [55, 37]. While the desirability of the unicity principle is perhaps up for debate, especially in light of recent developments in Homotopy Type Theory [58], theorists and practitioners alike generally agree that function extensionality is desirable.
A significant selling-point for ITT is that, by avoiding equality reflection, it presents a theory which can be implemented using type checking and normalization. Consequently, and rules are totally automatic and never require intervention from the user—in contrast to systems like RedPRL, whose users are accustomed to establishing equivalences by hand at times when heuristical tactics prove inadequate. The downsides of pure ITT, however, are manifold: function extensionality is absolutely critical in practice.
1.4 Setoids and internal model constructions
A standard technique for avoiding the deficiencies of the identity type in ITT is the setoid construction [35], an exact completion which glues an equivalence relation onto each type in the spirit of Bishop [17]. When using setoids, a function consists of a type-theoretic function together with a proof that it preserves the equivalence relation, ; a dependent setoid (family of setoids) is a type-theoretic family equipped with a coherent coercion operator.
Setoids are a discipline for expressing internally precisely the extrinsic properties required for constructions to be extensional (compatible with equality); these extra proof obligations must be satisfied in parallel with constructions at every turn. The state of affairs for setoids is essentially analogous to that of proof assistants with equality reflection, in which type functionality subgoals play a similar role to the auxiliary paperwork generated by setoids.
Paradoxically, however, every construction in ordinary ITT is automatically extensional in this sense. A solution to the problem of equality in type theory should, unlike setoids, take advantage of the fact that type theory is already restricted to extensional constructions, adding to it only enough language to refer to equality internally. This is the approach taken by both Observational Type Theory and XTT.
1.5 Observational Type Theory
The first systematic solution to the problem of syntax for extensional equality without equality reflection was Observational Type Theory (OTT) [6, 7], which built on early work by Altenkirch and McBride [3, 48]. The central idea of OTT is to work with a closed universe of types, defining by recursion for each pair of types a type of proofs that and are equal, and for each pair of elements and , a type of proofs that and are (heterogeneously) equal. Finally, one defines “generic programs” by recursion on type structure which calculate coercions and coherences along proofs of equality.
One can think of OTT as equipping the semantic setoid construction with a direct-style type-theoretic language, and adding to it closed, inductively defined universes of types. The heterogeneous equality of OTT, initially a simplifying measure adopted from McBride’s thesis [48], is an early precursor of the dependent paths which appear in Homotopy Type Theory [58], Cubical Type Theory [25, 8, 11], and XTT.
Recently, McBride and his collaborators have made progress toward a cubical version of OTT, using a different cube category and coercion structure, in which one coerces only from [math] to , and obtains fillers using an affine rescaling operation [24].
1.6 Cubical Type Theory
In a rather different line of research, Voevodsky showed that Intensional Type Theory is compatible with a univalence axiom yielding an element of for every equivalence (coherent isomorphism) between types [41, 58]. A univalent universe classifies types under a certain size cut-off in the sense of higher topos theory [44]. However, Intensional Type Theory extended with univalence lacks canonicity, because identity elimination computes only on and not on proofs constructed by univalence.
Since then, cubical type theories have been developed to validate univalence without disrupting canonicity [25, 11]. These type theories extend Martin-Löf’s type theory with an abstract interval, maps out of which represent paths, a higher-dimensional analogue to equality; the interval has abstract elements, represented by a new sort of dimension variable , and constant endpoints . Coercions arise as an instance of Kan structure governed directly by the structure of paths between types, which are nothing more than types dependent on an additional dimension variable.
There are currently two major formulations of cubical type theory. De Morgan cubical type theory [25] equips the interval with negation and binary connection (minimum and maximum) operations. Cartesian cubical type theory [8, 11], the closest relative of XTT, has no additional structure on the interval, but equips types with a much stronger notion of coercion generalizing the one described in Section 2.1.1.
1.7 Our contribution: XTT
We contribute XTT (Section A.2), a new type theory that supports extensional equality without equality reflection, using ideas from cubical type theory [25, 8, 11]. In particular, we obtain a compositional account of propositional equality satisfying function extensionality and a judgmental version of the unicity of identity proofs—when , we have judgmentally—enabling us to substantially simplify our Kan operations (Section 2.1.2). Moreover, XTT is closed under a cumulative hierarchy111As in previous work [53], we employ an algebraic version of cumulativity which does not require subtyping. of closed universes à la Russell. We hope to integrate XTT into the redtt cubical proof assistant [9] as an implementation of extensional equality in the style of two-level type theory [11].
A common thread that runs through the XTT formalism is the decomposition of constructs from OTT into more modular, judgmental principles. For instance, rather than defining equality separately at every type and entangling the connectives, we define equality once and for all using the interval. Likewise, rather than ensuring that equality proofs are unique through brute force, we obtain unicity using a structural rule which does not mention the equality type.
By first developing the model theory of XTT in an algebraic way (Section 3), we then prove a canonicity theorem for the initial model of XTT (Section 3.2): any closed term of boolean type is equal to either or . This result is obtained using a novel extension of the categorical gluing technique described by Coquand and Shulman [28, 52], in which one glues along a cubical nerve functor from XTT’s syntactic category into cubical sets. We learned after completion of this paper that the idea of proving canonicity for cubical type theories by gluing along a cubical nerve functor was circulated informally by Awodey some years prior, and is being independently developed by Awodey and Fiore. Canonicity expresses a form of “computational adequacy”—in essence, that the equational theory of XTT suffices to derive any equation which ought to hold by (closed) computation—and is one of many syntactical considerations that experience has shown to be correlated to usability.
2 Programming and proving in XTT
Like other cubical type theories, the XTT language extends Martin-Löf’s type theory with a new sort of variable ranging over an abstract interval with global elements [math] and ; we call an element of the interval a dimension, and we write to range over a constant dimension [math] or . Cubical type theories like XTT also use a special kind of hypothesis to constrain the values of dimensions: when and are dimensions, then is a constraint. In XTT, a single context accounts for both dimension variables () and constraints (). We will write for when a dimension is valid in a dimension context . The judgment holds when and are equal as dimensions with respect to the constraints in . Dimensions can be substituted for dimension variables, an operation written .
Finally, ordinary type-theoretic assumptions are kept in a context that depends on . In XTT, a full context is therefore written . The meaning of a judgment at context is completely determined by its instance under the substitution . Under the false constraint , all judgments hold; the resulting collapse of the typing judgment and the judgmental equality does not disrupt any important metatheoretic properties, because the theory of dimensions is decidable.
The general typehood judgment means that is a type of universe level in context over the cube ; note that this judgment presupposes the well-formedness of . Likewise, the element typing judgment means that is an element of the type in over as above; this form of judgment presupposes the well-formedness of and thence . We also have typed judgmental equality and , which presuppose the well-formedness of all their constituents.
Dependent equality types
XTT extends Martin-Löf type theory with dependent equality types when and and . Geometrically, elements of this type are lines or paths in the type ranging over dimension , with left endpoint and right endpoint .222Our dependent equality types are locally the same as dependent path types from cubical type theories; however, we have arranged in XTT for them to satisfy a unicity principle by which they earn the name “equality” rather than “path”. This type captures internally the equality of and ; dependency of on the dimension is in essence a cubical reconstruction of heterogeneous equality, albeit with different properties from the version invented by McBride in his thesis [48].
An element of the equality type is formed by the dimension -abstraction , requiring that is an element of in the extended context, and that are the left and right sides of respectively. Proofs of equality are eliminated by dimension application, , and are subject to rules analogous to those for function types. Finally, we have always, extending Gentzen’s principle of inversion to the side condition that we placed on . More formally:
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,i\mid{\Gamma}\vdash{}M:A}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,i=\varepsilon\mid{\Gamma}\vdash{}M=N_{\varepsilon}:A}}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\lambda{i}.{M}:\mathsf{Eq}{i.A}(N{0},N_{1})}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r\ \mathit{dim}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:\mathsf{Eq}{i.A}(N{0},N_{1})}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:\mathsf{Eq}{i.A}(N{0},N_{1})}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M(r):A\langle{r}/{i}\rangle}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:\mathsf{Eq}{i.A}(N{0},N_{1})}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M(\varepsilon)=N_{\varepsilon}:A\langle{\varepsilon}/{i}\rangle}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:\mathsf{Eq}{i.A}(N{0},N_{1})}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M=\lambda{i}.{M(i)}:\mathsf{Eq}{i.A}(N{0},N_{1})}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,i\mid{\Gamma}\vdash{}M:A}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}(\lambda{i}.{M})(r)=M\langle{r}/{i}\rangle:A\langle{r}/{i}\rangle}}}}}}
Function extensionality
A benefit of the cubical formulation of equality types is that the principle of function extensionality is trivially derivable in a computationally well-behaved way. Suppose that and we have a family of equalities ; then, we obtain a proof that equals by abstraction and application:
[TABLE]
In semantics of type theory, the structure of equality on a type usually mirrors the structure of the elements of that type in a straightforward way: for instance, a function of equations is used to equate two functions, and a pair of equations is used to equate two pairs. The benefit of the cubical approach is that this observation, at first purely empirical, is systematized by defining equality in every type in terms of the elements of that type in a context extended by a dimension.
Judgmental unicity of equality: boundary separation
In keeping with our desire to provide convenient syntax for working with extensional equality, we want proofs of the same equation to be judgmentally equal. Rather than adding a rule to that effect, whose justification in the presence of the elimination rules for equality types would be unclear, we instead impose a more primitive boundary separation principle at the judgmental level: every term is completely determined by its boundary.333We call this principle “boundary separation” because it turns out to be exactly the fact that the collections of types and elements, when arranged into presheaves on the category of contexts, are separated with respect to a certain coverage on this category. We develop this perspective in the appendices.
[TABLE]
In this rule we have abbreviated and as . We shall make use of this notation throughout the paper.
We can now derive a rule that (judgmentally) equates all .
Proof.
If , then to show that , it suffices to show that ; by the congruence rule for equality abstraction, it suffices to show that in the extended context. But by boundary separation, we may pivot on the boundary of , and it suffices to show that and . But these are automatic, because and are both proofs of , and therefore . ∎
In an unpublished note from 2017, Thierry Coquand identifies a class of cubical sets equivalent to our separated types, calling them “Bishop sets” [27].
2.1 Kan operations: coercion and composition
How does one use a proof of equality? We must have at least a coercion operation which, given a proof , coherently transforms elements to elements of .
2.1.1 Generalized coercion
In XTT, coercion and its coherence are obtained as instances of one general operation: for any two dimensions and a line of types , if is an element of , then is an element of .
[TABLE]
In the case of a proof of equality between types, we coerce to the type using the instance . But how does relate to its coercion? Coherence of coercion demands their equality, although such an equation must relate terms of (formally) different types; this heterogeneous equality is stated in XTT using a dependent equality type . To construct an element of this equality type, we use the same coercion operator but with a different choice of ; we construct this filler by coercing from [math] to a fresh dimension, obtaining : {diagram}
To see that the filler has the correct boundary with respect to , we inspect its instances under the substitutions . First, we observe that the right-hand side is exactly ; second, we must see that is , bringing us to an important equation that we must impose generally:
[TABLE]
How do coercions compute?
In order to ensure that proofs in XTT can be computed to a canonical form, we need to explain generalized coercion in each type in terms of the elements of that type. To warm up, we explain how coercion must compute in a non-dependent function type:
[TABLE]
That is, we abstract a variable and need to obtain an element of type . By reverse coercion, we obtain ; by applying to this, we obtain an element of type . Finally, we coerce from to . The version for dependent function types is not much harder, but requires a filler:
[TABLE]
The case for dependent pair types is similar, but without the contravariance:
[TABLE]
Coercions for base types (like ) are uniformly determined by regularity, a rule of XTT stating that if is a type which doesn’t vary in the dimension , then is just . Regularity makes type sense because ; semantically, it is more difficult to justify in the presence of standard universes, and is not known to be compatible with principles like univalence.444Regularity is proved by Swan to be incompatible with univalent universes assuming that certain standard techniques are used [56]; however, it is still possible that there is a different way to model univalent universes with regularity. Awodey constructs a model of intensional type theory without universes in regular Kan cubical sets [13], using the term normality for what we have called regularity. But XTT is specifically designed to provide a theory of equality rather than paths, so we do not expect or desire to justify univalence at this level.555Indeed, unicity of identity proofs is also incompatible with univalence. XTT is, however, compatible with a formulation in which it is just one level of a two-level type theory, along the lines of Voevodsky’s Homotopy Type System, in which the other level would have a univalent notion of path that coexists in harmony with our notion of equality [59, 11].
The only difficult case is to define coercion for equality types; at first, we might try to define as , but this does not make type-sense: we need to see that \mathopen{\big{(}}[i.A]\mathbin{\downarrow^{r}_{r^{\prime}}}P(j)\mathclose{\big{)}}\langle{\varepsilon}/{j}\rangle=N_{\varepsilon}, but we only obtain \mathopen{\big{(}}[i.A]\mathbin{\downarrow^{r}_{r^{\prime}}}P(j)\mathclose{\big{)}}\langle{\varepsilon}/{j}\rangle=[i.A]\mathbin{\downarrow^{r}_{r^{\prime}}}N_{\varepsilon}, which is “off by” a coercion. Intuitively, we can solve this problem by specifying what values a coercion takes under certain substitutions: in this case, under , and under . We call the resulting operation generalized composition.
2.1.2 Generalized composition
For any dimensions and a line of types , if is an element of and are lines of elements of defined respectively on the subcubes such that , then is an element of . This is called the composite of with from to , schematically abbreviated . As with coercion, when , we have , and moreover, if , we have .
Returning to coercion for equality types, we now have exactly what we need:
[TABLE]
Next we must explain how the generalized composition operation computes at each type; in previous works [11], we have seen that it is simpler to instead define generalized composition in terms of a simpler homogeneous version, in which one composes in a type rather than a line of types ; we write for this homogeneous composition, defining the generalized composition in terms of it as follows:
[TABLE]
Surprisingly, in XTT we do not need to build in any computation rules for homogeneous composition, because they are completely determined by judgmental boundary separation. For instance, we can derive a computation rule already for homogeneous composition in the dependent function type, by observing that the equands have the same boundary with respect to the dimension :
[TABLE]
From homogeneous composition, we obtain symmetry and transitivity for the equality types. Given , we obtain an element of type as follows:
[TABLE]
Furthermore, given , we obtain an element of type as follows:
[TABLE]
Example 2.1** (Identity type).**
It is possible to define Martin-Löf’s identity type and its eliminator, albeit with a much stronger computation rule than is customary.
[TABLE]
This particular definition of relies on XTT’s boundary separation rule, but one could instead define it in a more complicated way without boundary separation. However, that this construction of the identity type models the computation rule relies crucially on regularity, which does not hold in other cubical type theories whose path types validate univalence. In the absence of regularity, one can define an operator with the same type as but which satisfies its computation rule only up to a path.
2.2 Closed universes and type-case
In Section 2.1.1, we showed how to calculate coercions in each type former . In previous cubical type theories [25, 11], one could “uncover” all the things that a coercion must be equal to by reducing according to the rules which inspect the interior of the type line . While this strategy can be used to establish canonicity for closed terms, it fails to uncover certain reductions for open terms, a prerequisite for algorithmic type checking.
Specifically, given a variable , the coercion is not necessarily stuck, unlike in other cubical type theories. Suppose that we can find further proofs and ; in this case, is also a proof of , so by boundary separation it must be equal to , and therefore must be equal to . But the type-directed reduction rule for coercion applies only to the latter! Generally, to see how to reduce the first coercion, it seems that we need to be able to “dream up” proofs out of thin air, or determine that they can’t exist, an impossible task.
In XTT, we cut this Gordian knot by ensuring that always exist, following the approach employed in OTT. To invert the equation into and , we add an intensional type-case operator to XTT, committing to a closed and inductive notion of universe by allowing pattern-matching on types [50]. It is also possible to extend XTT with open and/or univalent universes which themselves lack boundary separation, as in two-level type theories.
For illustrative purposes, consider coercion along an equality between dependent function types. Given , we define by type-case the following:
[TABLE]
Because of ’s boundary, we are concerned only with the branch of the above expressions, and are free to emit a “dummy” answer in other branches. With in hand, we note that using boundary separation; therefore, we are free to calculate as follows:
[TABLE]
This lazy style of computing with proofs of equality means, in particular, that coercing along an equation cannot tell the difference between a postulated axiom and a canonical proof of equality, making XTT compatible with extension by consistent equational axioms.
Remark 2.2**.**
One might wonder whether it is possible to tame the use of type-case above to something compatible with a parametric understanding of types, in which (as in OTT) one cannot branch on whether or not is a function type or a pair type, etc. It is likely that this can be done, but we stress that the fundamental difficulty is not resolved: whether or not we allow general type-case, we have not escaped the need for type constructors to be disjoint and injective, which contradicts the role of universes in mathematics as (weak) classifiers of small families. Future work on XTT and its successors must focus on resolving this issue, quite apart from any considerations of parametricity.
2.3 Future extensions
Universe of propositions
XTT currently lacks one of the hallmarks of OTT, an extensional universe of proof-irrelevant propositions. In future work, we intend to extend XTT with a reflective subuniverse of propositions closed under equality and universal and existential quantification over arbitrary types, satisfying:
- •
Proof irrelevance. For each proposition , we have for all .
- •
Extensionality (univalence). For all , we have an element of whenever there are functions and .
The reflection of the propositional subuniverse will take a type to a proof-irrelevant proposition , acting as a strict truncation or squash type [26, 51, 15]. The addition of will allow XTT to be used as a syntax for topos-theoretic constructions, with playing the role of the subobject classifier.
(Indexed) Quotient Inductive Types
Another natural extension of XTT is the addition of quotient types; already considered as an extension to OTT by the Epigram Team [19] and more recently by Atkey [12], quotient types are essential when using type theory for either programming or mathematics. One of the ideas of Homotopy Type Theory and cubical type theories in particular is to reconstruct the notion of quotienting by an equivalence relation as a special case of higher inductive type (HITs), a generalization of ordinary inductive types which allows constructors to target higher dimensions with a specified partial boundary. When working purely at the level of sets, as in XTT, these higher inductive types are called quotient inductive types (QITs) [5].
We intend to adapt the work of Cavallo and Harper [23] to a general schema for indexed quotient inductive types as an extension of XTT. The resulting system would support ordinary quotients by equivalence relations en passant, and when these equivalence relations are valued in , one can show that they are effective. Quotient inductive types also enable the construction of free algebras for infinitary algebraic theories, usually obtained in classical set theory from the non-constructive axiom of choice [18, 43]. Another application of quotient inductive types is the definition of a localization functor with respect to a class of maps, enabling users of the extended XTT to work internally with sheaf subtoposes.
The extension of XTT with quotient inductive types means that we must account for formal homogeneous composites in QITs which are canonical forms [23, 29]. Ordinarily, this introduces a severe complicating factor to a canonicity proof, because the notion of canonical form ceases to be stable under all dimension substitutions [11, 38], but we expect the proof-relevant cubical logical families technique that we introduce in Section 3 to scale directly to the case of quotient inductive types without significant change, in contrast with classical approaches based on partial equivalence relations.
3 Algebraic model theory and canonicity
We have been careful to formulate the XTT language in a (generalized) algebraic way, obtaining automatically a category of algebras and homomorphisms which is equipped with an initial object [20, 21, 40]. That this initial object is isomorphic to the model of XTT obtained by constraining and quotienting its raw syntax under judgmental equality (i.e. the Lindenbaum–Tarski algebra) is an instance of Voevodsky’s famous Initiality Conjecture [60], and we do not attempt to prove it here; we merely observe that this result has been established for several simpler type theories [54, 22].
Working within the category of XTT-algebras enables us to formulate and prove results like canonicity and normalization for the initial XTT-algebra in an economical manner, avoiding the usual bureaucratic overhead of reduction relations and partial equivalence relations, which were the state of the art for type-theoretic metatheory prior to the work of Shulman [52], Altenkirch and Kaposi [4], and Coquand [28].
Because our algebraic techniques involve defining families over only well-typed terms already quotiented by judgmental equality, we avoid many of the technical difficulties arising from working with the raw terms of cubical type theories, including the closure under “coherent expansion” which is critical to earlier cubical metatheories [11, 38]. Our abstract gluing-based approach therefore represents a methodological advance in metatheory for cubical type theories.
Theorem 3.1** (Canonicity).**
In the initial XTT-algebra, if , then either or .
Following previous work [53], we employ for our semantics a variant of categories with families (cwf) [30] which supports a predicative hierarchy of universes à la Russell. A cwf in our sense begins with a category of contexts , and a presheaf of types ; here is the category of universe levels, with objects the natural numbers and unique arrows if and only if .666Observe that ; reversing arrows allows us to move types from smaller universes to larger ones. The fiber of the presheaf of types at is written , and contains the types in context of universe level . Reindexing implements simultaneous substitution and universe level shifting {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A. In our metatheory, we assume the Grothendieck Universe Axiom, and consequently obtain a transfinite ordinal-indexed hierarchy of meta-level universes . We impose the requirement that each collection of types is -small, i.e. .
Next, we require a dependent presheaf of elements , whose fibers we write ; to interpret the actions of level lifting on terms properly, we require the functorial actions \mathsf{El}_{\mathcal{C}}(\Gamma\vdash A)\rTo\mathsf{El}_{\mathcal{C}}(\Gamma\vdash{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A) to be identities, strictly equating the fibers and \mathsf{El}_{\mathcal{C}}(\Gamma\vdash{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A). The remaining data of a basic cwf is a context comprehension, which for every context and type determines an extended context with a weakening substitution and a variable term .
Next, we specify what further structure is required to make such a cwf into an XTT-algebra. To represent contexts semantically, we use the augmented Cartesian cube category , which adjoins to the Cartesian cube category an initial object; from this, we obtain equalizers in addition to the equalizers which exist in . We then require a split fibration with a terminal object, which implements the dependency of contexts on cubes and forces appropriate dimension restrictions to exist for contexts, types and elements. The split fibration induces all the structure necessary to implement dimension operations; we refer the reader to the appendices for details. In the following discussion, we limit ourselves to a few simpler consequences. First, we can apply dimension substitutions in terms and types, writing to apply in a type in context . We can also apply dimension substitutions to contexts, written . We write for the dimension substitution which weakens by a dimension variable . Finally, we write for the set of valid dimensions expressions generated from .
Requirement** (Boundary separation in models).**
In order to enforce boundary separation in XTT-algebras we require that types and elements over them satisfy a separation property. In the appendices we phrase the full condition as a separation requirement with respect to a particular Grothendieck topology on the category of contexts. A specific consequence is the familiar boundary separation principle for types: given two types and a dimension , if for each then .
Requirement** (Coercion in models).**
An XTT-algebra must also come with a coercion structure, specifying how generalized coercion is interpreted in each type. For every type over , dimensions , and element , we require an element with the following properties (in addition to naturality requirements):
- •
Adjacency. If then .
- •
Regularity. If for some , then .
Additional equations in later requirements specify that generalized coercion computes properly in each connective. Similarly, a model must be equipped with a composition structure which specifies the interpretation of the composition operator.
Finally, we specify algebraically the data with which such a cwf must be equipped in order to model all the connectives of XTT (again, details are contained in the appendices); to distinguish the abstract (De Bruijn) syntax of the cwf from the raw syntax of XTT we use boldface, writing , \mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,r) and to correspond to , \mathsf{app}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A}}(M,r) and respectively, etc. We take a moment to specify how some of the primitives of XTT are translated into requirements on a model.
Requirement** (Dependent equality types in models).**
An XTT-algebra must model dependent equality types, which is to say that the following structure is exhibited:
- •
Formation. For each type and elements , a type .
- •
Introduction. For each , an element \mathbf{plam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash\mathbf{Eq}(i.A,(0/i)^{\ddagger}M,(1/i)^{\ddagger}M)).
- •
Elimination. For each and , an element \mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,r)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash(r/i)^{\ddagger}A) satisfying the equations \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}.
- •
Computation. For and , the equation:
[TABLE]
- •
Unicity. For , M=\mathbf{plam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},j.\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.\hat{\jmath}^{\ddagger}A},\hat{\jmath}^{\ddagger}M,j)).
- •
Level restriction. The following equations:
[TABLE]
- •
Naturality. For , the following naturality equations:
[TABLE]
- •
Coercion. When and where , we require that equals the following abstraction:
[TABLE]
Any model of extensional type theory can be used to construct a model of XTT, so long as it is equipped with a cumulative, inductively defined hierarchy of universes closed under dependent function types, dependent pair types, extensional equality types and booleans. (Meaning explanations in the style of Martin-Löf [47] are one such model.) The interpretation of XTT into extensional models involves erasing dimensions, coercions, and compositions; the only subtlety, easily managed, is to ensure that all judgments under absurd constraints hold.
3.1 The cubical logical families construction
Any XTT-algebra extends to a category of proof-relevant logical predicates, which we call logical families by analogy. The proof-relevant character of the construction enables a simpler proof of canonicity than is obtained with proof-irrelevant techniques, such as partial equivalence relations. Logical families are a type-theoretic version of the categorical gluing construction, in which a very rich semantic category (such as sets) is cut down to include just the morphisms which track definable morphisms in ;777The gluing construction is similar to realizability; the main difference is that in gluing, one considers collections of “realizers” which are not all drawn from a single computational domain. one then uses the rich structure of the semantic category to obtain metatheoretic results about syntax (choosing to be the initial model) without considering raw terms at any point in the process.
Usually, to prove canonicity one glues the initial model together with along the global sections functor; this equips each context with a family of sets indexed in the closing substitutions for . In order to prove canonicity for a cubical language like XTT, we will need a more sophisticated version of this construction, in which the global sections functor is replaced with something that determines substitutions which are closed with respect to term variables, but open with respect to dimension variables.
The split fibration induces a functor which takes every cube to the empty variable context over . This functor in turn induces a nerve construction , taking to the cubical set .888This construction is also called the relative hom functor by Fiore [31]; its use in logic originates in the study of definability for -calculus, characterizing the domains of discourse for Kripke logical predicates of varying arity [39]. We learned the connection to the abstract nerve construction in conversations with M. Fiore about his unpublished joint work with S. Awodey. Intuitively, this is the presheaf of substitutions which are closed with respect to term variables, but open with respect to dimension variables; when wearing -tinted glasses, these appear to be the closed substitutions.
This nerve construction extends to the presheaves of types and elements; we define the fiber of at to be the set ; likewise, we define the fiber of at to be the set . Internally to , we regard as a dependent type over . We will then (abusively) write for the fiber of determined by .
Category of cubical logical families
Gluing together with along gives us a category of cubical logical families whose objects are pairs , with and a dependent cubical set over the cubical set . In other words, is a “Kripke logical family” on the substitutions which commutes with dimension substitutions . A morphism is a substitution together with a proof that preserves the logical family: that is, a closed element of the type in the internal type theory of . We write for the pair . We have a fibration which merely projects from .
Glued type structure
Recall from Section 2.2 that we must model closed universes. Therefore, the standard presheaf universes which lift to (weakly) classify all -small presheaves are insufficient in our case; instead, we must equip each type with a code so that type-case is definable. Accordingly, we define for each an inductive cubical set indexed over ; internally to , the cubical set is the collection of realizers for the -type . An imprecise but helpful analogy is to think of a realizer as something like a whnf of , with the caveat that A is an element of this inductively defined set, not a -type. Simultaneously, for each , we define a cubical family of realizers of elements of , with each being the logical family of the -type ; finally, we also define realizers for coercion and composition by recursion on the realizers for types.999It is important to note that we do not use large induction-recursion in (to our knowledge, the construction of inductive-recursive definitions has not yet been lifted to presheaf toposes); instead, we model object universes using the meta-universe . This is an instance of small induction-recursion, which can be translated into indexed inductive definitions which exist in every presheaf topos [34, 49]. A fragment of this definition is summarized in Figure 2. In the definition of we freely make use of the internal type theory of . This not only exposes the underlying logical relations flavor of these definitions but simplifies a number of proofs (see the appendices).
From all this, we can define the cwf structure on . We obtain a presheaf of types by taking to be the set of pairs where and is an element of the type in the internal type theory of . To define the dependent presheaf of elements, we take to be the set of pairs where and is an element of the type in the internal type theory of . In this model, the context comprehension operation is defined as the pair where is the cubical set ; it is easy to see that we obtain realizers for the weakening substitution and the variable term.
Construction 3.2** (Dependent equality types in ).**
Recall that we required a model of XTT to have sufficient structure to interpret dependent equality types. Here, we discuss how to obtain the formation rule; the full construction can be found in the appendices. Suppose and elements and with . We wish to construct a type in .
In , such a type is a pair of a type from with an element witnessing the logical family . We will set the first component to the dependent equality type from itself, namely . For the second component, we wish to construct an element of . Inspecting the rules for from Figure 2, there is only one choice: .
Construction 3.3** (Coercion in ).**
The coercion structure on is constructed from the coercion structures on and the coercion operator for codes from Figure 2.
Given a type over , dimensions , and an element , we must construct an element of . This element must be a pair of and a term . For the former, we rely on the coercion structure for and pick . For the latter, we use the coercion operation on codes defined in Figure 2 and choose .
It is routine to check that this coercion structure enjoys adjacency, regularity, and naturality once the corresponding properties are checked for the coercion operator on codes.
Theorem 3.4**.**
is an XTT-algebra, and moreover, is a homomorphism of XTT-algebras.
3.2 Canonicity theorem
Because is an XTT-algebra, we are now equipped to prove a canonicity theorem for the initial XTT-algebra : if is an element of type in the empty context, then either or , and not both.
Proof 3.5**.**
We have , and therefore \left\llbracket M\right\rrbracket\in\mathsf{El}_{{\mathcal{C}}^{\star}}(\cdot\vdash\overline{\mathbf{bool}}). From this we obtain where N=\pi_{\mathsf{syn}}\left\llbracket M\right\rrbracket, and ; by definition, is either a proof that or a proof that (see Figure 2). Therefore, it suffices to observe that \pi_{\mathsf{syn}}\left\llbracket M\right\rrbracket=M; but this follows from the universal property of the initial XTT-algebra and the fact that is an XTT-homomorphism. Moreover, because the interpretation of in is disjoint, cannot equal both and .
Appendix A The XTT language
Annotated syntax
The raw syntax of XTT includes typing annotations on function application \mathsf{app}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M,N) and pair projections \mathsf{fst}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M) and \mathsf{snd}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M), in order to ensure that the raw syntax could (in theory) be organized into an initial model of XTT, in the sense of Appendix B. A version of the syntax with fewer annotations would be justified by a normalization result for XTT, which we do not establish here.
Because these annotations can visually obscure the meaning of a term, we adopt the notational convention that when a term is already known to be well-typed, we omit the annotation and write for \mathsf{app}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M,N), and likewise for \mathsf{fst}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M), etc.
Heterogeneous composition
Following previous work [11], we take coercion and homogeneous composition as primitive operations, and define heterogeneous composition in terms of it:
[TABLE]
Other versions of cubical type theory, such as De Morgan cubical type theory [25], take heterogeneous composition as primitive and derive both coercion and homogeneous composition as a special case. In our setting, it is especially advantageous to take coercion and homogeneous composition as a primitive, because in XTT it is only necessary to provide -rules for coercion; in Section A.3, we observe that all the -rules for homogeneous composition are in fact already derivable, by exploiting the path unicity rule in Section A.2.4.
Convention A.1** (Presupposition).**
The XTT language involves many forms of judgment, each of which is defined conditionally on a presupposition; in type-theoretic formal systems, a judgment expresses the well-formedness of a raw term (the “subject”) relative to some parameters. The parameters themselves are rarely raw terms, but rather terms that are already known to be well-formed according to certain judgments (called “presuppositions”).
We indicate this situation schematically for a form of judgment in the following way, where are parameters and is a subject:
[TABLE]
A.1 The judgments of XTT
The judgments of XTT are summarized below using A.1.
“ is an (augmented) cube” \Psi\mid{}{\Gamma}\ \mathit{ctx}$${\Psi}\ \mathit{cube\textsubscript{+}} “ is a context over ” \Psi\mid{}r\ \mathit{dim}$${\Psi}\ \mathit{cube\textsubscript{+}} “ is a dimension over ” \Psi\mid{}r=r^{\prime}\ \mathit{dim}$$\Psi\mid{}r\ \mathit{dim} “ and are equal dimensions in ” {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}A\ \mathit{type}_{k}$${\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{}{\Gamma}\ \mathit{ctx} “ is a type at level in context ” {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}A=B\ \mathit{type}_{k}$${\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}A\ \mathit{type}_{k} {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}B\ \mathit{type}_{k} “ and are equal types at level ” {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}M:A$${\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}A\ \mathit{type}_{k} “ is a term of type ” {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}M=N:A$${\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}M:A {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}N:A “ and are equal terms of type ” {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}A\ \mathit{type}_{k}\ [\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\xi\hookrightarrow B}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\xi\hookrightarrow B}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\xi\hookrightarrow B}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\xi\hookrightarrow B}}]$$\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}B\ \mathit{type}_{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}B\ \mathit{type}_{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}B\ \mathit{type}_{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}B\ \mathit{type}_{k}}} “ is a type at level which matches each at ” {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}M:A\ [\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\xi\hookrightarrow N}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\xi\hookrightarrow N}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\xi\hookrightarrow N}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\xi\hookrightarrow N}}]$${\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi}\mid{\Gamma}\vdash{}A\ \mathit{type}_{k} \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\Psi},\xi\mid{\Gamma}\vdash{}N:A}} “ is an element of which matches each at ”
A.2 The rules of XTT
In the following sections, we summarize the rules of XTT; we systematically omit obvious premises to equational rules and all congruence rules for judgmental equality, because these can be mechanically obtained from the typing rules.
A.2.1 Cubes
emp
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle{\cdot}\ \mathit{cube\textsubscript{+}}}}}}}}
snoc/dim
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle{\Psi}\ \mathit{cube\textsubscript{+}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle{\Psi,i}\ \mathit{cube\textsubscript{+}}}}}}}}
snoc/constr
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle{\Psi}\ \mathit{cube\textsubscript{+}}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r,r^{\prime}\ \mathit{dim}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle{\Psi,r=r^{\prime}}\ \mathit{cube\textsubscript{+}}}}}}}}
A.2.2 Contexts
emp
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}{\cdot}\ \mathit{ctx}}}}}}}
snoc
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}{\Gamma}\ \mathit{ctx}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}_{k}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}{\Gamma,x:A}\ \mathit{ctx}}}}}}}
A.2.3 Dimensions
constant
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}\varepsilon\ \mathit{dim}}}}}}}
variable
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle i\in\Psi}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}i\ \mathit{dim}}}}}}}
reflexivity
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r=r\ \mathit{dim}}}}}}}
symmetry
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r=r^{\prime}\ \mathit{dim}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r^{\prime}=r\ \mathit{dim}}}}}}}
transitivity
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r_{0}=r_{1}\ \mathit{dim}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r_{1}=r_{2}\ \mathit{dim}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r_{0}=r_{2}\ \mathit{dim}}}}}}}
hyp
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\ni r=r^{\prime}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r=r^{\prime}\ \mathit{dim}}}}}}}
A.2.4 Structural
variable
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Gamma\ni{}x:A}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}x:A}}}}}}
false constraint
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}0=1\ \mathit{dim}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{J}}}}}}}
conversion
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A_{0}=A_{1}\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A{0}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A_{1}}}}}}}
boundary separation (types)
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r\ \mathit{dim}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A=B\ \mathit{type}_{k}}}}}}}
boundary separation (terms)
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r\ \mathit{dim}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}M=N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}M=N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}M=N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,r=\varepsilon\mid{\Gamma}\vdash{}M=N:A}}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M=N:A}}}}}}
The following rules are admissible:
constraint cut
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r=r^{\prime}\ \mathit{dim}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi,r=r^{\prime}\mid{\Gamma}\vdash{}\mathcal{J}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{J}}}}}}}
constraint weakening
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{J}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,\xi\mid{\Gamma}\vdash{}\mathcal{J}}}}}}}
A.2.5 Coercion
coercion
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r,r^{\prime}\ \mathit{dim}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi,i\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A\langle{r}/{i}\rangle}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[i.A]\mathbin{\downarrow^{r}{r^{\prime}}}M:A\langle{r^{\prime}}/{i}\rangle}}}}}}
coercion boundary
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[i.A]\mathbin{\downarrow^{r}_{r}}M=M:A\langle{r}/{i}\rangle}}}}}}
coercion regularity
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,j,j^{\prime}\mid{\Gamma}\vdash{}A\langle{j}/{i}\rangle=A\langle{j^{\prime}}/{i}\rangle\ \mathit{type}{k}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[i.A]\mathbin{\downarrow^{r}{r^{\prime}}}M=M:A\langle{r^{\prime}}/{i}\rangle}}}}}}
A.2.6 Composition
composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r,r^{\prime},s\ \mathit{dim}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]:A}}}}}}
composition boundary
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\mathbin{\downarrow^{r}{r}}M;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]=M:A}}}}\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\mathbin{\downarrow^{r}{r}}M;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]=M:A}}}}}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[\varepsilon\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon^{\prime}\hookrightarrow j.N{\varepsilon^{\prime}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon^{\prime}\hookrightarrow j.N_{\varepsilon^{\prime}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon^{\prime}\hookrightarrow j.N_{\varepsilon^{\prime}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon^{\prime}\hookrightarrow j.N_{\varepsilon^{\prime}}}}]=N_{\varepsilon}\langle{r^{\prime}}/{j}\rangle:A}}}}}}
A.2.7 Level restrictions
lift formation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle k\leq l}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A\ \mathit{type}_{l}}}}}}}
lift element
\displaystyle\displaystyle{\hbox{\raise 1.83437pt\hbox{\displaystyle\hbox{\vbox{\hbox{\hbox{\hbox{}}}\vbox{}}}}}\atop\hbox{\lower 2.78159pt\hbox{\displaystyle\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A}}}}}}}}$$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{\displaystyle\mkern-3.0mu=\mkern-3.0mu}}\hfil\joinrel\mathrel{=}
lift hypothesis
\displaystyle\displaystyle{\hbox{\raise 1.83437pt\hbox{\displaystyle\hbox{\vbox{\hbox{\hbox{\hbox{}}}\vbox{}}}}}\atop\hbox{\lower 2.78159pt\hbox{\displaystyle\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A}\vdash{}\mathcal{J}}}}}}}}}$$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{\displaystyle\mkern-3.0mu=\mkern-3.0mu}}\hfil\joinrel\mathrel{=}
lift functoriality
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{k}}A=A\ \mathit{type}{k}}}}}\hbox{\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{k}}A=A\ \mathit{type}{k}}}}\hskip 20.00003pt\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{l}^{m}}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A={\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{m}}A\ \mathit{type}{k}}}}}}}
lift coercion
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[i.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A]\mathbin{\downarrow^{r}{r^{\prime}}}M=[i.A]\mathbin{\downarrow^{r}{r^{\prime}}}M:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A\langle{r^{\prime}}/{i}\rangle}}}}}}
A.2.8 Dependent pair types
pair formation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}(x:A)\times B\ \mathit{type}{k}}}}}}}
pair lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}(x:A)\times B=(x:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A)\times{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B\ \mathit{type}{l}}}}}}}
pair introduction
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}N:B[M/x]}}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\langle M,N\rangle:(x:A)\times B}}}}}}
pair elimination
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:(x:A)\times B}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:(x:A)\times B}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:(x:A)\times B}}}\vbox{}}}}}\over\hbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M):A}}}}\hbox{\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M):A}}}\hskip 20.00003pt\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{snd}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M):B[\mathsf{fst}(M)/x]}}}}}}
pair elimination lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B}}(M)=\mathsf{fst}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M):A}}}}\hbox{\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B}}(M)=\mathsf{fst}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M):A}}}\hskip 20.00003pt\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{snd}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B}}(M)=\mathsf{snd}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M):B[\mathsf{fst}(M)/x]}}}}}}
pair computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}(\langle M,N\rangle)=M:A}}}}\hbox{\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}(\langle M,N\rangle)=M:A}}}\hskip 20.00003pt\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{snd}(\langle M,N\rangle)=N:B[M/x]}}}}}}
pair coercion computation (1)
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}([i.(x:A)\times B]\mathbin{\downarrow^{r}{r^{\prime}}}M)=[i.A]\mathbin{\downarrow^{r}{r^{\prime}}}\mathsf{fst}(M):A\langle{r^{\prime}}/{i}\rangle}}}}}}
pair coercion computation (2)
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}H\triangleq[i.B[[i.A]\mathbin{\downarrow^{r}{i}}\mathsf{fst}(M)/x]]\mathbin{\downarrow^{r}{r^{\prime}}}\mathsf{snd}(M)}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{snd}([i.(x:A)\times B]\mathbin{\downarrow^{r}{r^{\prime}}}M)=H:B\langle{r^{\prime}}/{i}\rangle[[i.A]\mathbin{\downarrow^{r}{r^{\prime}}}\mathsf{fst}(M)/x]}}}}}}
pair unicity
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M=\langle\mathsf{fst}(M),\mathsf{snd}(M)\rangle:(x:A)\times B}}}}}}
A.2.9 Dependent function types
function formation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}(x:A)\to B\ \mathit{type}{k}}}}}}}
function lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}(x:A)\to B=(x:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A)\to{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B\ \mathit{type}{l}}}}}}}
function introduction
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}M:B}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\lambda{x}.{M}:(x:A)\to B}}}}}}
function elimination
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:A}\vdash{}B\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:(x:A)\to B}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}N:A}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:(x:A)\to B}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}N:A}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{app}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M,N):B[N/x]}}}}}}
function elimination lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{app}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B}}(M,N)=\mathsf{app}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x:A.B}}(M,N):x[N/B]}}}}}}
function computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}(\lambda{x}.{M})(N)=M[N/x]:B[N/x]}}}}}}
function coercion computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,i\mid{\Gamma}\vdash{}\widetilde{N}[i]\triangleq[i.A]\mathbin{\downarrow^{r^{\prime}}{i}}N}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}([i.(x:A)\to B]\mathbin{\downarrow^{r}{r^{\prime}}}M)(N)=[i.B[\widetilde{N}[i]/x]]\mathbin{\downarrow^{r}_{r^{\prime}}}M(\widetilde{N}[r]):C}}}}}}
function unicity
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M=\lambda{x}.{M(x)}:(x:A)\to B}}}}}}
A.2.10 Dependent equality types
equality formation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,i\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A}}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{Eq}{i.A}(N{0},N_{1})\ \mathit{type}_{k}}}}}}}
equality lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}\mathsf{Eq}{i.A}(N_{0},N_{1})=\mathsf{Eq}{i.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A}(N_{0},N_{1})\ \mathit{type}_{l}}}}}}}
equality introduction
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,i\mid{\Gamma}\vdash{}M:A\ [\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{i=\varepsilon\hookrightarrow N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{i=\varepsilon\hookrightarrow N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{i=\varepsilon\hookrightarrow N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{i=\varepsilon\hookrightarrow N_{\varepsilon}}}]}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\lambda{i}.{M}:\mathsf{Eq}{i.A}(N{0},N_{1})}}}}}}
equality elimination
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r\ \mathit{dim}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi,i\mid{\Gamma}\vdash{}A\ \mathit{type}{k}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,i,i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:\mathsf{Eq}{i.A}(N{0},N_{1})}}}\vbox{}}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{app}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A}}(M,r):A\langle{r}/{i}\rangle}}}}}}
equality elimination lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{app}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A}}(M,r)=\mathsf{app}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A}}(M,r):A\langle{r}/{i}\rangle}}}}}}
equality boundary
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:\mathsf{Eq}{i.A}(N{0},N_{1})}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M(\varepsilon)=N_{\varepsilon}:A\langle{\varepsilon}/{i}\rangle}}}}}}
equality computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}(\lambda{i}.{M})(r)=M\langle{r}/{i}\rangle:A\langle{r}/{i}\rangle}}}}}}
equality coercion computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\left([j.\mathsf{Eq}{i.A}(N{0},N_{1})]\mathbin{\downarrow^{r}{r^{\prime}}}P\right)(s)=[j.A\langle{s}/{i}\rangle]\mathbin{\downarrow^{r}{r^{\prime}}}P(s);\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]:A\langle{r^{\prime},s}/{j,i}\rangle}}}}}}
equality unicity
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M=\lambda{i}.{M(i)}:\mathsf{Eq}{i.A}(N{0},N_{1})}}}}}}
A.2.11 Booleans
boolean formation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{bool}\ \mathit{type}_{k}}}}}}}
boolean lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}\mathsf{bool}=\mathsf{bool}\ \mathit{type}{l}}}}}}}
boolean introduction
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{true}:\mathsf{bool}}}}}\hbox{\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{true}:\mathsf{bool}}}}\hskip 20.00003pt\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{false}:\mathsf{bool}}}}}}}
boolean elimination
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\mathsf{bool}}\vdash{}C\ \mathit{type}{k}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:\mathsf{bool}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}N{0}:C[\mathsf{true}/x]}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}N_{1}:C[\mathsf{false}/x]}}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{if}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x.C}}({M};{N{0}},{N_{1}}):C[M/x]}}}}}}
boolean elimination lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{if}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}C}}({M};{N_{0}},{N_{1}})=\mathsf{if}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x.C}}({M};{N{0}},{N_{1}}):{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}C[M/x]}}}}}}
boolean computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{if}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x.C}}({\mathsf{true}};{N{0}},{N_{1}})=N_{0}:C[\mathsf{true}/x]}}}}\hbox{\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{if}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x.C}}({\mathsf{true}};{N{0}},{N_{1}})=N_{0}:C[\mathsf{true}/x]}}}\hskip 20.00003pt\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{if}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}x.C}}({\mathsf{false}};{N{0}},{N_{1}})=N_{1}:C[\mathsf{false}/x]}}}}}}
A.2.12 Universes
universe formation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle k<l}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{U}{k}\ \mathit{type}{l}}}}}}}
universe lifting
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{l}^{m}}\mathcal{U}{k}=\mathcal{U}{k}\ \mathit{type}{m}}}}}}}
universe elements
\displaystyle\displaystyle{\hbox{\raise 1.83437pt\hbox{\displaystyle\hbox{\vbox{\hbox{\hbox{\hbox{}}}\vbox{}}}}}\atop\hbox{\lower 2.78159pt\hbox{\displaystyle\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{}}}}}}}}$$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{\displaystyle\mkern-3.0mu=\mkern-3.0mu}}\hfil\joinrel\mathrel{=}
universe equality
\displaystyle\displaystyle{\hbox{\raise 1.83437pt\hbox{\displaystyle\hbox{\vbox{\hbox{\hbox{\hbox{}}}\vbox{}}}}}\atop\hbox{\lower 2.78159pt\hbox{\displaystyle\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{}}}}}}}}$$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{\displaystyle\mkern-3.0mu=\mkern-3.0mu}}\hfil\joinrel\mathrel{=}
type-case
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}C\ \mathit{type}{l}}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\mathcal{U}{k},y:x\to\mathcal{U}{k}}\vdash{}M{\Pi}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\mathcal{U}{k},y:x\to\mathcal{U}{k}}\vdash{}M_{\Sigma}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x_{0}:\mathcal{U}{k},x{1}:\mathcal{U}{k},x^{=}:\mathsf{Eq}{i.\mathcal{U}{k}}(x{0},x_{1}),y_{0}:x_{0},y_{1}:x_{1}}\vdash{}M_{\mathsf{Eq}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathsf{bool}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathcal{U}}:C}}}}}}}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\mathcal{U}{k},y:x\to\mathcal{U}{k}}\vdash{}M_{\Pi}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\mathcal{U}{k},y:x\to\mathcal{U}{k}}\vdash{}M_{\Sigma}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x_{0}:\mathcal{U}{k},x{1}:\mathcal{U}{k},x^{=}:\mathsf{Eq}{i.\mathcal{U}{k}}(x{0},x_{1}),y_{0}:x_{0},y_{1}:x_{1}}\vdash{}M_{\mathsf{Eq}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathsf{bool}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathcal{U}}:C}}}}}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\mathcal{U}{k},y:x\to\mathcal{U}{k}}\vdash{}M_{\Sigma}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x_{0}:\mathcal{U}{k},x{1}:\mathcal{U}{k},x^{=}:\mathsf{Eq}{i.\mathcal{U}{k}}(x{0},x_{1}),y_{0}:x_{0},y_{1}:x_{1}}\vdash{}M_{\mathsf{Eq}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathsf{bool}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathcal{U}}:C}}}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x_{0}:\mathcal{U}{k},x{1}:\mathcal{U}{k},x^{=}:\mathsf{Eq}{i.\mathcal{U}{k}}(x{0},x_{1}),y_{0}:x_{0},y_{1}:x_{1}}\vdash{}M_{\mathsf{Eq}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathsf{bool}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathcal{U}}:C}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathsf{bool}}:C}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathcal{U}}:C}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M_{\mathcal{U}}:C}}}\vbox{}}}}}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{tycase}\ X\ [\Pi_{x}y\mapsto M_{\Pi}\mid\Sigma_{x}y\mapsto M_{\Sigma}\mid\mathsf{Eq}{x{0},x_{1},x^{=}}(y_{0},y_{1})\mapsto M_{\mathsf{Eq}}\mid\mathsf{bool}\mapsto M_{\mathsf{bool}}\mid\mathcal{U}\mapsto M_{\mathcal{U}}]:C}}}}}}
type-case computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{tycase}\ ((z:A)\to B)\ [\Pi_{x}y\mapsto M\mid\ldots]=M[A,\lambda{z}.{B}/x,y]:C}}}}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{tycase}\ ((z:A)\times B)\ [\ldots\mid\Sigma_{x}y\mapsto M\mid\ldots]=M[A,\lambda{z}.{B}/x,y]:C}}}}\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{tycase}\ \mathsf{bool}\ [\ldots\mid\mathsf{bool}\mapsto M\mid\ldots]=M:C}}\hskip 20.00003pt\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{tycase}\ \mathcal{U}_{k^{\prime}}\ [\ldots\mid\mathcal{U}\mapsto M]=M:C}}}}}}
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}H\triangleq M[A\langle{0}/{i}\rangle,A\langle{1}/{i}\rangle,\lambda{i}.{A},N_{0},N_{1}/x_{0},x_{1},x^{=},y_{0},y_{1}]}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{tycase}\ (\mathsf{Eq}{i.A}(N{0},N_{1}))\ [\ldots\mid\mathsf{Eq}{x{0},x_{1},x^{=}}(y_{0},y_{1})\mapsto M\mid\ldots]=H:C}}}}}}
A.2.13 Boundary matching
type boundary
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}\qquad\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,\xi\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,\xi\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,\xi\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,\xi\mid{\Gamma}\vdash{}A=B\ \mathit{type}{k}}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\ \mathit{type}{k}\ [\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\xi\hookrightarrow B}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\xi\hookrightarrow B}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\xi\hookrightarrow B}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\xi\hookrightarrow B}}]}}}}}}
term boundary
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A\qquad\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,\xi\mid{\Gamma}\vdash{}M=N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,\xi\mid{\Gamma}\vdash{}M=N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,\xi\mid{\Gamma}\vdash{}M=N:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,\xi\mid{\Gamma}\vdash{}M=N:A}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A\ [\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\xi\hookrightarrow N}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\xi\hookrightarrow N}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\xi\hookrightarrow N}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\xi\hookrightarrow N}}]}}}}}}
A.3 Derivable Rules
Numerous additional rules about compositions are derivable by exploiting boundary separation. In previous presentations of cubical type theory (which did not enjoy the unicity of equality proofs), it was necessary to include -rules for compositions explicitly.
composition regularity
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,j_{0},j_{1},i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}\langle{j_{0}}/{j}\rangle=N_{\varepsilon}\langle{j_{1}}/{j}\rangle:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,j_{0},j_{1},i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}\langle{j_{0}}/{j}\rangle=N_{\varepsilon}\langle{j_{1}}/{j}\rangle:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,j_{0},j_{1},i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}\langle{j_{0}}/{j}\rangle=N_{\varepsilon}\langle{j_{1}}/{j}\rangle:A}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,j_{0},j_{1},i=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}\langle{j_{0}}/{j}\rangle=N_{\varepsilon}\langle{j_{1}}/{j}\rangle:A}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}A\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]=M:A}}}}}}
heterogeneous composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{}r,r^{\prime},s\ \mathit{dim}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}M:A\langle{r}/{j}\rangle}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\Psi,j,s=\varepsilon\mid{\Gamma}\vdash{}N_{\varepsilon}:A\ [j=r\hookrightarrow M]}}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[j.A]\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]:A\langle{r^{\prime}}/{j}\rangle}}}}}}
heterogeneous composition boundary
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[j.A]\mathbin{\downarrow^{r}{r}}M;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]=M:A\langle{r}/{j}\rangle}}}}\hbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[j.A]\mathbin{\downarrow^{r}{r}}M;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]=M:A\langle{r}/{j}\rangle}}}}}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}[j.A]\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[\varepsilon\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon^{\prime}\hookrightarrow j.N{\varepsilon^{\prime}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon^{\prime}\hookrightarrow j.N_{\varepsilon^{\prime}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon^{\prime}\hookrightarrow j.N_{\varepsilon^{\prime}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon^{\prime}\hookrightarrow j.N_{\varepsilon^{\prime}}}}]=N_{\varepsilon}\langle{r^{\prime}}/{j}\rangle:A\langle{r^{\prime}}/{j}\rangle}}}}}}
lift composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]=A\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]:{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A}}}}}}
lift type composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{U}{l}\mathbin{\downarrow^{r}{r^{\prime}}}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}A;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}B{\varepsilon}}}]={\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}{k}^{l}}\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}A;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.B{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}}}]\ \mathit{type}_{k}}}}}}}
pair composition computation (1)
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}H\triangleq A\mathbin{\downarrow^{r}{r^{\prime}}}\mathsf{fst}(M);\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N_{\varepsilon})}}]}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{fst}((x:A)\times B\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}])=H:A}}}}}}
pair composition computation (2)
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,k\mid{\Gamma}\vdash{}\widetilde{M_{1}}[k]\triangleq A\mathbin{\downarrow^{r}{k}}\mathsf{fst}(M);\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.\mathsf{fst}(N_{\varepsilon})}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}H\triangleq[k.B[\widetilde{M_{1}}[k]/x]]\mathbin{\downarrow^{r}{r^{\prime}}}\mathsf{snd}(M);\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.\mathsf{snd}(N{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.\mathsf{snd}(N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.\mathsf{snd}(N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.\mathsf{snd}(N_{\varepsilon})}}]}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathsf{snd}((x:A)\times B\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}])=H:B[\widetilde{M_{1}}[r^{\prime}]/x]}}}}}}
pair type composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,k\mid{\Gamma}\vdash{}\widetilde{A}[k]\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{k}}A;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}]}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,j\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{x}[j]\triangleq[k.\widetilde{A}[k]]\mathbin{\downarrow^{r^{\prime}}{j}}x}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{B}\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}B[\widetilde{x}[r]/x];\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.B{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}]}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,j\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{x}[j]\triangleq[k.\widetilde{A}[k]]\mathbin{\downarrow^{r^{\prime}}{j}}x}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{B}\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}B[\widetilde{x}[r]/x];\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.B{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}]}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{B}\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}B[\widetilde{x}[r]/x];\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}]}}}\vbox{}}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}((x:A)\times B);\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\times B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\times B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\times B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\times B_{\varepsilon}}}]=(x:\widetilde{A}[r^{\prime}])\times\widetilde{B}\ \mathit{type}_{l}}}}}}}
function composition computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}H\triangleq B[N/x]\mathbin{\downarrow^{r}{r^{\prime}}}M(N);\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.M{\varepsilon}(N)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}(N)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}(N)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}(N)}}]}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}((x:A)\to B\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.M{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}}}])(N)=H:(x:A)\to B}}}}}}
function type composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,k\mid{\Gamma}\vdash{}\widetilde{A}[k]\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{k}}A;\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}]}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,j\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{x}[j]\triangleq[k.\widetilde{A}[k]]\mathbin{\downarrow^{r^{\prime}}{j}}x}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{B}\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}B[\widetilde{x}[r]/x];\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.B{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}]}}}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,j\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{x}[j]\triangleq[k.\widetilde{A}[k]]\mathbin{\downarrow^{r^{\prime}}{j}}x}\hskip 20.00003pt\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{B}\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}B[\widetilde{x}[r]/x];\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.B{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}]}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma,x:\widetilde{A}[r^{\prime}]}\vdash{}\widetilde{B}\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}B[\widetilde{x}[r]/x];\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.B_{\varepsilon}[\widetilde{x}[j]/x]}}]}}}\vbox{}}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}((x:A)\to B);\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\to B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\to B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\to B_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.(x:A_{\varepsilon})\to B_{\varepsilon}}}]=(x:\widetilde{A}[r^{\prime}])\to\widetilde{B}\ \mathit{type}_{l}}}}}}}
equality composition computation
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}H\triangleq A\langle{s}/{i}\rangle\mathbin{\downarrow^{r}{r^{\prime}}}P(s);\allowbreak[k\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.Q{\varepsilon}(s)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.Q_{\varepsilon}(s)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.Q_{\varepsilon}(s)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.Q_{\varepsilon}(s)}}]}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}(\mathsf{Eq}{i.A}(N{0},N_{1})\mathbin{\downarrow^{r}{r^{\prime}}}P;\allowbreak[k\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.Q{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.Q_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.Q_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.Q_{\varepsilon}}}])(s)=H:A\langle{s}/{i}\rangle}}}}}}
equality type composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi,j,i\mid{\Gamma}\vdash{}\widetilde{A}[j,i]\triangleq\mathcal{U}{k}\mathbin{\downarrow^{r}{j}}A;\allowbreak[k\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.A_{\varepsilon}}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\widetilde{M}\triangleq[j.\widetilde{A}[j,r]]\mathbin{\downarrow^{r}{r^{\prime}}}M;\allowbreak[k\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.M{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.M_{\varepsilon}}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\widetilde{N}\triangleq[j.\widetilde{A}[j,r^{\prime}]]\mathbin{\downarrow^{r}{r^{\prime}}}N;\allowbreak[k\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N_{\varepsilon}}}]}}}\vbox{}}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}\mathsf{Eq}{i.A}(M,N);\allowbreak[k\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.\mathsf{Eq}{i.A_{\varepsilon}}(M_{\varepsilon},N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.\mathsf{Eq}{i.A{\varepsilon}}(M_{\varepsilon},N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.\mathsf{Eq}{i.A{\varepsilon}}(M_{\varepsilon},N_{\varepsilon})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.\mathsf{Eq}{i.A{\varepsilon}}(M_{\varepsilon},N_{\varepsilon})}}]=\mathsf{Eq}{i.\widetilde{A}[r^{\prime},i]}(\widetilde{M},\widetilde{N})\ \mathit{type}{l}}}}}}}
boolean type composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{U}{k}\mathbin{\downarrow^{r}{r^{\prime}}}\mathsf{bool};\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.\mathsf{bool}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.\mathsf{bool}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.\mathsf{bool}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.\mathsf{bool}}}]=\mathsf{bool}\ \mathit{type}_{l}}}}}}}
universe type composition
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\Psi\mid{\Gamma}\vdash{}\mathcal{U}{k^{\prime}}\mathbin{\downarrow^{r}{r^{\prime}}}\mathcal{U}{k};\allowbreak[i\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.\mathcal{U}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.\mathcal{U}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.\mathcal{U}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.\mathcal{U}{k}}}]=\mathcal{U}{k}\ \mathit{type}_{l}}}}}}}
Appendix B Algebraic model theory
We begin by giving a general formulation of a category with families (cwf) which has the structure of XTT. We work in a constructive set theory extended by Grothendieck’s Axiom of Universes: every set is contained in some Grothendieck Universe; this axiom induces a ordinal-indexed hierarchy of Grothendieck universes . Concretely, we will be using the chain of inclusions .
Let be the Cartesian cube category, the free strictly associative Cartesian category generated by an interval; concretely, its objects are dimension contexts , with morphisms given by substitutions between them. For the sake of clarity, we choose to work with the explicit syntactic presentation where is a list of named variables. Next, let be the augmented Cartesian cube category, which freely adjoins an initial object to . Using the initial object, we can see that has all equalizers, and that the evident functor is left exact (in other words, the new limits coincide with the old ones where they existed). We will write for the obvious weakening projection in .
B.1 Algebraic Cumulative Cwfs
We employ a variation on the notion of categories with families (cwfs) [30] suitable for modeling dependent type theory with a hierarchy of universes à la Russell which is cumulative in an algebraic sense (i.e. without subtyping).101010We emphasize that although the data of a cwf contains the data of a category, we are doing an algebraic model theory for type theory in which (e.g.) the initial object is determined up to isomorphism rather than up to equivalence.
B.1.1 Basic cwf structure: contexts, types, elements
Here, we develop the basic judgmental structure of a model of XTT, prior to requiring the existence of various connectives.
Category of contexts
An algebraic cumulative cwf begins with (the data of) a category of contexts , with morphisms interpreting substitutions. We require there to be a terminal context such that for any there is a unique substitution .
Notation B.1** (Yoneda isomorphism).**
For a presheaf on any category , we will use the following notations for the components of the Yoneda isomorphism: {diagram}
Cubical structure
We furthermore require our category of contexts be equipped with a split fibration which preserves the terminal object. To be precise, we equip with the data of a functor and a splitting for . It is important to note that we intend this structure to be preserved on the nose in homomorphisms of structured cwfs.
Notation B.2** (Split fibration).**
We impose the following notations for working with the split fibration , supplemented by Figure 3.
The fiber of over is written ; explicitly, this is the subcategory of whose objects are taken to by . 2. 2.
The splitting takes a dimension substitution and an object to a morphism such that . 3. 3.
Given a Cartesian morphism and an arrow , along with an arrow in the base category such that , the universal property of the Cartesian morphism guarantees a unique map which lies over , such that . 4. 4.
Given (not necessarily vertical) and disjoint from and , we write for the morphism where is the horizontal composite . 5. 5.
For a presheaf , we will write for the action of on .
Contexts and levels
is the category of contexts; but the judgments of XTT are also parameterized in a universe level. Therefore, we will need to work in presheaves not on but rather on . Recall that is the category of universe levels and is defined by .
Types and elements
Next, we require a presheaf in , yielding at each the set of types of level over ; we require each fiber to be -small in the ambient set theory. As a matter of notation, we write {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A for level restrictions, mirroring the concrete syntax of XTT.
Then, we require a dependent presheaf , writing for the fiber over ; in order to justify the rules which make elements of types and their level liftings definitionally interchangeable, we require that functorial action of maps (\Gamma,l,{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A)\rTo(\Gamma,k,A) in on the dependent presheaf must be strict identities. Consequently, we have \mathsf{El}_{\mathcal{C}}(\Gamma\vdash A)=\mathsf{El}_{\mathcal{C}}(\Gamma\vdash{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A), following [53].
By taking a dependent sum, it is possible to regard as an element of the slice ; this perspective will be profitable when defining the notion of a context comprehension.
Context comprehension
Writing for the evident projection of types from elements, we follow [32, 14] in requiring that be equipped with a choice of representable pullbacks along natural transformations out of representable objects (contexts): {diagram} We require the equation \Gamma.A=\Gamma.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A in the objects of .
Given a substitution and an element , we can form the extended substitution using the universal property of the pullback: {diagram}
Constraint comprehension
Let be the presheaf of dimensions, taking a context to the set of dimensions . Then, define , writing for the pair of ; we will follow the syntax of XTT in using to range over an element of .
Lemma B.3**.**
The split fibration forces the diagonal to be representable in the same sense as above; schematically: {diagram}
Proof B.4**.**
The context is obtained from the equalizer of in , using the splitting of the fibration : {diagram}
We can see that is indeed the pullback below: {diagram}
To see that the diagram commutes, we just verify that \color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\lfloor\normalcolor{\xi_{0}\circ\hat{\xi}=\xi_{0}\circ\hat{\xi}}\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\rfloor\normalcolor=\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\lfloor\normalcolor{\xi}\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\rfloor\normalcolor\circ\mathbf{y}(\hat{\xi}^{\dagger}\Gamma), which is the same as to say that ; but this is just the fact that is the equalizer of . Next, we check the universal property of the pullback; because limits in are formed pointwise (as in all presheaf categories), it suffices to check universality at representable objects only.
Fix and \mathbf{y}\Delta\rTo^{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\lfloor\normalcolor{s}\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\rfloor\normalcolor}\mathsf{Dim}_{\mathcal{C}} such that \delta\circ\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\lfloor\normalcolor{s}\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\rfloor\normalcolor=\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\lfloor\normalcolor{\xi}\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\rfloor\normalcolor\circ\mathbf{y}\gamma; we need to choose a unique morphism such that and \color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\lfloor\normalcolor{\xi_{0}}\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\rfloor\normalcolor\circ\mathbf{y}\eta=\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\lfloor\normalcolor{s}\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\rfloor\normalcolor. Unraveling the Yoneda paperwork, we have assumed that and we want to find such that the following triangles commute in and respectively:
[TABLE]
First, observe that because , the universal property of the equalizer guarantees a unique map with the same property: {diagram}
Using from above, we obtain from the universal property of the Cartesian lifting :
[TABLE]
We therefore see immediately that triangle (1) commutes; to see that triangle (2) commutes, we calculate: .
In order to model the collapse of the typing and equality judgments under the contraint in XTT’s syntax, we will require that the contexts and are initial in ; this implies initiality in the fibration , because the equalizer is the initial object in .
Notation B.5** (Constraint weakening).**
Because we will use it frequently, we will often write for the Cartesian lifting .
Notation B.6** (Constraint lifting).**
When , we write for .
We implicitly lift everything to do with dimensions and constraints into , by reindexing silently along the projection .
Boundary separation
To characterize models of XTT, we need to ensure that every type and every element is totally determined by its boundary with respect to the dimension context. A simple way to state this requirement is as a separation condition with respect to a particular coverage on the category of contexts . We define the coverage on by taking the constraint weakenings to constitute a covering family for each dimension :
[TABLE]
Lemma B.7**.**
The family of sets is a coverage on .
Proof B.8**.**
To see that is in fact a coverage, we fix and observe that any covering family can be pulled back to obtain a new covering family such that each composite factors through : {diagram}
This coverage lifts immediately along the projection to a coverage on ; because it will not result in ambiguity, we leave this lifting implicit.
Definition B.9** (Separation).**
Given a coverage on a category , a presheaf is -separated when, for any elements and covering family , if we have for each , then .
Definition B.10** (Boundary separation).**
We say that a cwf has boundary separation when the presheaves are -separated.
B.1.2 Kan operations: coercion and composition
Definition B.11** (Regular coercion structure).**
A cwf has regular coercion structure iff for every type over and dimensions and element , there is an element which has the following properties:
- •
Adjacency. If then .
- •
Regularity. If for some , then .
- •
Level restriction. The equation \mathbf{coe}_{i.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A}^{r\rightsquigarrow r^{\prime}}\,M=\mathbf{coe}_{i.A}^{r\rightsquigarrow r^{\prime}}\,M.
- •
Naturality. For we have .
Definition B.12** (Regular homogeneous composition structure).**
We say that has regular homogeneous composition structure iff, for each and and and for fresh such that , we have an element satisfying the following conditions:
- •
Adjacency. If then ; moreover, if , then .
- •
Regularity. If we have for some , then we have the equation .
- •
Naturality. For , we require the following naturality conditions:
[TABLE]
Notation B.13** (Heterogeneous composition).**
When a cwf has coercion and homogeneous composition, we write its heterogeneous composition using the following definitional extension:
[TABLE]
B.1.3 Closure under type-theoretic connectives
Definition B.14** (Booleans).**
A cwf has the booleans when it is equipped with the following structure:
- •
Formation. Types for all .
- •
Introduction. Elements and .
- •
Elimination. If and and and , an element \mathbf{if}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}C}}\left(M,N_{0},N_{1}\right)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash\langle\mathbf{id},M\rangle^{*}C).
- •
Computation. The following equations:
[TABLE]
- •
Level restriction. The following two equations:
[TABLE]
- •
Naturality. For , the following naturality equations:
[TABLE]
Definition B.15** (Dependent function types).**
A cwf has dependent function types when it is equipped with the following structure:
- •
Formation. For each type and family , a type .
- •
Introduction. For each , an element \mathbf{lam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash\boldsymbol{\Pi}(A,B)).
- •
Elimination. For each and an element \mathbf{app}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M,N)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash\langle\mathbf{id},N\rangle^{*}B).
- •
Computation. For each and , the equation \mathbf{app}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},\mathbf{lam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M),N)=\langle\mathbf{id},N\rangle^{*}M.
- •
Unicity. For each , the following equation:
[TABLE]
- •
Level restriction. The following equations:
[TABLE]
- •
Naturality. We have the following naturality conditions for each :
[TABLE]
- •
Coercion. When and and , we require the following equation:
[TABLE]
Definition B.16** (Dependent pair types).**
A cwf has dependent pair types when it is equipped with the following structure:
- •
Formation. For each type and family , a type .
- •
Introduction. For each and , an element \mathbf{pair}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M,N)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash\boldsymbol{\Sigma}(A,B)).
- •
Elimination. For each , elements \mathbf{fst}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash A) and \mathbf{snd}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash[\mathbf{id},\mathbf{fst}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M)]^{*}B).
- •
Computation. For and , the following equations:
[TABLE]
- •
Unicity. For , the equation M=\mathbf{pair}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},\mathbf{fst}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M),\mathbf{snd}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M)).
- •
Level restriction. The following equations:
[TABLE]
- •
Naturality. For substitutions the following naturality equations:
[TABLE]
- •
Coercion. When and and , we require the following equation:
[TABLE]
Definition B.17** (Dependent path types).**
A cwf has dependent path types when it is equipped with the following structure:
- •
Formation. For each type and elements , a type .
- •
Introduction. For each , an element \mathbf{plam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash\mathbf{Path}(i.A,(0/i)^{\ddagger}M,(1/i)^{\ddagger}M)).
- •
Elimination. For each and , an element \mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,r)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash(r/i)^{\ddagger}A) satisfying the equations \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,\epsilon)=N_{\epsilon}}}.
- •
Computation. For and , the equation \mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},\mathbf{plam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},i.M),r)=(r/i)^{\ddagger}M.
- •
Unicity. For , the equation M=\mathbf{plam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},j.\mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.\hat{\jmath}^{\ddagger}A},\hat{\jmath}^{\ddagger}M,j)).
- •
Level restriction. The following equations:
[TABLE]
- •
Naturality. For , the following naturality equations:
[TABLE]
- •
Coercion. When and and , we require the following equation:
[TABLE]
Definition B.18** (Dependent equality types).**
A cwf which has both boundary separation and dependent path types is said to have dependent equality types, and we accordingly write for .
Definition B.19** (Universes à la Russell).**
An algebraic cumulative cwf has universes à la Russell iff for all levels and context , there is a type such that . We additionally require the naturality equations and {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{l}^{m}}\mathbf{U}_{k}=\mathbf{U}_{k}.
Definition B.20** (Type-case).**
An algebraic cumulative cwf has type-case iff given the following data,
[TABLE]
we have an element \mathbf{tycase}_{k}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}C};X;M_{\Pi};M_{\Sigma};M_{\mathbf{Eq}};M_{\mathbf{bool}};M_{\mathbf{U}})\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash C) such that the following conditions hold:
- •
Computation.
[TABLE]
- •
Level restriction. The following equation:
[TABLE]
- •
Naturality. For , the following naturality condition:
[TABLE]
B.2 Syntactic model and initiality
The cwfs with all the structure described in Appendix B can be arranged into a category which has an initial object. This is because every piece of structure that we have defined in Appendix B is generalized algebraic in the sense of [20, 21]; even the universe structure can be seen to be generalized algebraic [53]. We conjecture (but do not prove) that the syntax of XTT can be used to construct a cwf (the Lindenbaum-Tarski algebra) which has the universal property of the initial object.
Syntactic presentation of augmented cubes
The syntactic contexts can be viewed as a particular syntactic presentation of the category of augmented Cartesian cubes, in which the equalizers are implemented formally by extending with equations.
Category of contexts
The well-typed term contexts can be organized (up to judgmental equality) into a category with morphisms with and , i.e. a well-typed substitution of terms in context for the variables from .
Types and terms
The presheaves of types are given by syntactic types up to judgmental equality, with action given by substitutions; well-typed terms taken up to judgmental equality generate the fibers of a natural transformation . The representability of is immediate from the fact that syntactic contexts can be extended by any type to yield . This context comes equipped with a projection and which implements the desired pullback square. The initiality of is ensured by the false constraint rule (see Section A.2.4).
Cubical judgmental structure
The functor takes a context to , and projects out the dimension component of a substitution . It is equipped with a splitting which, for the context , lifts to . Semantic boundary separation is obtained immediately from the boundary separation rules.
Connectives
We observe that our cwf also has dependent function, pair, equality, boolean and universe types given by the syntax.
Appendix C Cubical logical families and gluing
We fix an arbitrary structured cwf ; we will write for its objects. We will show how to build a cwf of cubical logical families over , called the “computability cwf”, which has some (but not all) of the structure of a model of XTT. Then, in Appendix D we will construct a genuine model of XTT by restricting to a closed universe.
C.1 The cubical nerve
We have a functor which takes a dimension context to -context with those dimensions but no term variables:
[TABLE]
This functor induces a nerve construction , taking to the presheaf . Intuitively, this is the presheaf of substitutions which are closed with respect to term variables, but open with respect to dimension variables; from the perspective of inside , these are the closed substitutions.
Abusing notation slightly, we now define the cubical set of “closed types” as . We furthermore define a dependent cubical set over , taking to ; internally, we will (abusively) write for the fiber of over . Given and , we abuse notation by writing .
Furthermore, we also define a dependent cubical set over , which internalizes the families of -types indexed in a given -type. Explicitly, we define a presheaf whose fibers are for each , and then exhibit the obvious projection .
Lemma C.1**.**
For each level , we have .
Proof C.2**.**
This follows from the fact that is a model of universes à la Russell. Calculate:
[TABLE]
C.2 Logical families by semantic gluing
By gluing the family fibration along the nerve functor , we acquire a category of cubical logical families, which we can used to prove canonicity for closed terms, instantiating with the initial structured cwf. Intuitively, the role of the gluing category is to “cut down” the morphisms in cubical sets to those which are definable in , allowing us to extract non-trivial theorems about using the very powerful tools afforded by the topos .
We will prefer a more explicit and type-theoretic presentation of the gluing category, but it is helpful for intuition to view it as a pullback of the fundamental fibration for along the cubical nerve functor: {diagram} Another view of the gluing category comes from the comma construction .
Diagrammatic construction of
Explicitly, an object in is a triple of a context , a cubical set , and a natural transformation ; a morphism is then a pair together with a commuting square: {diagram}
Type-theoretic construction of
Following [28], we will prefer a type-theoretic presentation of in terms of the hierarchy of Grothendieck universes , which lift directly into as in [36]. We found that this type-theoretic style scales more easily to the complex situations involved in the semantics of dependent type theory than the diagrammatic style above.
According to the type-theoretic presentation, an object of is a pair with and a family for some . A morphism is a pair with . To be precise, is a global element of the dependent function type in ; witnesses the fact that the syntactic substitution preserves the logical family.
There is a slight mismatch with the earlier diagrammatic intuition: the type-theoretic presentation only allows for families whose fibers fit into for some . Since we will work exclusively with the more restrictive type-theoretic presentation from now on this poses no technical challenges. Those who prefer the intuition provided by the diagrammatic presentation need merely restrict the pullback construction to certain suitably small cubical sets.
What’s it for?
is a proof-relevant logical predicate (“logical family”) on elements of which may have free dimension variables, but which commutes with all substitutions of those dimension variables. In other words, is a (cubical, proof-relevant) predicate on the elements of .
C.3 Cwf structure: types and elements
A glued type of level in context is a pair with and a global element of the cubical set . Level restrictions {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\overline{A} are inherited directly from : the family part of a glued type can remain unchanged because \llparenthesis{A}\rrparenthesis=\llparenthesis{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A}\rrparenthesis and . A glued element in context of type is a pair with and a global element of the cubical set .
We observe that the induced projection is representable by exhibiting the evident context comprehension for and , taking for its syntactic part, and using the following family for its semantic part:
[TABLE]
We clearly have that the restrictions \mathsf{El}_{\mathcal{C}^{\bullet}}(\overline{\Gamma}\vdash\overline{A})\rTo\mathsf{El}_{\mathcal{C}^{\bullet}}(\overline{\Gamma}\vdash{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\overline{A}) are identities, and \overline{\Gamma}.\overline{A}=\overline{\Gamma}.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\overline{A}. Therefore, forms an algebraic cumulative cwf; we will call it the “computability cwf”. The cubical structure is inherited from by precomposing with the fibration . We define the glued constraint comprehension by taking for the syntactic part, and defining its logical family as follows:
[TABLE]
This choice of realizers for the constraint comprehension ensures the initiality of inconsistent contexts in the gluing model.
Appendix D Canonicity for XTT: the computability model
We have not succeeded in closing the computability cwf from Appendix C under Kan universes à la Russell of Kan types; the essential difficulties are the separation property and the regular coercion structure. Therefore, this cwf does not have the structure of a model of XTT.
To rectify this, we will restrict to a smaller cwf , in which the types are generated inductively in a way reminiscent of the construction of closed universes in PER models [2]; the main difference is that, rather than using large induction-recursion (which has not been shown to exist in presheaf toposes), we model object universes in the cubical universe (an instance of small induction-recursion, which can be translated to constructs available in every presheaf topos [34, 49]).
Finally, using the universal property of the type structure of the restricted cwf, we will generate the coercion and composition structure recursively, obtaining a model of XTT.
D.1 Closed universe hierarchy
We will define a family internally to , together with . The former will serve as the computability predicate for a closed universe, and we will use the latter in order to define a family of types to decode the closed universe.
[TABLE]
We define an auxiliary family of types to capture family of type-codes:
[TABLE]
The assignment of computability families to type codes is as follows:
[TABLE]
Lemma D.1**.**
For any and with , we have \mathfrak{U}_{k}^{\bullet}{A}=\mathfrak{U}_{l}^{\bullet}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A.
Proof D.2**.**
We will show that \mathfrak{U}_{k}^{\bullet}{A}\subseteq\mathfrak{U}_{l}^{\bullet}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A; the other direction is symmetric. Fix ; we verify that \texttt{A}:\mathfrak{U}_{l}^{\bullet}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A as well, proceeding by induction.
Case.
[TABLE]
We have , and \mathbf{U}_{j}={\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\mathbf{U}_{j}.
Case.
[TABLE]
We likewise have , and \mathbf{bool}={\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\mathbf{bool}.
Case.
[TABLE]
To see that \texttt{pi}\left(\texttt{A};\texttt{B}\right):\mathfrak{U}_{l}^{\bullet}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\boldsymbol{\Pi}(A,B)}, by calculation, it suffices to show that \texttt{pi}\left(\texttt{A};\texttt{B}\right):\mathfrak{U}_{l}^{\bullet}{\boldsymbol{\Pi}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A,{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}B)}. By induction, we have \texttt{A}:\mathfrak{U}_{l}^{\bullet}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A; to verify that \texttt{B}:\mathfrak{F}_{l}[\texttt{A}]^{\bullet}{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}B, we fix and and need to check that \texttt{B}MM^{\bullet}:\mathfrak{U}_{l}^{\bullet}{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\left(\langle\mathbf{id},M\rangle^{*}B\right)}; but this follows from our second induction hypothesis and the fact that level restriction commutes with substitution.
The remaining cases are analogous.
Notation D.3**.**
We will write for the formula , the boundary of .
Lemma D.4**.**
Internally to , the following formulas are true:
[TABLE]
Proof D.5**.**
This follows from the fact that, as a model of XTT, has boundary separation; therefore, its types and elements are separated with respect to . This implies that all elements are completely defined by their boundaries. We prove this in detail for types only, and the case for terms is analogous. It suffices, using the Kripke-Joyal semantics of the topos , to fix and show that for all , , and , if then .
We will write for the equalizer of for each . Recalling that , by the -separation of (see Definition B.10), to show that it suffices to show that for each .
Unraveling the Kripke-Joyal paperwork of our assumption, we know that for all , if then . Instantiating this hypothesis with the equalizer , it remains only to check that . But we immediately have and by the property of the equalizer.
Definition D.6**.**
Given and , we say that A is elementwise separated (or just separated) iff the following formula holds internally to :
[TABLE]
We write for the above formula.
Definition D.7**.**
Given and , we say that A is typewise separated iff the following formula holds internally to :
[TABLE]
We write for the above formula.
Lemma D.8**.**
Internally to , the following formula is true:
[TABLE]
Proof D.9**.**
We begin by strong induction on ; then, we proceed by induction on A.
Case (dependent function type). Fixing and , we have to verify that is typewise and elementwise separated.
- (a)
Typewise separation. We need to show that for all , if , then . First we observe that there exist such that . This follows by inversion on B: if B is a pi our goal is immediate, otherwise we would have and in we have that giving a contradiction.
Therefore, we have some E and F such that . By inversion, we have . We need to show that and .
- i.
Instantiating our induction hypothesis for the typewise separation of C with E, we obtain from . 2. ii.
To see that , we fix and , and show that . Instantiating our induction hypothesis for the typewise separation of , we obtain from . 2. (b)
Elementwise separation Fixing and such that , we need to show that . We fix and , to verify that . Using our induction hypothesis for the elementwise separation of , we obtain from . 2. 2.
Case (dependent pair type). Fixing and , we have to verify that is typewise and elementwise separated.
- (a)
Typewise separation. This case is identical to the case for dependent function types. 2. (b)
Elementwise separation. Fixing and such that , we need to show that . It suffices to show that and .
- i.
From our induction hypothesis for the elementwise separation of C, we obtain from . 2. ii.
From our induction hypothesis for the elementwise separation of , we obtain from . 3. 3.
Case (equality type). Fixing and and , we have to verify that is typewise and elementwise separated.
- (a)
Typewise separation. We need to show that for all , if , then . By inversion, we observe that there exist and and such that . By inversion we have . We need to show that and .
- i.
To see that , we fix and verify that . Instantiating our induction hypothesis for the typewise separation of , we obtain from . 2. ii.
To see that , we instantiate our induction hypothesis for the elementwise separation of , obtaining from . 2. (b)
Elementwise separation. Fixing and such that , we need to show that ; fixing , we verify that . Using our induction hypothesis for the elementwise separation of , we obtain from . 4. 4.
Case (boolean type). We need to show that bool is typewise and elementwise separated.
- (a)
Typewise separation. We need to show that for all , if , then . But this is immediate by considering the restriction maps for bool. 2. (b)
Elementwise separation. Fixing and such that , we need to show that . We obtain our goal by case on , observing that the cross-cases and are impossible. 5. 5.
Case (universe). We need to show that is typewise and elementwise separated for .
- (a)
Typewise separation. We need to show that for all , if , then . But this is immediate by considering the restriction maps for . 2. (b)
Elementwise separation. Elementwise separation of follows from the typewise separation part of the outer induction hypothesis at .
D.2 The universe type and its decoding
Next, we define a hierarchy of closed universes à la Tarski . Note that these are not universes à la Russell in the sense of Definition B.19. For the syntactic part, take itself; then, we define the computability family using :
[TABLE]
We equip each type with regular coercion and homogeneous composition structure for these universes, by recursion on the type codes. For readability, we leave syntactic arguments like implicit.
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle r,r^{\prime}:\mathbb{I}}\hskip 10.00002pt\hbox{\hbox{\displaystyle\displaystyle\texttt{A}:\textstyle\prod_{i:\mathbb{I}}\mathfrak{U}{n}^{\bullet}A{i}}\hskip 10.00002pt\hbox{\hbox{\displaystyle\displaystyle M^{\bullet}:\texttt{A}r^{\circ}M}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle[i.\texttt{A}i]\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet}:\texttt{A}r^{\prime\circ}\mathopen{\big{(}}\mathbf{coe}{i.A_{i}}^{r\rightsquigarrow r^{\prime}},M\mathclose{\big{)}}}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle r,r^{\prime}:\mathbb{I}}\hskip 10.00002pt\hbox{\hbox{\displaystyle\displaystyle\texttt{A}:\mathfrak{U}{n}^{\bullet}{A}}\hskip 10.00002pt\hbox{\hbox{\displaystyle\displaystyle M^{\bullet}:\texttt{A}^{\circ}M}}}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\textstyle\mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{N{\varepsilon}^{\bullet}:\prod_{i:\mathbb{I}}(s=\varepsilon)\to\left{x:\texttt{A}^{\bullet}N_{i}\mid i=r\implies x=M^{\bullet}\right}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{N_{\varepsilon}^{\bullet}:\prod_{i:\mathbb{I}}(s=\varepsilon)\to\left{x:\texttt{A}^{\bullet}N_{i}\mid i=r\implies x=M^{\bullet}\right}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{N_{\varepsilon}^{\bullet}:\prod_{i:\mathbb{I}}(s=\varepsilon)\to\left{x:\texttt{A}^{\bullet}N_{i}\mid i=r\implies x=M^{\bullet}\right}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{N_{\varepsilon}^{\bullet}:\prod_{i:\mathbb{I}}(s=\varepsilon)\to\left{x:\texttt{A}^{\bullet}N_{i}\mid i=r\implies x=M^{\bullet}\right}}}}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{A}\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.N{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}]:\texttt{A}^{\circ}\left(\mathbf{hcom}{A}^{r\rightsquigarrow r^{\prime}},M;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.N{i}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.N_{i}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.N_{i}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.N_{i}}}]\right)}}}}}}
[TABLE]
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{M^{\bullet}}=[i.\texttt{A}{i}]\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\widetilde{N\varepsilon^{\bullet}}=\lambda i.,[i.\texttt{A}{i}]\mathbin{\downarrow^{i}{r^{\prime}}}N^{\bullet}{i}}}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle[i.\texttt{A}{i}]\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.N{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}]=\texttt{A}{r^{\prime}}\mathbin{\downarrow^{r}{r^{\prime}}}\widetilde{M^{\bullet}};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.N_{\varepsilon}^{\bullet}i}}]}}}}}}
\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{univ}{n}\mathbin{\downarrow^{r}{r^{\prime}}}\texttt{bool};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow_.\texttt{bool}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow_.\texttt{bool}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow_.\texttt{bool}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow_.\texttt{bool}}}]=\texttt{bool}}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{univ}{n}\mathbin{\downarrow^{r}{r^{\prime}}}\texttt{univ}{k};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow_.\texttt{univ}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow_.\texttt{univ}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow_.\texttt{univ}{k}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow_.\texttt{univ}{k}}}]=\texttt{univ}{k}}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{\texttt{A}}=\lambda i.,\texttt{univ}{n}\mathbin{\downarrow^{r}{i}}\texttt{A};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{\texttt{B}}=\lambda N^{\bullet}.,\texttt{univ}{n}\mathbin{\downarrow^{r}{r^{\prime}}}\texttt{B}\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{r}}N^{\bullet}\mathclose{\big{)}};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}]}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{univ}{n}\mathbin{\downarrow^{r}{r^{\prime}}}\texttt{pi}\left(\texttt{A};\texttt{B}\right);\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\texttt{pi}\left(\texttt{A'}i;\texttt{B'}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\texttt{pi}\left(\texttt{A'}i;\texttt{B'}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\texttt{pi}\left(\texttt{A'}i;\texttt{B'}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\texttt{pi}\left(\texttt{A'}i;\texttt{B'}i\right)}}]=\texttt{pi}\left(\widetilde{\texttt{A}}r^{\prime};\widetilde{\texttt{B}}\right)}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{\texttt{A}}=\lambda i.,\texttt{univ}{n}\mathbin{\downarrow^{r}{i}}\texttt{A};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\texttt{A'}i}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{\texttt{B}}=\lambda N^{\bullet}.,\texttt{univ}{n}\mathbin{\downarrow^{r}{r^{\prime}}}\texttt{B}\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{r}}N^{\bullet}\mathclose{\big{)}};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\texttt{B'}i\mathopen{\big{(}}[i.\widetilde{\texttt{A}}i]\mathbin{\downarrow^{r^{\prime}}{i}}N^{\bullet}\mathclose{\big{)}}}}]}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{univ}{n}\mathbin{\downarrow^{r}{r^{\prime}}}\texttt{sg}\left(\texttt{A};\texttt{B}\right);\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\texttt{sg}\left(\texttt{A'}i;\texttt{B'}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\texttt{sg}\left(\texttt{A'}i;\texttt{B'}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\texttt{sg}\left(\texttt{A'}i;\texttt{B'}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\texttt{sg}\left(\texttt{A'}i;\texttt{B'}i\right)}}]=\texttt{sg}\left(\widetilde{\texttt{A}}r^{\prime};\widetilde{\texttt{B}}\right)}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{\texttt{A}}=\lambda j,i.,\texttt{univ}{n}\mathbin{\downarrow^{r}{j}}\texttt{A}i;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.\texttt{A'}ji}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.\texttt{A'}ji}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.\texttt{A'}ji}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.\texttt{A'}ji}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{M}=[j.\widetilde{\texttt{A}}jr]\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.M^{\prime\bullet}j}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.M^{\prime\bullet}j}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.M^{\prime\bullet}j}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.M^{\prime\bullet}j}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{N}=[j.\widetilde{\texttt{A}}jr^{\prime}]\mathbin{\downarrow^{r}{r^{\prime}}}N^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow j.N^{\prime\bullet}j}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow j.N^{\prime\bullet}j}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow j.N^{\prime\bullet}j}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow j.N^{\prime\bullet}j}}]}}}\vbox{}}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{univ}{n}\mathbin{\downarrow^{r}{r^{\prime}}}\texttt{eq}\left(\texttt{A};M^{\bullet},N^{\bullet}\right);\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\texttt{eq}\left(\texttt{A}^{\prime}i;M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\texttt{eq}\left(\texttt{A}^{\prime}i;M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\texttt{eq}\left(\texttt{A}^{\prime}i;M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\texttt{eq}\left(\texttt{A}^{\prime}i;M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}]=\texttt{eq}\left(\widetilde{\texttt{A}}r^{\prime};\widetilde{M^{\bullet}},\widetilde{N^{\bullet}}\right)}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{bool}\mathbin{\downarrow^{r}{r^{\prime}}}\mathbf{inl}(\mathbf{refl});\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow_.\mathbf{inl}(\mathbf{refl})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow_.\mathbf{inl}(\mathbf{refl})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow_.\mathbf{inl}(\mathbf{refl})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow_.\mathbf{inl}(\mathbf{refl})}}]=\mathbf{inl}(\mathbf{refl})}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{bool}\mathbin{\downarrow^{r}{r^{\prime}}}\mathbf{inr}(\mathbf{refl});\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow_.\mathbf{inr}(\mathbf{refl})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow_.\mathbf{inr}(\mathbf{refl})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow_.\mathbf{inr}(\mathbf{refl})}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow_.\mathbf{inr}(\mathbf{refl})}}]=\mathbf{inr}(\mathbf{refl})}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{pi}\left(\texttt{A};\texttt{B}\right)\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}]=\lambda N^{\bullet}.,\texttt{B}N^{\bullet}\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet}N^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}iNN^{\bullet}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}iNN^{\bullet}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}iNN^{\bullet}}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}iNN^{\bullet}}}]}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{M^{\bullet}}=\lambda j.,\texttt{A}\mathbin{\downarrow^{r}{j}}M^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}]}}}\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle\widetilde{N^{\bullet}}=[i.\texttt{B}\mathopen{\big{(}}\widetilde{M^{\bullet}}i\mathclose{\big{)}}]\mathbin{\downarrow^{r}{r^{\prime}}}N^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow N^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow N^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow N^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow N^{\prime\bullet}i}}]}}}\vbox{}}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{sg}\left(\texttt{A};\texttt{B}\right)\mathbin{\downarrow^{r}{r^{\prime}}}\left(M^{\bullet},N^{\bullet}\right);\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.\left(M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.\left(M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.\left(M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.\left(M^{\prime\bullet}i,N^{\prime\bullet}i\right)}}]=\mathopen{\big{(}}\widetilde{M^{\bullet}}r^{\prime},\widetilde{N^{\bullet}}\mathclose{\big{)}}}}}}}} \displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{\displaystyle\displaystyle}}}\vbox{}}}\over\hbox{\vbox{\vbox{}\hbox{\hbox{\hbox{\displaystyle\displaystyle\texttt{eq}\left(\texttt{A};N{0}^{\bullet},N_{1}^{\bullet}\right)\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet};\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}i}}]=\lambda j.,\texttt{A}j\mathbin{\downarrow^{r}{r^{\prime}}}M^{\bullet}j;\allowbreak[s\ \mathsf{with}\ \mathchoice{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\displaystyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}ij}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\textstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}ij}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}ij}}{\overarrow@\arrowfill@\relbar\relbar\rightharpoonup\scriptscriptstyle{\varepsilon\hookrightarrow i.M^{\prime\bullet}ij}}]}}}}}}
Next, we show that every element determines a type . For the syntactic part, choose itself (which is possible because is a universe à la Russell in ). The computability family is given as follows:
[TABLE]
D.3 The closed-universe computability cwf
Now, we are equipped to build a new cwf , which we will show to be a model of XTT in Section D.4. Let the underlying category of be the same as ’s; we will choose new presheaves of types and elements, however.
[TABLE]
When and , we exhibit the level restriction by taking {\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}A for the syntactic part, and retaining for the semantic part, a move justified by the fact that the type codes are invariant under lifting (Lemma D.1).
Given and , we need to exhibit the context comprehension with the appropriate projection map and variable term . We choose the already-existing context comprehension inherited from ; the projection map and variable term are likewise inherited. From Lemma D.1 we also immediately obtain \mathsf{El}_{{\mathcal{C}}^{\star}}(\overline{\Gamma}\vdash\overline{A})=\mathsf{El}_{{\mathcal{C}}^{\star}}(\overline{\Gamma}\vdash{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\overline{A}) and \overline{\Gamma}.\overline{A}=\overline{\Gamma}.{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}{\Uparrow}_{k}^{l}}\overline{A}.
The projection lifts from to a fibration , because the underlying categories of and are identical. A cubical structure for is obtained from the composite .
D.4 A logical families model of XTT
In this section, we argue that the cwf has the structure of a model of XTT.
Construction D.10**.**
In preparation, we first will observe that internally to , we have the following operations for any and fresh :
[TABLE]
Fix and and , defining: {diagram} Naturality is just the associativity of composition. 2. 2.
Fix and and and . We need to construct some element of . Observing that constitute a map in , we see that our goal is in fact to transform into a map which lies over . This we obtain in the same way as before, this time using the composite fibration : {diagram} By analogy, we write this map as . ∎
Construction D.11**.**
When lies over and , we obtain a natural transformation ; fixing , we obtain: {diagram} We will write given and when working internally. ∎
Proposition D.12**.**
If , then .
Lemma D.13**.**
has regular coercion structure in the sense of Definition B.11.
Proof D.14**.**
Fixing over and dimensions and an element , we must construct an element which satisfies the adjacency, regularity and naturality equations. Taking for the syntactic part, we construct its realizer as follows:
[TABLE]
- •
Adjacency. If then . This holds already for the syntactic part, so it remains to see that our realizer preserves it; this is proved by induction on the graph of the realizer for coercion in Section D.2.
- •
Regularity. If for some , then . As above, we need only observe that the realizer exhibits regularity, which is evident by inspecting each of the clauses in Section D.2.
- •
Naturality. For we have . As above, this holds already of the syntactic part, so we need only to verify for each the following:
[TABLE]
The above follows from the naturality of Construction D.11.
Lemma D.15**.**
has regular homogeneous composition structure in the sense of Definition B.12.
Proof D.16**.**
Fix a type , dimensions , a cap and a tube for fresh such that . Choosing
[TABLE]
The adjacency and regularity conditions hold by induction on the graph of the realizer defined in Section D.2. The naturality condition lifts directly from as in Lemma D.13.
Lemma D.17**.**
has the boolean type, in the sense of Definition B.14.
Proof D.18**.**
- •
Formation. To exhibit , we choose itself for the syntactic part, and for its realizer we choose .
- •
Introduction. Choosing and for the syntactic parts, we exhibit realizers as follows:
[TABLE]
- •
Elimination. Fixing and and and , we choose \mathbf{if}_{{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}C}}\left(M,N_{0},N_{1}\right)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash\langle\mathbf{id},M\rangle^{*}){C} for the syntactic part, exhibiting its realizer as follows:
[TABLE]
- •
Computation, naturality. The satisfaction of the equational conditions is immediate.
Lemma D.19**.**
has dependent function types in the sense of Definition B.15.
Proof D.20**.**
- •
Formation. Fixing and a family , we must exhibit a type . Choosing for the syntactic part, we must exhibit a realizer for the type:
[TABLE]
- •
Introduction. Fixing , we must exhibit an element \mathbf{lam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\overline{A}},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\overline{B}},\overline{M})\in\mathsf{El}_{{\mathcal{C}}^{\star}}(\overline{\Gamma}\vdash\boldsymbol{\Pi}(\overline{A},\overline{B})). Choosing \mathbf{lam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M) for the syntactic part, we code its realizer as follows:
[TABLE]
- •
Elimination. Fixing and , we need an element \mathbf{app}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\overline{A}},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\overline{B}},\overline{M},\overline{N})\in\mathsf{El}_{{\mathcal{C}}^{\star}}(\overline{\Gamma}\vdash\langle\mathbf{id},\overline{N}\rangle^{*}\overline{B}). Choosing \mathbf{app}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M,N) for the syntactic part, we code its realizer:
[TABLE]
- •
Computation, unicity, naturality. These equations follow immediately from the fact that they hold of , and the corresponding properties of the dependent function types in .
- •
Coercion. Supposing and and , we need to verify the following equation:
[TABLE]
As this holds already of the syntactic part, we need only verify that it holds of the realizers (determined in Lemma D.13); but this is immediate by the definition of realizer for coercion at in Section D.2.
Lemma D.21**.**
has dependent pair types in the sense of Definition B.16.
Proof D.22**.**
- •
Formation. Fixing a type and a family , we choose for the syntactic part, and exhibit its realizer as follows:
[TABLE]
- •
Introduction. Fixing and , we choose \mathbf{pair}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M,N) for the syntactic part, coding its realizer as follows:
[TABLE]
- •
Elimination. Given , we choose \mathbf{fst}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M)\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash A) and \mathbf{snd}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}A},{\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}B},M) for the syntactic parts of the elimination forms, and give their realizers as follows:
[TABLE]
- •
Computation, unicity, naturality. These are all immediate from the fact that they hold in , and the fact that analogous principles hold for the dependent pair types of .
- •
Coercion. Analogous to Lemma D.19.
Lemma D.23**.**
has dependent path types in the sense of Definition B.17.
Proof D.24**.**
Here, we make use of Constructions D.10 and D.11.
- •
Formation. Fixing over and elements , we choose for the syntactic part, coding its realizer as follows:
[TABLE]
- •
Introduction. Given , we choose \mathbf{plam}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},i.M) for the syntactic part, and exhibit its realizer as follows:
[TABLE]
- •
Elimination. Fixing and , we choose \mathbf{papp}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}i.A},M,r) for the syntactic part; its realizer is analogous:
[TABLE]
- •
Computation, boundary, unicity and naturality. Immediate.
- •
Coercion. Analogous to Lemma D.19.
Lemma D.25**.**
has universes à la Russell in the sense of Definition B.19.
Proof D.26**.**
Fixing and levels , we need a type such that . For the syntactic part, we simply choose ; for its realizer:
[TABLE]
To see that the condition is met, we first observe that ; and moreover, . Therefore, it suffices to show that .
[TABLE]
Lemma D.27**.**
has boundary separation in the sense of Definition B.10.
Proof D.28**.**
Because has boundary separation, we need only to see that this property lifts to the realizers. Therefore, it suffices to show the following:
- •
Types. For all and , we must verify the following implication:
[TABLE]
Fixing and , it suffices to show:
[TABLE]
But this is equivalent to the following, which is obtained from the typewise separation of , a consequence of Lemma D.8:
[TABLE]
- •
Elements. For all and and , we must verify the following implication:
[TABLE]
This follows in an analogous way to the above from Lemma D.8, using the elementwise separation of .
Lemma D.29**.**
has type-case in the sense of Definition B.20.
Proof D.30**.**
We fix the following glued data:
[TABLE]
We need to exhibit an element \mathbf{tycase}_{k}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}\overline{C}};\overline{X};\overline{M_{\Pi}};\overline{M_{\Sigma}};\overline{M_{\mathbf{Eq}}};\overline{M_{\mathbf{bool}}};\overline{M_{\mathbf{U}}})\in\mathsf{El}_{{\mathcal{C}}^{\star}}(\overline{\Gamma}\vdash\overline{C}) with the specified computation and naturality rules. Inheriting the syntactic part from as \mathbf{tycase}_{k}({\color[rgb]{.44,.5,.565}\definecolor[named]{pgfstrokecolor}{rgb}{.44,.5,.565}C};X;M_{\Pi};M_{\Sigma};M_{\mathbf{Eq}};M_{\mathbf{bool}};M_{\mathbf{U}})\in\mathsf{El}_{\mathcal{C}}(\Gamma\vdash C), it remains to define its realizer:
[TABLE]
The required equations follow by calculation.
Corollary D.31**.**
is a model of XTT and moreover, is a homomorphism of XTT-algebras.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Andreas Abel, Thierry Coquand, and Peter Dybjer. On the algebraic foundation of proof assistants for intuitionistic type theory. In Jacques Garrigue and Manuel V. Hermenegildo, editors, Functional and Logic Programming , pages 3–13. Springer Berlin Heidelberg, 2008.
- 2[2] Stuart Frazier Allen. A non-type-theoretic semantics for type-theoretic language . Ph D thesis, 1987.
- 3[3] Thorsten Altenkirch. Extensional equality in intensional type theory. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR 00158) , pages 412–420, July 1999. doi:10.1109/LICS.1999.782636 . · doi ↗
- 4[4] Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) , volume 52 of Leibniz International Proceedings in Informatics (LIP Ics) , pages 6:1–6:16. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016. URL: http://drops.dagstuhl.de/opus/volltexte/2016/5972 , doi:10.4230/LIP Ics.FSCD.2016.6 . · doi ↗
- 5[5] Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL ’16, pages 18–29. ACM, 2016. URL: http://doi.acm.org/10.1145/2837614.2837638 , doi:10.1145/2837614.2837638 . · doi ↗
- 6[6] Thorsten Altenkirch and Conor Mc Bride. Towards Observational Type Theory, 2006. URL: www.strictlypositive.org/ott.pdf .
- 7[7] Thorsten Altenkirch, Conor Mc Bride, and Wouter Swierstra. Observational equality, now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification , PLPV ’07, pages 57–68. ACM, 2007.
- 8[8] Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. Syntax and models of cartesian cubical type theory. Preprint, February 2019. URL: https://github.com/dlicata 335/cart-cube .