# Cubical Type Theory: a constructive interpretation of the univalence axiom

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg

► To cite this version:

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. 21st International Conference on Types for Proofs and Programs, May 2015, Tallinn, Estonia. pp.262, 10.4230/LIPIcs.TYPES.2015.5 . hal-01378906v2

HAL Id: hal-01378906

https://inria.hal.science/hal-01378906v2

Submitted on 17 Apr 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom*

Cyril Cohen¹, Thierry Coquand², Simon Huber³, and Anders Mörtberg⁴

1 Inria Sophia Antipolis – Méditerranée,
2004 route des Lucioles, BP 93, 06902 Sophia Antipolis Cedex, France
cyril.cohen@inria.fr

2 Department of Computer Science and Engineering, University of Gothenburg,
412 96 Gothenburg, Sweden
thierry.coquand@cse.gu.se

3 Department of Computer Science and Engineering, University of Gothenburg,
412 96 Gothenburg, Sweden
simon.huber@cse.gu.se

4 School of Mathematics, Institute for Advanced Study,
1 Einstein Drive, Princeton, NJ 08540, USA
amortberg@math.ias.edu

## Abstract

This paper presents a type theory in which it is possible to directly manipulate *n*-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky’s univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

**1998 ACM Subject Classification** F.3.2 Logics and Meanings of Programs: Semantics of Programming Languages, F.4.1 Mathematical Logic and Formal Languages: Mathematical Logic

**Keywords and phrases** univalence axiom, dependent type theory, cubical sets

**Digital Object Identifier** 10.4230/LIPIcs.TYPES.2015.5

## 1 Introduction

This work is a continuation of the program started in [6, 13] to provide a constructive justification of Voevodsky’s univalence axiom [27]. This axiom allows many improvements for the formalization of mathematics in type theory: function extensionality, identification of isomorphic structures, etc. In order to preserve the good computational properties of type theory it is crucial that postulated constants have a computational interpretation. Like in [6, 13, 22] our work is based on a nominal extension of λ-calculus, using *names* to represent formally elements of the unit interval [0, 1]. This paper presents two main contributions.

<figure><img src="image_2.png" /></figure>

<footnote>* This material is based upon work supported by the National Science Foundation under agreement No. DMS-1128155. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.</footnote>
## 5:2 Cubical Type Theory

The first one is a refinement of the semantics presented in [6, 13]. We add new operations on names corresponding to the fact that the interval [0, 1] is canonically a de Morgan algebra [3]. This allows us to significantly simplify our semantical justifications. In the previous work, we noticed that it is crucial for the semantics of higher inductive types [26] to have a “diagonal” operation. By adding this operation we can provide a semantical justification of some higher inductive types and we give two examples (the spheres and propositional truncation). Another shortcoming of the previous work was that using path types as equality types did not provide a justification of the computation rule of the Martin-Löf identity type [19] as a judgmental equality. This problem has been solved by Andrew Swan [25], in the framework of [6, 13, 22], who showed that we can define a new type, equivalent to, but not judgmentally equal to the path type. This has a simple definition in the present framework.

The second contribution is the design of a type system<fnref n="1" /> inspired by this semantics which extends Martin-Löf type theory [20, 19]. We add two new operations on contexts: addition of new names representing dimensions and a restriction operation. Using these we can define a notion of extensibility which generalizes the notion of being connected by a path, and then a Kan composition operation that expresses that being extensible is preserved along paths. We also define a new operation on types which expresses that this notion of extensibility is preserved by equivalences. The axiom of univalence, and composition for the universe, are then both expressible using this new operation.

The paper is organized as follows. The first part, Sections 2 to 7, presents the type system. The second part, Section 8, provides its semantics in cubical sets. Finally, in Section 9, we present two possible extensions: the addition of an identity type, and two examples of higher inductive types.

# 2 Basic Type Theory

In this section we introduce the version of dependent type theory on which the rest of the paper is based. This presentation is standard, but included for completeness. The type theory that we consider has a type of natural numbers, but no universes (we consider the addition of universes in Section 7). It also has $\beta$ and $\eta$-conversion for dependent functions and surjective pairing for dependent pairs.

The syntax of contexts, terms and types is specified by:

<table><tr><td>Γ, Δ</td><td>::=</td><td>() | Γ, x : A</td><td>Contexts</td></tr><tr><td>t, u, A, B</td><td>::=</td><td>x | λx : A. t | t u | (x : A) → B<br>| (t, u) | t.1 | t.2 | (x : A) × B<br>| 0 | s u | natrec t u | N</td><td>Π-types<br>Σ-types<br>Natural numbers</td></tr></table>

We write $A \to B$ for the non-dependent function space and $A \times B$ for the type of non-dependent pairs. Terms and types are considered up to $\alpha$-equivalence of bound variables. Substitutions, written $\sigma = (x_1/u_1, \dots, x_n/u_n)$, are defined to act on expressions as usual, i.e., simultaneously replacing $x_i$ by $u_i$, renaming bound variables whenever necessary. The inference rules of this system are presented in Figure 1 where in the $\eta$-rule for $\Pi$- and $\Sigma$-types we omitted the premises that $t$ and $u$ should have the respective type.

<footnote n="1">¹ We have implemented a type-checker for this system in HASKELL, which is available at: https://github.com/mortberg/cubicaltt</footnote>
Well-formed contexts, $\Gamma \vdash$ (The condition $x \notin \text{dom}(\Gamma)$ means that $x$ is not declared in $\Gamma$)

$$ \underline{\quad} \quad \underline{\Gamma \vdash A \quad (x \notin \text{dom}(\Gamma))} $$

Well-formed types, $\Gamma \vdash A$

$$ \frac{\Gamma, x : A \vdash B}{\Gamma \vdash (x : A) \to B} $$

$$ \frac{\Gamma, x : A \vdash B}{\Gamma \vdash (x : A) \times B} $$

$$ \frac{\Gamma \vdash \quad \Gamma \vdash N}{\Gamma \vdash N} $$

Well-typed terms, $\Gamma \vdash t : A$

$$ \frac{\Gamma \vdash t : A \quad \Gamma \vdash A = B}{\Gamma \vdash t : B} $$

$$ \frac{\Gamma, x : A \vdash t : B}{\Gamma \vdash \lambda x : A. t : (x : A) \to B} $$

$$ \frac{\Gamma \vdash \quad (x : A \in \Gamma)}{\Gamma \vdash x : A} $$

$$ \frac{\Gamma \vdash t : (x : A) \to B \quad \Gamma \vdash u : A}{\Gamma \vdash t u : B(x/u)} $$

$$ \frac{\Gamma \vdash t : (x : A) \times B}{\Gamma \vdash t.1 : A} $$

$$ \frac{\Gamma \vdash t : (x : A) \times B}{\Gamma \vdash t.2 : B(x/t.1)} $$

$$ \frac{\Gamma, x : A \vdash B \quad \Gamma \vdash t : A \quad \Gamma \vdash u : B(x/t)}{\Gamma \vdash (t, u) : (x : A) \times B} $$

$$ \frac{\Gamma \vdash \quad \Gamma \vdash 0 : N}{\Gamma \vdash N} $$

$$ \frac{\Gamma \vdash n : N \quad \Gamma \vdash s n : N}{\Gamma \vdash s n : N} $$

$$ \frac{\Gamma, x : N \vdash P \quad \Gamma \vdash a : P(x/0) \quad \Gamma \vdash b : (n : N) \to P(x/n) \to P(x/s n)}{\Gamma \vdash \text{natrec } a b : (x : N) \to P} $$

Type equality, $\Gamma \vdash A = B$ (Congruence and equivalence rules which are omitted)

Term equality, $\Gamma \vdash a = b : A$ (Congruence and equivalence rules are omitted)

$$ \frac{\Gamma \vdash t = u : A \quad \Gamma \vdash A = B}{\Gamma \vdash t = u : B} $$

$$ \frac{\Gamma, x : A \vdash t : B \quad \Gamma \vdash u : A}{\Gamma \vdash (\lambda x : A. t) u = t(x/u) : B(x/u)} $$

$$ \frac{\Gamma, x : A \vdash t x = u x : B}{\Gamma \vdash t = u : (x : A) \to B} $$

$$ \frac{\Gamma, x : A \vdash B \quad \Gamma \vdash t : A \quad \Gamma \vdash u : B(x/t)}{\Gamma \vdash (t, u).1 = t : A} $$

$$ \frac{\Gamma, x : A \vdash B \quad \Gamma \vdash t : A \quad \Gamma \vdash u : B(x/t)}{\Gamma \vdash (t, u).2 = u : B(x/t)} $$

$$ \frac{\Gamma, x : A \vdash B \quad \Gamma \vdash t.1 = u.1 : A \quad \Gamma \vdash t.2 = u.2 : B(x/t.1)}{\Gamma \vdash t = u : (x : A) \times B} $$

$$ \frac{\Gamma, x : N \vdash P \quad \Gamma \vdash a : P(x/0) \quad \Gamma \vdash b : (n : N) \to P(x/n) \to P(x/s n)}{\Gamma \vdash \text{natrec } a b 0 : a : P(x/0)} $$

$$ \frac{\Gamma, x : N \vdash P \quad \Gamma \vdash a : P(x/0) \quad \Gamma \vdash b : (n : N) \to P(x/n) \to P(x/s n)}{\Gamma \vdash n : N} $$

<caption>Figure 1 Inference rules of the basic type theory.</caption>
5:4 Cubical Type Theory

We define $\Delta \vdash \sigma : \Gamma$ by induction on $\Gamma$. Given $\Delta \vdash$ we have $\Delta \vdash () : ()$ (the empty substitution), and $\Delta \vdash (\sigma, x/u) : \Gamma, x : A$ if $\Delta \vdash \sigma : \Gamma$ and $\Delta \vdash u : A\sigma$.

We write $J$ for an arbitrary judgment and, as usual, we consider also *hypothetical judgments* $\Gamma \vdash J$ in a *context* $\Gamma$.

The following lemma will be valid for all extensions of type theory we consider below.

**► Lemma 1.** *Substitution is admissible:*

$$ \frac{\Gamma \vdash J \quad \Delta \vdash \sigma : \Gamma \\ \Delta \vdash J\sigma}{\quad} $$

*In particular, weakening is admissible, i.e., a judgment valid in a context stays valid in any extension of this context.*

3 Path Types

As in [6, 22] we assume that we are given a discrete infinite set of names (representing directions) $i, j, k, \dots$. We define $\mathbb{I}$ to be the free de Morgan algebra [3] on this set of names. This means that $\mathbb{I}$ is a bounded distributive lattice with top element 1 and bottom element 0 with an involution $1 - r$ satisfying:

$$ 1 - 0 = 11 - 1 = 01 - (r \lor s) = (1 - r) \land (1 - s)1 - (r \land s) = (1 - r) \lor (1 - s) $$

The elements of $\mathbb{I}$ can hence be described by the following grammar:

$$ r, s ::= 0 \mid 1 \mid i \mid 1 - r \mid r \land s \mid r \lor s $$

The set $\mathbb{I}$ also has decidable equality, and as a distributive lattice, it can be described as the free distributive lattice generated by symbols $i$ and $1-i$ [3]. As in [6], the elements in $\mathbb{I}$ can be thought as formal representations of elements in $[0, 1]$, with $r \land s$ representing $min(r, s)$ and $r \lor s$ representing $max(r, s)$. With this in mind it is clear that $(1 - r) \land r \neq 0$ and $(1 - r) \lor r \neq 1$ in general.

**► Remark.** We could instead also use a so-called Kleene algebra [15], i.e., a de Morgan algebra satisfying in addition $r \land (1 - r) \le s \lor (1 - s)$. The free Kleene algebra on the set of names can be described as above but by additionally imposing the equations $i \land (1 - i) \le j \lor (1 - j)$ on the generators; this still has a decidable equality. Note that $[0, 1]$ with the operations described above is a Kleene algebra. With this added condition, $r = s$ if, and only if, their interpretations in $[0, 1]$ are equal. A consequence of using a Kleene algebra instead would be that more terms would be judgmentally equal in the type theory.

3.1 Syntax and Inference Rules

Contexts can now be extended with name declarations:

$$ \Gamma, \Delta ::= \dots | \Gamma, i : \mathbb{I} $$

together with the context rule:

$$ \frac{\Gamma \vdash}{\Gamma, i : \mathbb{I} \vdash} (i \notin \mathrm{dom}(\Gamma)) $$

A judgment of the form $\Gamma \vdash r : \mathbb{I}$ means that $\Gamma \vdash$ and $r$ in $\mathbb{I}$ depends only on the names declared in $\Gamma$. The judgment $\Gamma \vdash r = s : \mathbb{I}$ means that $r$ and $s$ are equal as elements of $\mathbb{I}$,
$$ \frac{\Gamma \vdash A \qquad \Gamma \vdash t : A \qquad \Gamma \vdash u : A}{\Gamma \vdash \text{Path } A t u} $$

$$ \frac{\Gamma \vdash A \qquad \Gamma, i : \mathbb{I} \vdash t : A}{\Gamma \vdash \langle i \rangle t : \text{Path } A t(i0) t(i1)} $$

$$ \frac{\Gamma \vdash t : \text{Path } A u_0 u_1 \qquad \Gamma \vdash r : \mathbb{I}}{\Gamma \vdash t r : A} $$

$$ \frac{\Gamma \vdash A \qquad \Gamma, i : \mathbb{I} \vdash t : A \qquad \Gamma \vdash r : \mathbb{I}}{\Gamma \vdash (\langle i \rangle t) r = t(i/r) : A} $$

$$ \frac{\Gamma, i : \mathbb{I} \vdash t i = u i : A}{\Gamma \vdash t = u : \text{Path } A u_0 u_1} $$

$$ \frac{\Gamma \vdash t : \text{Path } A u_0 u_1}{\Gamma \vdash t 0 = u_0 : A} $$

$$ \frac{\Gamma \vdash t : \text{Path } A u_0 u_1}{\Gamma \vdash t 1 = u_1 : A} $$

<caption>Figure 2 Inference rules for path types.</caption>

$\Gamma \vdash r : \mathbb{I}$, and $\Gamma \vdash s : \mathbb{I}$. Note, that judgmental equality for $\mathbb{I}$ will be re-defined once we introduce restricted contexts in Section 4.

The extension to the syntax of basic dependent type theory is:

$$ t, u, A, B ::= \dots \\ | \quad \text{Path } A t u \mid \langle i \rangle t \mid t r \qquad \text{Path types} $$

Path abstraction, $\langle i \rangle t$, binds the name $i$ in $t$, and path application, $t r$, applies a term $t$ to an element $r : \mathbb{I}$. This is similar to the notion of name-abstraction in nominal sets [21].

The substitution operation now has to be extended to substitutions of the form $(i/r)$. There are special substitutions of the form $(i/0)$ and $(i/1)$ corresponding to taking faces of an $n$-dimensional cube, we write these simply as $(i0)$ and $(i1)$.

The inference rules for path types are presented in Figure 2 where again in the $\eta$-rule we omitted that $t$ and $u$ should be appropriately typed.

We define $1_a : \text{Path } A a a$ as $1_a = \langle i \rangle a$, which corresponds to a proof of reflexivity.

The intuition is that a type in a context with $n$ names corresponds to an $n$-dimensional cube:

<table><thead><tr><th></th><th></th></tr></thead><tbody><tr><td>$() \vdash A$</td><td>$\bullet A$</td></tr><tr><td>$i : \mathbb{I} \vdash A$</td><td>$A(i0) \xrightarrow{A} A(i1)$</td></tr><tr><td>$i : \mathbb{I}, j : \mathbb{I} \vdash A$</td><td>$A(i0)(j1) \xrightarrow{A(j1)} A(i1)(j1)$<br>$\uparrow \quad \uparrow$<br>$A(i0) \quad A(i1)$<br>$A(i0)(j0) \xrightarrow{A(j0)} A(i1)(j0)$</td></tr><tr><td>$\vdots$</td><td>$\vdots$</td></tr></tbody></table>

Note that $A(i0)(j0) = A(j0)(i0)$. The substitution $(i/j)$ corresponds to renaming a dimension, while $(i/1 - i)$ corresponds to the inversion of a path. If we have $i : \mathbb{I} \vdash p$ with $p(i0) = a$ and $p(i1) = b$ then it can be seen as a line

$$ a \xrightarrow{p} b $$

in direction $i$, then:

$$ b \xrightarrow{p(i/1 - i)} a $$
5:6 Cubical Type Theory

The substitutions $(i/i \wedge j)$ and $(i/i \vee j)$ correspond to special kinds of degeneracies called connections [7]. The connections $p(i/i \wedge j)$ and $p(i/i \vee j)$ can be drawn as the squares:

<figure><img src="image_3.png" /></figure>

where, for instance, the right-hand side of the left square is computed as

$$p(i/i \wedge j)(i1) = p(i/1 \wedge j) = p(i/j)$$

and the bottom and left-hand sides are degenerate.

3.2 Examples

Representing equalities using path types allows novel definitions of many standard operations on identity types that are usually proved by identity elimination. For instance, the fact that the images of two equal elements are equal can be defined as:

$$\frac{\Gamma \vdash a : A \quad \Gamma \vdash b : A \quad \Gamma \vdash f : A \to B \quad \Gamma \vdash p : \text{Path } A a b}{\Gamma \vdash \langle i \rangle f (p i) : \text{Path } B (f a) (f b)}$$

This operation satisfies some judgmental equalities that do not hold judgmentally when the identity type is defined as an inductive family (see Section 7.2 of [6] for details).

We can also define new operations, for instance, function extensionality for path types can be proved as:

$$\frac{\Gamma \vdash f : (x : A) \to B \quad \Gamma \vdash g : (x : A) \to B \quad \Gamma \vdash p : (x : A) \to \text{Path } B (f x) (g x)}{\Gamma \vdash \langle i \rangle \lambda x : A. p x i : \text{Path } ((x : A) \to B) f g}$$

To see that this is correct we check that the term has the correct faces, for instance:

$$\langle i \rangle \lambda x : A. p x i = 0 \qquad \lambda x : A. p x 0 = \lambda x : A. f x = f$$

We can also justify the fact that singletons are contractible, that is, that any element in $(x : A) \times (\text{Path } A a x)$ is equal to $(a, 1_a)$:

$$\frac{\Gamma \vdash p : \text{Path } A a b}{\Gamma \vdash \langle i \rangle (p i, \langle j \rangle p (i \wedge j)) : \text{Path } ((x : A) \times (\text{Path } A a x)) (a, 1_a) (b, p)}$$

As in the previous work [6, 13] we need to add composition operations, defined by induction on the type, in order to justify the elimination principle for paths.

4 Systems, Composition, and Transport

In this section we define the operation of context restriction which will allow us to describe new geometrical shapes corresponding to “sub-polyhedra” of a cube. Using this we can define the composition operation. From this operation we will also be able to define the transport operation and the elimination principle for Path types.
## 4.1 The Face Lattice

The face lattice, $\mathbb{F}$, is the distributive lattice generated by symbols $(i = 0)$ and $(i = 1)$ with the relation $(i = 0) \wedge (i = 1) = 0_{\mathbb{F}}$. The elements of the face lattice, called face formulas, can be described by the grammar

$$ \varphi, \psi ::= 0_{\mathbb{F}} | 1_{\mathbb{F}} | (i = 0) | (i = 1) | \varphi \wedge \psi | \varphi \vee \psi $$

There is a canonical lattice map $\mathbb{I} \to \mathbb{F}$ sending $i$ to $(i = 1)$ and $1 - i$ to $(i = 0)$. We write $(r = 1)$ for the image of $r : \mathbb{I}$ in $\mathbb{F}$ and we write $(r = 0)$ for $(1 - r = 1)$. We have $(r = 1) \wedge (r = 0) = 0_{\mathbb{F}}$ and we define the lattice map $\mathbb{F} \to \mathbb{F}$, $\psi \mapsto \psi(i/r)$ sending $(i = 1)$ to $(r = 1)$ and $(i = 0)$ to $(r = 0)$.

Any element of $\mathbb{F}$ is the join of the irreducible elements below it. An irreducible element of this lattice is a face, i.e., a conjunction of elements of the form $(i = 0)$ and $(j = 1)$. This provides a disjunctive normal form for face formulas, and it follows from this that the equality on $\mathbb{F}$ is decidable.

Geometrically, the face formulas describe “sub-polyhedra” of a cube. For instance, the element $(i = 0) \vee (j = 1)$ can be seen as the union of two faces of the square in directions $j$ and $i$. If $I$ is a finite set of names, we define the boundary of $I$ as the element $\partial_I$ of $\mathbb{F}$ which is the disjunction of all $(i = 0) \vee (i = 1)$ for $i$ in $I$. It is the greatest element depending at most on elements in $I$ which is $< 1_{\mathbb{F}}$.

We write $\Gamma \vdash \psi : \mathbb{F}$ to mean that $\psi$ is a face formula using only the names declared in $\Gamma$. We introduce then the new restriction operation on contexts:

$$ \Gamma, \Delta ::= \dots | \Gamma, \varphi $$

together with the rule:

$$ \frac{\Gamma \vdash \varphi : \mathbb{F}}{\Gamma, \varphi \vdash} $$

This allows us to describe new geometrical shapes: as we have seen above, a type in a context $\Gamma = i : \mathbb{I}, j : \mathbb{I}$ can be thought of as a square, and a type in the restricted context $\Gamma, \varphi$ will then represent a compatible union of faces of this square. This can be illustrated by:

<table><tr><td>$i : \mathbb{I}, (i = 0) \vee (i = 1) \vdash A$</td><td>$A(i0) \bullet \quad A(i1) \bullet$</td></tr><tr><td>$i : \mathbb{I}, j : \mathbb{I}, (i = 0) \vee (j = 1) \vdash A$</td><td>$A(i0)(j1) \xrightarrow{A(j1)} A(i1)(j1)$<br>$\begin{array}{c} \uparrow \\ A(i0) \\ \downarrow \\ A(i0)(j0) \end{array}$</td></tr><tr><td>$i : \mathbb{I}, j : \mathbb{I}, (i = 0) \vee (i = 1) \vee (j = 0) \vdash A$</td><td>$A(i0)(j1) \quad A(i1)(j1)$<br>$\begin{array}{c} \uparrow \\ A(i0) \\ \downarrow \\ A(i0)(j0) \end{array} \xrightarrow{A(j0)} A(i1)(j0)$</td></tr></table>

There is a canonical map from the lattice $\mathbb{F}$ to the congruence lattice of $\mathbb{I}$, which is distributive [3], sending $(i = 1)$ to the congruence identifying $i$ with 1 (and $1 - i$ with 0) and sending
5:8 Cubical Type Theory

(i = 0) to the congruence identifying i with 0 (and 1 − i with 1). In this way, any element
ψ of F defines a congruence r = s (mod. ψ) on I.

This congruence can be described as a substitution if ψ is irreducible; for instance, if
ψ is (i = 0) ∧ (j = 1) then r = s (mod. ψ) is equivalent to r(i0)(j1) = s(i0)(j1). The
congruence associated to ψ = ϕ₀ ∨ ϕ₁ is the meet of the congruences associated to ϕ₀ and
ϕ₁ respectively, so that we have, e.g., i = 1 − j (mod. ψ) if ϕ₀ = (i = 0) ∧ (j = 1) and
ϕ₁ = (i = 1) ∧ (j = 0).

To any context Γ we can associate recursively a congruence on I, the congruence on
Γ, ψ being the join of the congruence defined by Γ and the congruence defined by ψ. The
congruence defined by () is equality in I, and an extension x : A or i : I does not change the
congruence. The judgment Γ ⊢ r = s : I then means that r = s (mod. Γ), Γ ⊢ r : I, and
Γ ⊢ s : I.

In the case where Γ does not use the restriction operation, this judgment means r = s
in I. If i is declared in Γ, then Γ, (i = 0) ⊢ r = s : I is equivalent to Γ ⊢ r(i0) = s(i0) : I.
Similarly any context Γ defines a congruence on F with Γ, ψ ⊢ ϕ₀ = ϕ₁ : F being equivalent
to Γ ⊢ ψ ∧ ϕ₀ = ψ ∧ ϕ₁ : F.

As explained above, the elements of I can be seen as formal representations of elements
in the interval [0, 1]. The elements of F can then be seen as formulas on elements of [0, 1].
We have a simple form of quantifier elimination on F: given a name i, we define ∀i: F → F
as the lattice morphism sending (i = 0) and (i = 1) to 0F, and being the identity on all the
other generators. If ψ is independent of i, we have ψ ≤ ϕ if, and only if, ψ ≤ ∀i.ϕ. For
example, if ϕ is (i = 0) ∨ ((i = 1) ∧ (j = 0)) ∨ (j = 1), then ∀i.ϕ is (j = 1). This operation
will play a crucial role in Section 6.2 for the definition of composition of glueing.

Since F is not a Boolean algebra, we don't have in general $\varphi = (\varphi \wedge (i = 0)) \vee (\varphi \wedge (i = 1))$,
but we always have the following decomposition:

► **Lemma 2.** For any element $\varphi$ of $\mathbb{F}$ and any name $i$ we have

$$
\varphi = (\forall i.\varphi) \lor (\varphi \land (i = 0)) \lor (\varphi \land (i = 1))
$$

We also have $\varphi \wedge (i = 0) \le \varphi(i0)$ and $\varphi \wedge (i = 1) \le \varphi(i1)$.

4.2 Syntax and Inference Rules for Systems

Systems allow to introduce “sub-polyhedra” as compatible unions of cubes. The extension
to the syntax of dependent type theory with path types is:

$$
t, u, A, B ::= \dots \\
\qquad \mid [ \varphi_1 t_1, \dots, \varphi_n t_n ] \qquad \text{Systems}
$$

We allow $n = 0$ and get the empty system $[ ]$. As explained above, a context now corresponds
in general to the union of sub-faces of a cube. In Figure 3 we provide operations for combining
compatible systems of types and elements, the side condition for these rules is that $\Gamma \vdash$
$\varphi_1 \lor \dots \lor \varphi_n = 1_F : \mathbb{F}$. This condition requires $\Gamma$ to be sufficiently restricted: for example
$\Delta, (i = 0) \lor (i = 1) \vdash (i = 0) \lor (i = 1) = 1_F$. The first rule introduces systems of types,
each defined on one $\varphi_l$ and requiring the types to agree whenever they overlap; the second
rule is the analogous rule for terms. The last two rules make sure that systems have the
correct faces. The third inference rule says that any judgment which is valid locally at
each $\varphi_l$ is valid; note that in particular $n = 0$ is allowed (then the side condition becomes
$\Gamma \vdash 0_F = 1_F : \mathbb{F}$).
$$ \frac{\Gamma, \varphi_1 \vdash A_1 \quad \dots \quad \Gamma, \varphi_n \vdash A_n \quad \Gamma, \varphi_i \wedge \varphi_j \vdash A_i = A_j \quad (1 \le i, j \le n)}{\Gamma \vdash [\varphi_1 A_1, \dots, \varphi_n A_n]} $$

$$ \frac{\Gamma \vdash A}{\Gamma, \varphi_1 \vdash t_1 : A \quad \dots \quad \Gamma, \varphi_n \vdash t_n : A \quad \Gamma, \varphi_i \wedge \varphi_j \vdash t_i = t_j : A \quad (1 \le i, j \le n)} \quad \Gamma \vdash [\varphi_1 t_1, \dots, \varphi_n t_n] : A $$

$$ \frac{\Gamma, \varphi_1 \vdash J \quad \dots \quad \Gamma, \varphi_n \vdash J}{\Gamma \vdash J} \qquad \frac{\Gamma \vdash [\varphi_1 A_1, \dots, \varphi_n A_n]}{\Gamma \vdash [\varphi_1 A_1, \dots, \varphi_n A_n]} = A_i $$

$$ \frac{\Gamma \vdash [\varphi_1 t_1, \dots, \varphi_n t_n] : A \quad \Gamma \vdash \varphi_i = 1_F : F}{\Gamma \vdash [\varphi_1 t_1, \dots, \varphi_n t_n] = t_i : A} $$

**Figure 3** Inference rules for systems with side condition $\Gamma \vdash \varphi_1 \lor \dots \lor \varphi_n = 1_F : F$.

Note that when $n = 0$ the second of the above rules should be read as: if $\Gamma \vdash 0_F = 1_F : F$ and $\Gamma \vdash A$, then $\Gamma \vdash [] : A$.

We extend the definition of the substitution judgment by $\Delta \vdash \sigma : \Gamma, \varphi$ if $\Delta \vdash \sigma : \Gamma, \Gamma \vdash \varphi : F$, and $\Delta \vdash \varphi\sigma = 1_F : F$.

If $\Gamma, \varphi \vdash u : A$, then $\Gamma \vdash a : A[\varphi \mapsto u]$ is an abbreviation for $\Gamma \vdash a : A$ and $\Gamma, \varphi \vdash a = u : A$. In this case, we see this element $a$ as a witness that the partial element $u$, defined on the “extent” $\varphi$ (using the terminology from [10]), is *extensible*. More generally, we write $\Gamma \vdash a : A[\varphi_1 \mapsto u_1, \dots, \varphi_k \mapsto u_k]$ for $\Gamma \vdash a : A$ and $\Gamma, \varphi_1 \vdash a = u_1 : A$ for $l = 1, \dots, k$.

For instance, if $\Gamma, i : \mathbb{I} \vdash A$ and $\Gamma, j : \mathbb{I}, \varphi \vdash u : A$ where $\varphi = (i = 0) \lor (i = 1)$ then the element $u$ is determined by two elements $\Gamma \vdash a_0 : A(i0)$ and $\Gamma \vdash a_1 : A(i1)$ and an element $\Gamma, i : \mathbb{I} \vdash a : A[(i = 0) \mapsto a_0, (i = 1) \mapsto a_1]$ gives a path connecting $a_0$ and $a_1$.

**► Lemma 3.** *The following rules are admissible.<fnref n="2" />*

$$ \frac{\Gamma \vdash \varphi \le \psi : \mathbb{F} \quad \Gamma, \psi \vdash J \quad \Gamma, 1_F \vdash J \quad \Gamma, \varphi, \psi \vdash J}{\Gamma, \varphi \vdash J} $$

Furthermore, if $\varphi$ is independent of $i$, the following rules are admissible

$$ \frac{\Gamma, i : \mathbb{I}, \varphi \vdash J}{\Gamma, \varphi, i : \mathbb{I} \vdash J} $$

and it follows that we have in general:

$$ \frac{\Gamma, i : \mathbb{I}, \varphi \vdash J}{\Gamma, \forall i. \varphi, i : \mathbb{I} \vdash J} $$

## 4.3 Composition Operation

The syntax of compositions is given by:

$$ t, u, A, B ::= \dots \\ \qquad \mid \quad \text{comp}^i A [\varphi \mapsto u] a_0 \qquad \text{Compositions} $$

<footnote n="2">² The inference rules with double line are each a pair of rules, because they can be used in both directions.</footnote>
5:10 Cubical Type Theory

where $u$ is a system on the extent $\varphi$.

The composition operation expresses that being extensible is preserved along paths: if a
partial path is extensible at 0, then it is extensible at 1.

$$
\frac{
  \begin{array}{ccc}
    \Gamma \vdash \varphi : \mathbb{F} & \Gamma, i : \mathbb{I} \vdash A & \Gamma, \varphi, i : \mathbb{I} \vdash u : A \\
    \hline
    \Gamma \vdash \mathrm{comp}^i A [\varphi \mapsto u] a_0 : A(i1) [\varphi \mapsto u(i1)]
  \end{array}
}{
  \Gamma \vdash \mathrm{comp}^i A [\varphi \mapsto u] a_0 : A(i0) [\varphi \mapsto u(i0)]
}
$$

Note that comp^i binds i in A and u and that we have in particular the following equality judgments for systems:

$$
\Gamma \vdash \mathrm{comp}^i A [1_{\mathbb{F}} \mapsto u] a_0 = u(i1) : A(i1)
$$

If we have a substitution $\Delta \vdash \sigma : \Gamma$, then

$$
(\mathrm{comp}^i A [\varphi \mapsto u] a_0)\sigma = \mathrm{comp}^j A(\sigma, i/j) [\varphi\sigma \mapsto u(\sigma, i/j)] a_0\sigma
$$

where $j$ is fresh for $\Delta$, which corresponds semantically to the uniformity [6, 13] of the composition operation.

We use the abbreviation [ $\varphi_1 \mapsto u_1, \dots, \varphi_n \mapsto u_n $] for [ $\bigvee_l \varphi_l \mapsto [\varphi_1 u_1, \dots, \varphi_n u_n] $] and in particular we write [] for [ $0_{\mathbb{F}} \mapsto []$].

► Example 4. With composition we can justify transitivity of path types:

$$
\frac{
  \begin{array}{ccc}
    \Gamma \vdash p : \text{Path } A & a & b \\
    \hline
    \Gamma \vdash \langle i \rangle \ \mathrm{comp}^j A & [(i = 0) \mapsto a, (i = 1) \mapsto q] & j
  \end{array}
}{
  (p \ i) : \text{Path } A \ a \ c
}
$$

This composition can be visualized as the dashed arrow in the square:

<figure><img src="image_4.png" /></figure>

4.4 Kan Filling Operation

As we have connections we also get Kan filling operations from compositions:

$$
\Gamma, i : \mathbb{I} \vdash \mathrm{fill}^i A [\varphi \mapsto u] a_0 = \mathrm{comp}^j A(i/i \wedge j) [\varphi \mapsto u(i/i \wedge j), (i=0) \mapsto a_0] a_0 : A
$$

where $j$ is fresh for $\Gamma$. The element $\Gamma, i : \mathbb{I} \vdash v = \mathrm{fill}^i A [\varphi \mapsto u] a_0 : A$ satisfies:

$$
\Gamma \vdash v(i0) = a_0 : A(i0) \quad \Gamma \vdash v(i1) = \mathrm{comp}^i A [\varphi \mapsto u] a_0 : A(i1) \quad \Gamma, \varphi, i : \mathbb{I} \vdash v = u : A
$$

This means that we can not only compute the lid of an open box but also its filling. If $\varphi$ is
the boundary formula on the names declared in $\Gamma$, we recover the Kan operation for cubical
sets [16].

4.5 Equality Judgments for Composition

The equality judgments for comp^i C [ φ ↦→ u ] a_0 are defined by cases on the type C which depends on i , i.e., Γ, i : II ⊢ C . The right hand side of the definitions are all equal to u (i1) on the extent φ by the typing rule for compositions. There are four cases to consider:
### Product types, $C = (x : A) \to B$

Given $\Gamma, \varphi, i : \mathbb{I} \vdash \mu : C$ and $\Gamma \vdash \lambda_0 : C(i0)[\varphi \mapsto \mu(i0)]$ the composition will be of type $C(i1)$.

For $\Gamma \vdash u_1 : A(i1)$, we first let:

$$w = \text{fill}^i A(i/1 - i) \quad [] \quad u_1 \quad \text{(in context } \Gamma, i : \mathbb{I} \text{ and of type } A(i/1 - i)\text{)}$$

$$v = w(i/1 - i) \quad \text{(in context } \Gamma, i : \mathbb{I} \text{ and of type } A\text{)}$$

Using this we define the equality judgment:

$$\Gamma \vdash (\text{comp}^i C [\varphi \mapsto \mu] \lambda_0) u_1 = \text{comp}^i B(x/v) [\varphi \mapsto \mu v] (\lambda_0 v(i0)) : B(x/v)(i1)$$

### Sum types, $C = (x : A) \times B$

Given $\Gamma, \varphi, i : \mathbb{I} \vdash w : C$ and $\Gamma \vdash w_0 : C(i0)[\varphi \mapsto w(i0)]$ we let:

$$a = \text{fill}^i A [\varphi \mapsto w.1] w_0.1 \quad \text{(in context } \Gamma, i : \mathbb{I} \text{ and of type } A\text{)}$$

$$c_1 = \text{comp}^i A [\varphi \mapsto w.1] w_0.1 \quad \text{(in context } \Gamma \text{ and of type } A(i1)\text{)}$$

$$c_2 = \text{comp}^i B(x/a) [\varphi \mapsto w.2] w_0.2 \quad \text{(in context } \Gamma \text{ and of type } B(x/a)(i1)\text{)}$$

From which we define:

$$\Gamma \vdash \text{comp}^i C [\varphi \mapsto w] w_0 = (c_1, c_2) : C(i1)$$

### Natural numbers, $C = N$

In this we define $\text{comp}^i C [\varphi \mapsto n] n_0$ by recursion:

$$\Gamma \vdash \text{comp}^i C [\varphi \mapsto 0] \quad 0 = 0 : C$$

$$\Gamma \vdash \text{comp}^i C [\varphi \mapsto s n] (s n_0) = s (\text{comp}^i C [\varphi \mapsto n] n_0) : C$$

### Path types, $C = \text{Path A} u v$

Given $\Gamma, \varphi, i : \mathbb{I} \vdash p : C$ and $\Gamma \vdash p_0 : C(i0)[\varphi \mapsto p(i0)]$ we define:

$$\Gamma \vdash \text{comp}^i C [\varphi \mapsto p] p_0 = \langle j \rangle \text{comp}^i A [\varphi \mapsto p j, (j = 0) \mapsto u, (j = 1) \mapsto v] (p_0 j) : C(i1)$$

## 4.6 Transport

Composition for $\varphi = 0_F$ corresponds to transport:

$$\Gamma \vdash \text{transp}^i A a = \text{comp}^i A [] a : A(i1)$$

Together with the fact that singletons are contractible, from Section 3.2, we get the elimination principle for Path types in the same manner as explained for identity types in Section 7.2 of [6].

# 5 Derived Notions and Operations

This section defines various notions and operations that will be used for defining compositions for the glue operation in the next section. This operation will then be used to define the composition operation for the universe and to prove the univalence axiom.
## 5.1 Contractible Types

We define isContr $A = (x : A) \times ((y : A) \to \text{Path } A \times y)$. A proof of isContr $A$ witnesses the fact that $A$ is *contractible*.

Given $\Gamma \vdash p : \text{isContr } A$ and $\Gamma, \varphi \vdash u : A$ we define the operation<fnref n="3" />

$$ \Gamma \vdash \text{contr } p [\varphi \mapsto u] = \text{comp}^i A [\varphi \mapsto p.2 \ u \ i] \ p.1 : A[\varphi \mapsto u] $$

Conversely, we can state the following characterization of contractible types:

**▶ Lemma 5.** Let $\Gamma \vdash A$ and assume that we have one operation

$$ \frac{\Gamma, \varphi \vdash u : A}{\Gamma \vdash \text{contr} [\varphi \mapsto u] : A[\varphi \mapsto u]} $$

then we can find an element in isContr $A$.

**Proof.** We define $x = \text{contr} [] : A$ and prove that any element $y : A$ is path equal to $x$. For this, we introduce a fresh name $i : \mathbb{I}$ and define $\varphi = (i = 0) \lor (i = 1)$ and $u = [(i = 0) \mapsto x, (i = 1) \mapsto y]$. Using this we obtain $\Gamma, i : \mathbb{I} \vdash v = \text{contr} [\varphi \mapsto u] : A[\varphi \mapsto u]$. In this way, we get a path $\langle i \rangle \text{ contr} [\varphi \mapsto u]$ connecting $x$ and $y$. ◀

## 5.2 The pres Operation

The pres operation states that the image of a composition is path equal to the composition of the respective images, so that any function preserves composition, up to path equality.

**▶ Lemma 6.** We have an operation:

$$ \frac{\Gamma, i : \mathbb{I} \vdash f : T \to A \quad \Gamma \vdash \varphi : \mathbb{F} \quad \Gamma, \varphi, i : \mathbb{I} \vdash t : T \quad \Gamma \vdash t_0 : T(i0)[\varphi \mapsto t(i0)]}{\Gamma \vdash \text{pres}^i f [\varphi \mapsto t] t_0 : (\text{Path } A(i1) c_1 c_2)[\varphi \mapsto \langle j \rangle (f t)(i1)]} $$

where $c_1 = \text{comp}^i A [\varphi \mapsto f t] (f(i0) t_0)$ and $c_2 = f(i1) (\text{comp}^i T [\varphi \mapsto t] t_0)$.

**Proof.** Let $\Gamma \vdash a_0 = f(i0) t_0 : A(i0)$ and $\Gamma, i : \mathbb{I} \vdash v = \text{fill}^i T [\varphi \mapsto t] t_0 : T$. We take $\text{pres}^i f [\varphi \mapsto t] t_0 = \langle j \rangle \text{comp}^i A [\varphi \lor (j = 1) \mapsto f v] a_0$. ◀

Note that $\text{pres}^i$ binds $i$ in $f$ and $t$.

## 5.3 The equiv Operation

We define isEquiv $T A f = (y : A) \to \text{isContr} ((x : T) \times \text{Path } A \times (f x))$ and Equiv $T A = (f : T \to A) \times \text{isEquiv } T A f$. If $f : \text{Equiv } T A$ and $t : T$, we may write $f t$ for $f.1 t$.

**▶ Lemma 7.** If $\Gamma \vdash f : \text{Equiv } T A$, we have an operation

$$ \frac{\Gamma, \varphi \vdash t : T \quad \Gamma \vdash a : A \quad \Gamma, \varphi \vdash p : \text{Path } A \ a \ (f \ t)}{\Gamma \vdash \text{equiv } f [\varphi \mapsto (t, p)] \ a : ((x : T) \times \text{Path } A \ a \ (f \ x))[\varphi \mapsto (t, p)]} $$

Conversely, if $\Gamma \vdash f : T \to A$ and we have such an operation, then we can build a proof that $f$ is an equivalence.

**Proof.** We define equiv $f [\varphi \mapsto (t, p)] a = \text{contr} (f.2 a) [\varphi \mapsto (t, p)]$ using the contr operation defined above. The second statement follows from Lemma 5. ◀

<footnote n="3">³ This expresses that the restriction map $\Gamma, \varphi \to \Gamma$ has the left lifting property w.r.t. any “trivial fibration”, i.e., contractible extensions $\Gamma, x : A \to \Gamma$. The restriction maps $\Gamma, \varphi \to \Gamma$ thus represent “cofibrations” while the maps $\Gamma, x : A \to \Gamma$ represent “fibrations”.</footnote>
$$
\begin{array}{ccc}
\Gamma \vdash A & \Gamma, \varphi \vdash T & \Gamma, \varphi \vdash f : \text{Equiv } T A \\
\hline
\multicolumn{3}{c}{\Gamma \vdash \text{Glue } [\varphi \mapsto (T, f)] A} \\
\multicolumn{3}{c}{\Gamma \vdash b : \text{Glue } [\varphi \mapsto (T, f)] A} \\
\multicolumn{3}{c}{\Gamma \vdash \text{un glue } b : A[\varphi \mapsto f b]} \\
\\
\multicolumn{3}{c}{\Gamma, \varphi \vdash f : \text{Equiv } T A} & \Gamma, \varphi \vdash t : T & \Gamma \vdash a : A[\varphi \mapsto f t] \\
\hline
\multicolumn{3}{c}{\Gamma \vdash T} & \multicolumn{2}{c}{\Gamma \vdash a : A[\varphi \mapsto f t]} \\
\multicolumn{3}{c}{\Gamma \vdash \text{Glue } [1_F \mapsto (T, f)] A = T} & \multicolumn{2}{c}{\Gamma \vdash t : T} \\
\multicolumn{3}{c}{} & \multicolumn{2}{c}{\Gamma \vdash f : \text{Equiv } T A} \\
\hline
\multicolumn{3}{c}{} & \multicolumn{2}{c}{\Gamma \vdash \text{glue } [1_F \mapsto t] (f t) = t : T} \\
\\
\multicolumn{3}{c}{\Gamma \vdash b : \text{Glue } [\varphi \mapsto (T, f)] A} & \multicolumn{2}{c}{} \\
\hline
\multicolumn{3}{c}{\Gamma \vdash b = \text{glue } [\varphi \mapsto b] \text{ (un glue } b) : \text{Glue } [\varphi \mapsto (T, f)] A} \\
\\
\multicolumn{3}{c}{\Gamma, \varphi \vdash f : \text{Equiv } T A} & \Gamma, \varphi \vdash t : T & \Gamma \vdash a : A[\varphi \mapsto f t] \\
\hline
\multicolumn{3}{c}{} & \multicolumn{2}{c}{\Gamma \vdash \text{un glue } (\text{glue } [\varphi \mapsto t] a) : a : A}
\end{array}
$$

<figure><img src="image_5.png" /><figcaption>Figure 4 Inference rules for glueing.</figcaption></figure>

# 6 Glueing

In this section, we introduce the glueing operation. This operation expresses that to be “extensible” is invariant by equivalence. From this operation, we can define a composition operation for universes, and prove the univalence axiom.

## 6.1 Syntax and Inference Rules for Glueing

We introduce the *glueing* construction at type and term level by:

$$
t, u, A, B ::= \dots
\begin{array}{l@{\quad}l@{\quad}l}
\text{Glue } [\varphi \mapsto (T, f)] A & \text{Glue type} & \\
\text{glue } [\varphi \mapsto t] u & \text{Glue term} & \\
\text{un glue } [\varphi \mapsto f] u & \text{Unglue term} &
\end{array}
$$

We may write simply unglue $b$ for unglue $[\varphi \mapsto f] b$. The inference rules for these are presented in Figure 4.

It follows from these rules that if $\Gamma \vdash b : \text{Glue } [\varphi \mapsto (T, f)] A$, then $\Gamma, \varphi \vdash b : T$.

In the case $\varphi = (i = 0) \lor (i = 1)$ the glueing operation can be illustrated as the dashed line in:

<figure><img src="image_6.png" /></figure>

This illustrates why the operation is called glue: it *glues* together along a partial equivalence the partial type *T* and the total type *A* to a total type that extends *T*.
5:14 Cubical Type Theory

► Remark. In general Glue [φ ↦→ (T, f)] A can be illustrated as:

<figure><img src="image_7.png" /></figure>

This diagram suggests that a construction similar to Glue also appears in the simplicial set model. Indeed, the proof of Theorem 3.4.1 in [17] contains a similar diagram where $\bar{E}_1$ corresponds to Glue [φ ↦→ (T, f)] A.

► **Example 8.** Using glueing we can construct a path from an equivalence $\Gamma \vdash f : \text{Equiv } A B$ by defining

$$ \Gamma, i : \mathbb{I} \vdash E = \text{Glue} [(i = 0) \mapsto (A, f), (i = 1) \mapsto (B, \text{id}_B)] B $$

so that $E(i0) = A$ and $E(i1) = B$, where $\text{id}_B : \text{Equiv } B B$ is defined as:

$$ \text{id}_B = (\lambda x : B. x, \lambda x : B. ((x, 1_x), \lambda u : (y : B) \times \text{Path } B x y. \langle i \rangle (u.2 i, \langle j \rangle u.2 (i \wedge j)))) $$

In Section 7 we introduce a universe of types U and we will be able to define a function of type $(A B : U) \to \text{Equiv } A B \to \text{Path } U A B$ by:

$$ \lambda A B : U. \lambda f : \text{Equiv } A B. \langle i \rangle \text{Glue} [(i = 0) \mapsto (A, f), (i = 1) \mapsto (B, \text{id}_B)] B $$

## 6.2 Composition for Glueing

We assume $\Gamma, i : \mathbb{I} \vdash B = \text{Glue} [\varphi \mapsto (T, f)] A$, and define the composition in $B$. In order to do so, assume

$$ \Gamma, \psi, i : \mathbb{I} \vdash b : B \qquad \Gamma \vdash b_0 : B(i0)[\psi \mapsto b(i0)] $$

and define:

$$ \begin{array}{ll} a = \text{unglue } b & (\text{in context } \Gamma, \psi, i : \mathbb{I} \text{ and of type } A[\varphi \mapsto f b]) \\ a_0 = \text{unglue } b_0 & (\text{in context } \Gamma \text{ and of type } A(i0)[\varphi(i0) \mapsto f(i0), \psi \mapsto a(i0)]) \end{array} $$

The following provides the algorithm for composition $\text{comp}^i B [\psi \mapsto b] b_0 = b_1$ of type $B(i1)[\psi \mapsto b(i1)]$.

$$ \begin{array}{rcl} \delta & = & \forall i. \varphi \\ a'_1 & = & \text{comp}^i A [\psi \mapsto a] a_0 \\ t'_1 & = & \text{comp}^i T [\psi \mapsto b] b_0 \\ \omega & = & \text{pres}^i f [\psi \mapsto b] b_0 \\ (t_1, \alpha) & = & \text{equiv} f(i1) [\delta \mapsto (t'_1, \omega), \psi \mapsto (b(i1), \langle j \rangle a'_1)] a'_1 \\ a_1 & = & \text{comp}^j A(i1) [\varphi(i1) \mapsto \alpha j, \psi \mapsto a(i1)] a'_1 \\ b_1 & = & \text{glue} [\varphi(i1) \mapsto t_1] a_1 \end{array} \qquad \begin{array}{l} \Gamma \\ \Gamma \\ \Gamma, \delta \\ \Gamma, \delta \\ \Gamma, \varphi(i1) \\ \Gamma \\ \Gamma \end{array} $$
We can check that whenever $\Gamma, i : \mathbb{I} \vdash \varphi = 1_{\mathbb{F}} : \mathbb{F}$ the definition of $b_1$ coincides with $\mathrm{comp}^i T [\psi \mapsto b] b_0$, which is consistent with the fact that $B = T$ in this case.

In the next section we will use the glue operation to define the composition for the
universe and to prove the univalence axiom.

# 7 Universe and the Univalence Axiom

As in [20], we now introduce a universe U à la Russell by reflecting all typing rules and

$$ \frac{\Gamma \vdash \Gamma \vdash A : U}{\Gamma \vdash U \quad \Gamma \vdash A} $$

In particular, we have $\Gamma \vdash \mathrm{Glue} [\varphi \mapsto (T, f)] A : U$ whenever $\Gamma \vdash A : U$, $\Gamma, \varphi \vdash T : U$, and $\Gamma, \varphi \vdash f : \mathrm{Equiv} T A$.

## 7.1 Composition for the Universe

In order to describe the composition operation for the universe we first have to explain how to construct an equivalence from a line in the universe. Given $\Gamma \vdash A$, $\Gamma \vdash B$, and $\Gamma, i : \mathbb{I} \vdash E$, such that $E(i0) = A$ and $E(i1) = B$, we will construct $\mathrm{equiv}^i E : \mathrm{Equiv} A B$. In order to do this we first define

$$ f = \lambda x : A. \mathrm{transp}^i E x \qquad (\text{in context } \Gamma \text{ and of type } A \to B) $$

$$ g = \lambda y : B. (\mathrm{transp}^i E(i/1 - i) y)(i/1 - i) \qquad (\text{in context } \Gamma \text{ and of type } B \to A) $$

$$ u = \lambda x : A. \mathrm{fill}^i E [] x \qquad (\text{in context } \Gamma, i : \mathbb{I} \text{ and of type } A \to E) $$

$$ v = \lambda y : B. (\mathrm{fill}^i E(i/1 - i) [] y)(i/1 - i) \qquad (\text{in context } \Gamma, i : \mathbb{I} \text{ and of type } B \to E) $$

such that:

$$ u(i0) = \lambda x : A.x \qquad u(i1) = f \qquad v(i0) = g \qquad v(i1) = \lambda y : B.y $$

We will now prove that $f$ is an equivalence. Given $y : B$ we see that $(x : A) \times \mathrm{Path} B y (f x)$ is inhabited as it contains the element $(g y, \langle j \rangle \theta_0(i1))$ where

$$ \theta_0 = \mathrm{fill}^i E [(j = 0) \mapsto v y, (j = 1) \mapsto u (g y)] (g y). $$

Next, given an element $(x, \beta)$ of $(x : A) \times \mathrm{Path} B y (f x)$ we will construct a path from $(g y, \langle j \rangle \theta_0(i1))$ to $(x, \beta)$. Let

$$ \theta_1 = (\mathrm{fill}^i E(i/1 - i) [(j = 0) \mapsto (v y)(i/1 - i), (j = 1) \mapsto (u x)(i/1 - i)] (\beta j)) (i/1 - i) $$

and $\omega = \theta_1(i0)$ so $\Gamma, i : \mathbb{I}, j : \mathbb{I} \vdash \theta_1 : E, \omega(j0) = g y$, and $\omega(j1) = x$. And further with

$$ \delta = \mathrm{comp}^i E [(k = 0) \mapsto \theta_0, (k = 1) \mapsto \theta_1, (j = 0) \mapsto v y, (j = 1) \mapsto u \omega(j/k)] \omega(j/j \wedge k) $$

we obtain

$$ \langle k \rangle (\omega(j/k), \langle j \rangle \delta) : \mathrm{Path} ((x : A) \times \mathrm{Path} B y (f x)) (g y, \langle j \rangle \theta_0(i1)) (x, \beta) $$

as desired. This concludes the proof that $f$ is an equivalence and thus also the construction of $\mathrm{equiv}^i E : \mathrm{Equiv} A B$.

Using this we can now define the composition for the universe:

$$ \Gamma \vdash \mathrm{comp}^i U [\varphi \mapsto E] A_0 = \mathrm{Glue} [\varphi \mapsto (E(i1), \mathrm{equiv}^i E(i/1 - i))] A_0 : U $$
5:16 Cubical Type Theory

► **Remark.** Given $\Gamma, i : \mathbb{I} \vdash E$ we can also get an equivalence in $\text{Equiv } A B$ (where $A = E(i0)$ and $B = E(i1)$) with a less direct description by

$$ \Gamma \vdash \text{transp}^i (\text{Equiv } A E) \text{ id}_A : \text{Equiv } A B $$

where $\text{id}_A$ is the identity equivalence as given in Example 8.

7.2 The Univalence Axiom

Given $B = \text{Glue} [\varphi \mapsto (T, f)] A$ the map unglue : $B \to A$ extends $f$, in the sense that $\Gamma, \varphi \vdash \text{unglue } b = f b : A$ if $\Gamma \vdash b : B$.

► **Theorem 9.** *The map unglue : $B \to A$ is an equivalence.*

*Proof.* By Lemma 7 it suffices to construct

$$ \tilde{b} : B[\psi \mapsto b] \qquad \tilde{\alpha} : \text{Path } A u (\text{unglue } \tilde{b})[\psi \mapsto \alpha] $$

given $\Gamma, \psi \vdash b : B$ and $\Gamma \vdash u : A$ and $\Gamma, \psi \vdash \alpha : \text{Path } A u (\text{unglue } b)$.

Since $\Gamma, \varphi \vdash f : T \to A$ is an equivalence and

$$ \Gamma, \varphi, \psi \vdash b : T \qquad \Gamma, \varphi, \psi \vdash \alpha : \text{Path } A u (f b) $$

we get, using Lemma 7

$$ \Gamma, \varphi \vdash t : T[\psi \mapsto b] \qquad \Gamma, \varphi \vdash \beta : \text{Path } A u (f t) [\psi \mapsto \alpha] $$

We then define $\tilde{a} = \text{comp}^i A [\varphi \mapsto \beta i, \psi \mapsto \alpha i] u$, and using this we conclude by letting $\tilde{b} = \text{glue} [\varphi \mapsto t] \tilde{a}$ and $\tilde{\alpha} = \text{fill}^i A [\varphi \mapsto \beta i, \psi \mapsto \alpha i] u$. ◀

► **Corollary 10.** For any type $A : U$ the type $C = (X : U) \times \text{Equiv } X A$ is contractible.<fnref n="4" />

*Proof.* It is enough by Lemma 5 to show that any partial element $\varphi \vdash (T, f) : C$ is path equal to the restriction of a total element. The map unglue extends $f$ and is an equivalence by the previous theorem. Since any two elements of the type is $\text{Equiv } X A$ $f.1$ are path equal, this shows that any partial element of type $C$ is path equal to the restriction of a total element. We can then conclude by Theorem 9. ◀

► **Corollary 11 (Univalence axiom).** For any term

$$ t : (A B : U) \to \text{Path } U A B \to \text{Equiv } A B $$

the map $t A B : \text{Path } U A B \to \text{Equiv } A B$ is an equivalence.

*Proof.* Both $(X : U) \times \text{Path } U A X$ and $(X : U) \times \text{Equiv } A X$ are contractible. Hence the result follows from Theorem 4.7.7 in [26]. ◀

Two alternative proofs of univalence can be found in Appendix B.

<footnote n="4">⁴ This formulation of the univalence axiom can be found in the message of Martín Escardó in: https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ This is also used in the (classical) proofs of the univalence axiom, see Theorem 3.4.1 of [17] and Proposition 2.18 of [8], where an operation similar to the glueing operation appears implicitly.</footnote>
# 8 Semantics

In this section we will explain the semantics of the type theory under consideration in cubical sets. We will first review how cubical sets, as a presheaf category, yield a model of basic type theory, and then explain the additional so-called composition structure we have to require to interpret the full cubical type theory.

## 8.1 The Category of Cubes and Cubical Sets

Consider the monad $dM$ on the category of sets associating to each set the free de Morgan algebra on that set. The category of cubes $C$ is the small category whose objects are finite subsets $I, J, K, \dots$ of a fixed, discrete, and countably infinite set, called names, and a morphism $\text{Hom}(J, I)$ is a map $I \to dM(J)$. Identities and compositions are inherited from the Kleisli category of $dM$, i.e., the identity on $I$ is given by the unit $I \to dM(I)$, and composition $fg \in \text{Hom}(K, I)$ of $g \in \text{Hom}(K, J)$ and $f \in \text{Hom}(J, I)$ is given by $\mu_K \circ dM(g) \circ f$ where $\mu_K: dM(dM(K)) \to dM(K)$ denotes multiplication of $dM$. We will use $f, g, h$ for morphisms in $C$ and simply write $f: J \to I$ for $f \in \text{Hom}(J, I)$. We will often write unions with commas and omit curly braces around finite sets of names, e.g., writing $I, i, j$ for $I \cup \{i, j\}$ and $I - i$ for $I - \{i\}$ etc.

If $i$ is in $I$ and $b$ is $0_I$ or $1_I$, we have maps $(ib)$ in $\text{Hom}(I - i, I)$ whose underlying map sends $j \neq i$ to itself and $i$ to $b$. A face map is a composition of such maps. A strict map $\text{Hom}(J, I)$ is a map $I \to dM(J)$ which never takes the value $0_I$ or $1_I$. Any $f$ can be uniquely written as a composition $f = gh$ where $g$ is a face map and $h$ is strict.

**► Definition 12.** A cubical set is a presheaf on $C$.

Thus, a cubical set $\Gamma$ is given by sets $\Gamma(I)$ for each $I \in C$ and maps (called restrictions) $\Gamma(f): \Gamma(I) \to \Gamma(J)$ for each $f: J \to I$. If we write $\Gamma(f)(\rho) = \rho f$ for $\rho \in \Gamma(I)$ (leaving the $\Gamma$ implicit), these maps should satisfy $\rho \text{id}_I = \rho$ and $(\rho f)g = \rho(fg)$ for $f: J \to I$ and $g: K \to J$.

Let us discuss some important examples of cubical sets. Using the canonical de Morgan algebra structure of the unit interval, $[0, 1]$, we can define a functor

$$C \to \text{Top}, \quad I \mapsto [0, 1]^I. \qquad (1)$$

If $u$ is in $[0, 1]^I$ we can think of $u$ as an environment giving values in $[0, 1]$ to each $i \in I$, so that $iu$ is in $[0, 1]$ if $i \in I$. Since $[0, 1]$ is a de Morgan algebra, this extends uniquely to $ru$ for $r \in dM(I)$. So any $f: J \to I$ in $C$ induces $f: [0, 1]^J \to [0, 1]^I$ by $i(fu) = (if)u$.

To any topological space $X$ we can associate its singular cubical set $S(X)$ by taking $S(X)(I)$ to be the set of continuous functions $[0, 1]^I \to X$.

For a finite set of names $I$ we get the formal cube $yI$ where $y: C \to [C^{\text{op}}, \text{Set}]$ denotes the Yoneda embedding. Note that since **Top** is cocomplete the functor in (1) extends to a cocontinuous functor assigning to each cubical set its geometric realization as a topological space, in such a way that $yI$ has $[0, 1]^I$ as its geometric realization.

The formal interval $\mathbb{I}$ induces a cubical set given by $\mathbb{I}(I) = dM(I)$. The face lattice $\mathbb{F}$ induces a cubical set by taking as $\mathbb{F}(I)$ to be those $\varphi \in \mathbb{F}$ which only use symbols in $I$. The restrictions along $f: J \to I$ are in both cases simply substituting the symbols $i \in I$ by $f(i) \in dM(J)$.

As any presheaf category, cubical sets have a subobject classifier $\Omega$ where $\Omega(I)$ is the set of sieves on $I$ (i.e., subfunctors of $yI$). Consider the natural transformation $(\cdot = 1): \mathbb{I} \to \Omega$ where for $r \in \mathbb{I}(I)$, $(r = 1)$ is the sieve on $I$ of all $f: J \to I$ such that $rf = 1_I$. The image of $(\cdot = 1)$ is $\mathbb{F} \to \Omega$, assigning to each $\varphi$ the sieve of all $f$ with $\varphi f = 1_{\mathbb{F}}$.
## 8.2 Presheaf Semantics

The category of cubical sets (with morphisms being natural transformations) induce—as does any presheaf category—a category with families (CwF) [9] where the category of contexts and substitutions is the category of cubical sets. We will review the basic constructions but omit verification of the required equations (see, e.g., [12, 13, 6] for more details).

### Basic Presheaf Semantics

As already mentioned the category of (semantic) contexts and substitutions is given by cubical sets and their maps. In this section we will use $\Gamma, \Delta$ to denote cubical sets and (semantic) substitutions by $\sigma: \Delta \to \Gamma$, overloading previous use of the corresponding meta-variables to emphasize their intended role.

Given a cubical set $\Gamma$, the types $A$ in context $\Gamma$, written $A \in \text{Ty}(\Gamma)$, are given by sets $A\rho$ for each $I \in \mathcal{C}$ and $\rho \in \Gamma(I)$ together with restriction maps $A\rho \to A(\rho f)$, $u \mapsto uf$ for $f: J \to I$ satisfying $u \text{id}_I = u$ and $(uf)g = u(fg) \in A(\rho fg)$ if $g: K \to J$. Equivalently, $A \in \text{Ty}(\Gamma)$ are the presheaves on the category of elements of $\Gamma$. For a type $A \in \text{Ty}(\Gamma)$ its terms $a \in \text{Ter}(\Gamma; A)$ are given by families of elements $a\rho \in A\rho$ for each $I \in \mathcal{C}$ and $\rho \in \Gamma(I)$ such that $(a\rho)f = a(\rho f)$ for $f: J \to I$. Note that our notation leaves a lot implicit; e.g., we should have written $A(I, \rho)$ for $A\rho; A(I, \rho, f)$ for the restriction map $A\rho \to A(\rho f)$; and $a(I, \rho)$ for $a\rho$.

For $A \in \text{Ty}(\Gamma)$ and $\sigma: \Delta \to \Gamma$ we define $A\sigma \in \text{Ty}(\Delta)$ by $(A\sigma)\rho = A(\sigma\rho)$ and the induced restrictions. If we also have $a \in \text{Ter}(\Gamma; A)$, we define $a\sigma \in \text{Ter}(\Delta; A\sigma)$ by $(a\sigma)\rho = a(\sigma\rho)$. For a type $A \in \text{Ty}(\Gamma)$ we define the cubical set $\Gamma.A$ by $(\Gamma.A)(I)$ being the set of all $(\rho, u)$ with $\rho \in \Gamma(I)$ and $u \in A\rho$; restrictions are given by $(\rho, u)f = (\rho f, uf)$. The first projection yields a map $\rho: \Gamma.A \to \Gamma$ and the second projection a term $q \in \text{Ter}(\Gamma.A; A\rho)$. Given $\sigma: \Delta \to \Gamma$, $A \in \text{Ty}(\Gamma)$, and $a \in \text{Ter}(\Delta; A\sigma)$ we define $(\sigma, a): \Delta \to \Gamma.A$ by $(\sigma, a)\rho = (\sigma\rho, a\rho)$. For $u \in \text{Ter}(\Gamma; A)$ we define $[u] = (\text{id}_\Gamma, u): \Gamma \to \Gamma.A$.

The basic type formers are interpreted as follows. For $A \in \text{Ty}(\Gamma)$ and $B \in \text{Ty}(\Gamma.A)$ define $\Sigma_\Gamma(A, B) \in \text{Ty}(\Gamma)$ by letting $\Sigma_\Gamma(A, B)\rho$ contain all pairs $(u, v)$ where $u \in A\rho$ and $v \in B(\rho, v)$; restrictions are defined as $(u, v)f = (uf, vf)$. Given $w \in \text{Ter}(\Gamma; \Sigma(A, B))$ we get $w.1 \in \text{Ter}(\Gamma; A)$ and $w.2 \in \text{Ter}(\Gamma; B[w.1])$ by $(w.1)\rho = \mathbf{p}(w\rho)$ and $(w.2)\rho = \mathbf{q}(w\rho)$ where $\mathbf{p}(u, v) = u$ and $\mathbf{q}(u, v) = v$ are the set-theoretic projections.

Given $A \in \text{Ty}(\Gamma)$ and $B \in \text{Ty}(\Gamma.A)$ the dependent function space $\Pi_\Gamma(A, B) \in \text{Ty}(\Gamma)$ is defined by letting $\Pi_\Gamma(A, B)\rho$ for $\rho \in \Gamma(I)$ contain all families $w = (w_f | J \in \mathcal{C}, f: J \to I)$ where

$$w_f \in \prod_{u \in A(\rho f)} B(\rho f, u) \quad \text{such that} \quad (w_f u)g = w_{fg}(ug) \quad \text{for } u \in A(\rho f), g: K \to J.$$

The restriction by $f: J \to I$ of such a $w$ is defined by $(wf)_g = w_{fg}$. Given $v \in \text{Ter}(\Gamma.A; B)$ we have $\lambda_{\Gamma;A}v \in \text{Ter}(\Gamma; \Pi(A, B))$ given by $((\lambda v)\rho)_f u = v(\rho f, u)$. Application $\mathbf{app}(w, u) \in \text{Ter}(\Gamma; B[u])$ of $w \in \text{Ter}(\Gamma; \Pi(A, B))$ to $u \in \text{Ter}(\Gamma; A)$ is defined by

$$\mathbf{app}(w, u)\rho = (w\rho)_{\text{id}_I}(u\rho) \in (B[u])\rho. \qquad (2)$$

Basic data types like the natural numbers can be interpreted as discrete presheaves, i.e., $\mathbb{N} \in \text{Ty}(\Gamma)$ is given by $\mathbb{N}\rho = \mathbb{N}$; the constants are interpreted by the lifts of the corresponding set-theoretic operations on $\mathbb{N}$. This concludes the outline of the basic CwF structure on cubical sets.
**Remark.** Following Aczel [1] we will make use of that our semantic entities are actual sets in the ambient set theory. This will allow us to interpret syntax in Section 8.3 with fewer type annotations than are usually needed for general categorical semantics of type theory (see [24]). E.g., the definition of application `app(w, u)ρ` as defined in (2) is independent of Γ, A and B, since set-theoretic application is a (class) operation on all sets. Likewise, we don't need annotations for first and second projections. But note that we will need the type A for λ-abstraction for $(\lambda_{\Gamma;A}v)ρ$ to be a set by the replacement axiom.

## Semantic path types

Note that we can consider any cubical set $X$ as $X' \in \text{Ty}(\Gamma)$ by setting $X'\rho = X(I)$ for $\rho \in \Gamma(I)$. We will usually simply write $X$ for $X'$. In particular, for a cubical set $\Gamma$ we can form the cubical set $\Gamma.I$.

For $A \in \text{Ty}(\Gamma)$ and $u, v \in \text{Ter}(\Gamma; A)$ the semantic path type $\text{Path}_A^\Gamma(u, v) \in \text{Ty}(\Gamma)$ is given by: for $\rho \in \Gamma(I)$, $\text{Path}_A(u, v)\rho$ consists of equivalence classes $\langle i \rangle w$ where $i \notin I$, $w \in A(\rho s_i)$ such that $w(i0) = u\rho$ and $w(i1) = v\rho$; two such elements $\langle i \rangle w$ and $\langle j \rangle w'$ are equal iff $w(i/j) = w'$. Here $s_i: I, i \to I$ is induced by the inclusion $I \subseteq I, i$ and $(i/j)$ setting $i$ to $j$. We define $(\langle i \rangle w) f = \langle j \rangle w(f, i/j)$ for $f: J \to I$ and $j \notin J$. For $r \in I(I)$ we set $(\langle i \rangle w) r = w(i/r)$. Both operations, name abstraction and application, lift to terms, i.e., if $w \in \text{Ter}(\Gamma.I; A)$, then $\langle \rangle w \in \text{Ter}(\Gamma; \text{Path}_A(w[0], w[1]))$ given by $(\langle \rangle w)\rho = \langle i \rangle w(\rho s_i)$ for a fresh $i$; also if $u \in \text{Ter}(\Gamma; \text{Path}_A(a, b))$ and $r \in \text{Ter}(\Gamma; I)$, then $u r \in \text{Ter}(\Gamma; A)$ defined as $(u r)\rho = (u\rho)(r\rho)$.

## Composition Structure

For $\varphi \in \text{Ter}(\Gamma; \mathbb{F})$ we define the cubical set $\Gamma, \varphi$ by taking $\rho \in (\Gamma, \varphi)(I)$ iff $\rho \in \Gamma(I)$ and $\varphi\rho = 1_{\mathbb{F}} \in \mathbb{F}$; the restrictions are those induced by $\Gamma$. In particular, we have $\Gamma, 1 = \Gamma$ and $\Gamma, 0$ is the empty cubical set. (Here, $0 \in \text{Ter}(\Gamma; \mathbb{F})$ is $0\rho = 0_{\mathbb{F}}$ and similarly for $1_{\mathbb{F}}$.) Any $\sigma: \Delta \to \Gamma$ gives rise to a morphism $\Delta, \varphi\sigma \to \Gamma, \varphi$ which we also will denote by $\sigma$.

If $A \in \text{Ty}(\Gamma)$ and $\varphi \in \text{Ter}(\Gamma; \mathbb{F})$, we define a *partial element of A* $\in \text{Ty}(\Gamma)$ *of extent* $\varphi$ to be an element of $\text{Ter}(\Gamma, \varphi; A \iota_{\varphi})$ where $\iota_{\varphi}: \Gamma, \varphi \hookrightarrow \Gamma$ is the inclusion. So, such a partial element $u$ is given by a family of elements $u\rho \in A\rho$ for each $\rho \in \Gamma(I)$ such that $\varphi\rho = 1$, satisfying $(u\rho)f = u(\rho f)$ whenever $f: J \to I$. Each $u \in \text{Ter}(\Gamma; A)$ gives rise to the partial element $u\iota \in \text{Ter}(\Gamma, \varphi; A\iota)$; a partial element is *extensible* if it is induced by such an element of $\text{Ter}(\Gamma; A)$.

For the next definition note that if $A \in \text{Ty}(\Gamma)$, then $\rho \in \Gamma(I)$ corresponds to $\rho: \mathbf{y} I \to \Gamma$ and thus $A\rho \in \text{Ty}(\mathbf{y} I)$; also, any $\varphi \in \mathbb{F}(I)$ corresponds to $\varphi \in \text{Ter}(\mathbf{y} I; \mathbb{F})$.

**Definition 13.** A *composition structure* for $A \in \text{Ty}(\Gamma)$ is given by the following operations. For each $I, i \notin I$, $\rho \in \Gamma(I, i)$, $\varphi \in \mathbb{F}(I)$, $u$ a partial element of $A\rho$ of extent $\varphi$, and $a_0 \in A\rho(i0)$ with $a_0 f = u_{(i0)f}$ for all $f: J \to I$ with $\varphi f = 1_{\mathbb{F}}$ (i.e., $a_0 \iota_{\varphi} = u(i0)$ if $a_0$ is considered as element of $\text{Ter}(\mathbf{y} I; A\rho(i0)))$, we require

$$ \text{comp}(I, i, \rho, \varphi, u, a_0) \in A\rho(i1) $$

such that for any $f: J \to I$ and $j \notin J$,

$$ (\text{comp}(I, i, \rho, \varphi, u, a_0))f = \text{comp}(J, j, \rho(f, i = j), \varphi f, u(f, i = j), a_0 f), $$

and $\text{comp}(I, i, \rho, 1_{\mathbb{F}}, u, a_0) = u_{(i1)}$.
5:20 Cubical Type Theory

A type $A \in \text{Ty}(\Gamma)$ together with a composition structure $\text{comp}$ on $A$ is called a *fibrant type*, written $(A, \text{comp}) \in \text{FTy}(\Gamma)$. We will usually simply write $A \in \text{FTy}(\Gamma)$ and $\text{comp}_A$ for its composition structure. But observe that $A \in \text{Ty}(\Gamma)$ can have different composition structures. Call a cubical set $\Gamma$ *fibrant* if it is a fibrant type when $\Gamma$ considered as type $\Gamma \in \text{Ty}(\Gamma)$ is fibrant where $\Gamma$ is a terminal cubical set. A prime example of a fibrant cubical set is the singular cubical set of a topological space (see Appendix C).

**Theorem 14.** The CwF on cubical sets supporting dependent products, dependent sums, and natural numbers described above can be extended to fibrant types.

**Proof.** For example, if $A \in \text{FTy}(\Gamma)$ and $\sigma: \Delta \to \Gamma$, we set

$$ \text{comp}_{A\sigma}(I, i, \rho, \varphi, u, a_0) = \text{comp}_A(I, i, \sigma\rho, \varphi, u, a_0) $$

as the composition structure on $A\sigma$ in $\text{FTy}(\Delta)$. Type formers are treated analogously to their syntactic counterpart given in Section 4. Note that one also has to check that all equations between types are also preserved by their associated composition structures. ◀

Note that we can also, like in the syntax, define a composition structure on $\text{Path}_A(u, v)$ given that $A$ has one.

Semantic Glueing

Next we will give a semantic counterpart to the Glue construction. To define the semantic glueing as an element of $\text{Ty}(\Gamma)$ it is not necessary that the given types have composition structures or that the functions are equivalences; this is only needed later to give the composition structure. Assume $\varphi \in \text{Ter}(\Gamma; \mathbb{F})$, $T \in \text{Ty}(\Gamma, \varphi)$, $A \in \text{Ty}(\Gamma)$, and $w \in \text{Ter}(\Gamma, \varphi; T \to A\iota)$ (where $A \to B$ is $\Pi(A, B\rho)$).

**Definition 15.** The semantic glueing $\text{Glue}_\Gamma(\varphi, T, A, w) \in \text{Ty}(\Gamma)$ is defined as follows. For $\rho \in \Gamma(I)$, we let $u \in \text{Glue}(\varphi, T, A, w)\rho$ iff either

u $\in T\rho$ and $\varphi\rho = 1_{\mathbb{F}}$; or

u = glue($\varphi\rho, t, a$) and $\varphi\rho \neq 1_{\mathbb{F}}$, where $t \in \text{Ter}(\mathbf{y} I, \varphi\rho; T\rho)$ and $a \in \text{Ter}(\mathbf{y} I; A\rho)$ such that $\text{app}(w\rho, t) = a\iota \in \text{Ter}(\mathbf{y} I, \varphi\rho; A\rho\iota)$.

For $f: J \to I$ we define the restriction $uf$ of $u \in \text{Glue}(\varphi, T, A, w)$ to be given by the restriction of $T\rho$ in the first case; in the second case, i.e., if $\varphi\rho \neq 1_{\mathbb{F}}$, we let $uf = \text{glue}(\varphi\rho, t, a)f = t_f \in T\rho f$ in case $\varphi\rho f = 1_{\mathbb{F}}$, and otherwise $uf = \text{glue}(\varphi\rho f, tf, af)$.

Here glue was defined as a constructor; we extend glue to any $t \in \text{Ter}(\mathbf{y} I; T\rho)$, $a \in \text{Ter}(\mathbf{y} I; A\rho)$ such that $\text{app}(w\rho, t) = a$ (so if $\varphi\rho = 1_{\mathbb{F}}$) by glue($1_{\mathbb{F}}, t, a) = t_{\text{id}_I}$. This way any element of $\text{Glue}(\varphi, T, A, w)\rho$ is of the form glue($\varphi\rho, t, a$) for suitable $t$ and $a$, and restriction is given by $(\text{glue}(\varphi\rho, t, a))f = \text{glue}(\varphi\rho f, tf, af)$. Note that we get

$$ \text{Glue}_{\Gamma}(1_{\mathbb{F}}, T, A, w) = T \text{ and } (\text{Glue}_{\Gamma}(\varphi, T, A, w))\sigma = \text{Glue}_{\Delta}(\varphi\sigma, T\sigma, A\sigma, w\sigma) \quad (3) $$

for $\sigma: \Delta \to \Gamma$. We define unglue($\varphi, w) \in \text{Ter}(\Gamma.\text{Glue}(\varphi, T, A, w); A\rho)$ by

$$ \begin{aligned} \text{unglue}(\varphi, w)(\rho, t) &= \text{app}(w\rho, t)_{\text{id}_I} \in A\rho & \text{whenever } \varphi\rho = 1_{\mathbb{F}}, \text{ and} \\ \text{unglue}(\varphi, w)(\rho, \text{glue}(\varphi, t, a)) &= a & \text{otherwise,} \end{aligned} $$

where $\rho \in \Gamma(I)$.

**Definition 16.** For $A, B \in \text{Ty}(\Gamma)$ and $w \in \text{Ter}(\Gamma; A \to B)$ an equivalence structure for $w$ is given by the following operations such that for each
- $\rho \in \Gamma(I),$

- $\varphi \in \mathbb{F}(I),$

- $b \in B\rho$, and

- partial elements $a$ of $A\rho$ and $\omega$ of $\mathbf{Path}_B(\mathbf{app}(w\rho, a), bl)\rho$ with extent $\varphi$, we are given

$e_0(\rho, \varphi, b, a, \omega) \in A\rho$, and a path $e_1(\rho, \varphi, b, a, \omega)$ between $\mathbf{app}(w\rho, e_0(\rho, \varphi, b, a, \omega))$ and $b$ such that $e_0(\rho, \varphi, b, a, \omega)\iota = a$, $e_1(\rho, \varphi, b, a, \omega)\iota = \omega$ (where $\iota: \mathbf{y}I, \varphi \to \mathbf{y}I$) and for any $f: J \to I$ and $\nu = 0, 1$:

$$ (e_\nu(\rho, \varphi, b, a, \omega))f = e_\nu(\rho f, \varphi f, bf, af, \omega f). $$

Following the argument in the syntax we can use the equivalence structure to explain a composition for Glue.

**Theorem 17.** If $A \in \mathbf{FTy}(\Gamma)$, $T \in \mathbf{FTy}(\Gamma, \varphi)$, and we have an equivalence structure for $w$, then we have a composition structure for $\mathbf{Glue}(\varphi, T, A, w)$ such that the equations (3) also hold for the respective composition structures.

## Semantic Universes

Assuming a Grothendieck universe of small sets in our ambient set theory, we can define $A \in \mathbf{Ty}_0(\Gamma)$ iff all $A\rho$ are small for $\rho \in \Gamma(I)$; and $A \in \mathbf{FTy}_0(\Gamma)$ iff $A \in \mathbf{Ty}_0(\Gamma)$ when forgetting the composition structure of $A$.

**Definition 18.** The semantic universe $\mathbf{U}$ is the cubical set defined by $\mathbf{U}(I) = \mathbf{FTy}_0(\mathbf{y}I)$; restriction along $f: J \to I$ is simply substitution along $\mathbf{y}f$.

We can consider $\mathbf{U}$ as an element of $\mathbf{Ty}(\Gamma)$. As such we can, as in the syntactic counterpart, define a composition structure on $\mathbf{U}$ using semantic glueing, so that $\mathbf{U} \in \mathbf{FTy}(\Gamma)$. Note that semantic glueing preserves smallness.

For $T \in \mathrm{Ter}(\Gamma; \mathbf{U})$ we can define decoding $\mathrm{El}T \in \mathbf{FTy}_0(\Gamma)$ by $(\mathrm{El}T)\rho = (T\rho)\mathrm{id}_I$ and likewise for the composition structure. For $A \in \mathbf{FTy}_0(\Gamma)$ we get its code $\lceil A \rceil \in \mathrm{Ter}(\Gamma; \mathbf{U})$ by setting $\lceil A \rceil \rho \in \mathbf{FTy}_0(\mathbf{y}I)$ to be given by the sets $(\lceil A \rceil \rho)f = A(\rho f)$ and likewise for restrictions and composition structure. These operations satisfy $\mathrm{El}\lceil A \rceil = A$ and $\lceil \mathrm{El}T \rceil = T$.

## 8.3 Interpretation of the syntax

Following [24] we define a partial interpretation function from raw syntax to the CwF with fibrant types given in the previous section.

To interpret the universe rules à la Russell we assume two Grothendieck universes in the underlying set theory, say *tiny* and *small* sets. So that any tiny set is small, and the set of tiny sets is small. For a cubical set $X$ we define $\mathbf{FTy}_0(X)$ and $\mathbf{FTy}_1(X)$ as in the previous section, now referring to tiny and small sets, respectively. We get semantic universes $U_i(I) = \mathbf{FTy}_i(\mathbf{y}I)$ for $i = 0, 1$; we identify those with their lifts to types. As noted above, these lifts carry a composition structure, and thus are fibrant. We also have $U_0 \subseteq U_1$ and thus $\mathrm{Ter}(X; U_0) \subseteq \mathrm{Ter}(X; U_1)$. Note that coding and decoding are, as set-theoretic operations, the same for both universes. We get that $\lceil U_0 \rceil \in \mathrm{Ter}(X; U_1)$ which will serve as the interpretation of $\mathbf{U}$.

In what follows, we define a partial interpretation function of raw syntax: $\llbracket \Gamma \rrbracket$, $\llbracket \Gamma; t \rrbracket$, and $\llbracket \Delta; \sigma \rrbracket$ by recursion on the raw syntax. Since we want to interpret a universe à la Russell we
cannot assume terms and types to have different syntactic categories. The definition is given below and should be read such that the interpretation is defined whenever all interpretations on the right-hand sides are defined and make sense; so, e.g., for $\llbracket \Gamma \rrbracket$. $\mathbf{El} \llbracket \Gamma; A \rrbracket$ below, we require that $\llbracket \Gamma \rrbracket$ is defined and a cubical set, $\llbracket \Gamma; A \rrbracket$ is defined, and $\mathbf{El} \llbracket \Gamma; A \rrbracket \in \mathbf{FTy}(\llbracket \Gamma \rrbracket)$. The interpretation for raw contexts is given by:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
\llbracket () \rrbracket = \top & \llbracket \Gamma, x : A \rrbracket = \llbracket \Gamma \rrbracket. \mathbf{El} \llbracket \Gamma; A \rrbracket & \text{if } x \notin \mathrm{dom}(\Gamma) \\
\llbracket \Gamma, \varphi \rrbracket = \llbracket \Gamma \rrbracket, \llbracket \Gamma; \varphi \rrbracket & \llbracket \Gamma, i : \mathbb{I} \rrbracket = \llbracket \Gamma \rrbracket. \mathbb{I} & \text{if } i \notin \mathrm{dom}(\Gamma)
\end{array}
$$

where $\top$ is a terminal cubical set and in the last equation $\mathbb{I}$ is considered as an element of $\mathbf{Ty}(\llbracket \Gamma \rrbracket)$. When defining $\llbracket \Gamma; t \rrbracket$ we require that $\llbracket \Gamma \rrbracket$ is defined and a cubical set; then $\llbracket \Gamma; t \rrbracket$ is a (partial) family of sets $\llbracket \Gamma; t \rrbracket(I, \rho)$ for $I \in \mathcal{C}$ and $\rho \in \llbracket \Gamma \rrbracket(I)$ (leaving $I$ implicit in the definition). We define:

$$ 
\begin{align*}
\llbracket \Gamma; U \rrbracket &= \lceil U_0 \rceil \in \mathrm{Ter}(\llbracket \Gamma \rrbracket; U_1) \\
\llbracket \Gamma; N \rrbracket &= \lceil N \rceil \in \mathrm{Ter}(\llbracket \Gamma \rrbracket; U_0) \\
\llbracket \Gamma; (x : A) \to B \rrbracket &= \lceil \Pi_{\llbracket \Gamma \rrbracket} (\mathbf{El} \llbracket \Gamma; A \rrbracket, \mathbf{El} \llbracket \Gamma, x : A; B \rrbracket) \rceil \\
\llbracket \Gamma; (x : A) \times B \rrbracket &= \lceil \Sigma_{\llbracket \Gamma \rrbracket} (\mathbf{El} \llbracket \Gamma; A \rrbracket, \mathbf{El} \llbracket \Gamma, x : A; B \rrbracket) \rceil \\
\llbracket \Gamma; \mathrm{Path} A a b \rrbracket &= \lceil \mathrm{Path}_{\mathbf{El} \llbracket \Gamma; A \rrbracket}^{\llbracket \Gamma \rrbracket} (\llbracket \Gamma; a \rrbracket, \llbracket \Gamma; b \rrbracket) \rceil \\
\llbracket \Gamma; \mathrm{Glue} [\varphi \mapsto (T, f)] A \rrbracket &= \lceil \mathrm{Glue}_{\llbracket \Gamma \rrbracket} (\llbracket \Gamma; \varphi \rrbracket, \mathbf{El} \llbracket \Gamma, \varphi; T \rrbracket, \mathbf{El} \llbracket \Gamma; A \rrbracket, \llbracket \Gamma, \varphi; f \rrbracket) \rceil \\
\llbracket \Gamma; \lambda x : A.t \rrbracket &= \lambda_{\llbracket \Gamma \rrbracket; \mathbf{El} \llbracket \Gamma; A \rrbracket} (\llbracket \Gamma, x : A; t \rrbracket) \\
\llbracket \Gamma; t u \rrbracket &= \mathrm{app}(\llbracket \Gamma; t \rrbracket, \llbracket \Gamma; u \rrbracket) \\
\llbracket \Gamma; \langle i \rangle t \rrbracket &= \langle \rangle_{\llbracket \Gamma \rrbracket} \llbracket \Gamma, i : \mathbb{I}; t \rrbracket \\
\llbracket \Gamma; t r \rrbracket &= \llbracket \Gamma; t \rrbracket \llbracket \Gamma; r \rrbracket
\end{align*}
$$

where for path application, juxtaposition on the right-hand side is semantic path application. In the case of a bound variable, we assume that $x$ (respectively $i$) is a chosen variable fresh for $\Gamma$; if this is not possible the expression is undefined. Moreover, all type formers should be read as those on fibrant types, i.e., also defining the composition structure. In the case of Glue, it is understood that the function part, i.e., the fourth argument of Glue in Definition 15 is $\mathfrak{p} \circ \llbracket \Gamma, \varphi; f \rrbracket$ and the required (by Theorem 17) equivalence structure is to be extracted from $\mathfrak{q} \circ \llbracket \Gamma, \varphi; f \rrbracket$ as in Section 5.3. In virtue of the remark in Section 8.2 we don't need type annotations to interpret applications. Note that coding and decoding tacitly refer to $\llbracket \Gamma \rrbracket$ as well. For the rest of the raw terms we also assume we are given $\rho \in \llbracket \Gamma \rrbracket(I)$. Variables are interpreted by:

$$ \llbracket \Gamma, x : A; x \rrbracket \rho = \mathfrak{q}(\rho) \qquad \llbracket \Gamma, x : A; y \rrbracket \rho = \llbracket \Gamma; y \rrbracket (\mathfrak{p}(\rho)) \qquad \llbracket \Gamma, \varphi; y \rrbracket \rho = \llbracket \Gamma; y \rrbracket \rho $$

These should also be read to include the case when $x$ or $y$ are name variables; if $x$ is a name variable, we require $A$ to be $\mathbb{I}$. The interpretations of $\llbracket \Gamma; r \rrbracket \rho$ where $r$ is not a name and $\llbracket \Gamma; \varphi \rrbracket \rho$ follow inductively as elements of $\mathbb{I}$ and $\mathbb{F}$, respectively.

Constants for dependent sums are interpreted by:

$$ \llbracket \Gamma; (t, u) \rrbracket \rho = (\llbracket \Gamma; t \rrbracket \rho, \llbracket \Gamma; u \rrbracket \rho) \qquad \llbracket \Gamma; t.1 \rrbracket \rho = \mathfrak{p}(\llbracket \Gamma; t \rrbracket \rho) \qquad \llbracket \Gamma; t.2 \rrbracket \rho = \mathfrak{q}(\llbracket \Gamma; t \rrbracket \rho) $$

Likewise, constants for $\mathbb{N}$ will be interpreted by their semantic analogues (omitted). The interpretations for the constants related to glueing are

$$ 
\begin{align*}
\llbracket \Gamma; \mathrm{glue} [\varphi \mapsto t] u \rrbracket \rho &= \mathrm{glue}(\llbracket \Gamma; \varphi \rrbracket \rho, \llbracket \Gamma, \varphi; t \rrbracket \hat{\rho}, \llbracket \Gamma; u \rrbracket \rho) \\
\llbracket \Gamma; \mathrm{un glue} [\varphi \mapsto f] u \rrbracket \rho &= \mathrm{un glue}(\llbracket \Gamma; \varphi \rrbracket, \mathfrak{p} \circ \llbracket \Gamma; f \rrbracket)(\rho, \llbracket \Gamma; u \rrbracket \rho)
\end{align*}
$$
where $[[\Gamma, \varphi; t]]\hat{\rho}$ is the family assigning $[[\Gamma, \varphi; t]](\rho f)$ to $J \in \mathcal{C}$ and $f: J \to I$ (and $\rho f$ refers to the restriction given by $[[\Gamma]]$ which is assumed to be a cubical set). Partial elements are interpreted by

$$[[\Gamma; [\varphi_1 u_1, \dots, \varphi_n u_n]]]\rho = [[\Gamma, \varphi_i; u_i]]\rho \quad \text{if } [[\Gamma; \varphi_i]]\rho = 1_F,$$

where for this to be defined we additionally assume that all $[[\Gamma, \varphi_i; u_i]]$ are defined and $[[\Gamma, \varphi_i; u_i]]\rho' = [[\Gamma, \varphi_j; u_j]]\rho'$ for each $\rho' \in [[\Gamma]](I)$ with $[[\Gamma; \varphi_i \wedge \varphi_j]]\rho' = 1_F$.

Finally, the interpretation of composition is given by

$$[[\Gamma; \mathrm{comp}^i A [\varphi \mapsto u] a_0]]\rho = \mathrm{comp}_{\mathrm{El}}[[\Gamma, i; \mathbb{I}; A]](I, j, \rho', [[\Gamma; \varphi]]\rho, [[\Gamma, \varphi, i: \mathbb{I}; u]]\rho', [[\Gamma; a_0]]\rho)$$

if $i \notin \mathrm{dom}(\Gamma)$, and where $j$ is fresh and $\rho' = (\rho s_j, i = j)$ with $s_j: I, j \to I$ induced from the inclusion $I \subseteq I, j$.

The interpretation of raw substitutions $[[\Delta; \sigma]]$ is a (partial) family of sets $[[\Delta; \sigma]](I, \rho)$ for $I \in \mathcal{C}$ and $\rho \in [[\Delta]](I)$. We set

$$[[\Delta; ()]]\rho = *, \quad [[\Delta; (\sigma, x/t)]]\rho = ([[\Delta; \sigma]]\rho, [[\Delta; t]]\rho) \quad \text{if } x \notin \mathrm{dom}(\sigma),$$

where $*$ is the unique element of $\top(I)$. This concludes the definition of the interpretation of syntax.

In the following $\alpha$ stands for either a raw term or raw substitution. In the latter case, $\alpha\sigma$ denotes composition of substitutions.

**Lemma 19.** Let $\Gamma'$ be like $\Gamma$ but with some $\varphi$'s inserted, and assume both $[[\Gamma]]$ and $[[\Gamma']]$ are defined; then:

1. $[[\Gamma']]]$ is a sub-cubical set of $[[\Gamma]]$;

2. if $[[\Gamma; \alpha]]$ is defined, then so is $[[\Gamma'; \alpha]]$ and they agree on $[[\Gamma']]$.

**Lemma 20 (Weakening).** Let $[[\Gamma]]$ be defined.

1. If $[[\Gamma, x : A, \Delta]]$ is defined, then so is $[[\Gamma, x : A, \Delta; x]]$ which is moreover the projection to the $x$-part.<fnref n="5" />

2. If $[[\Gamma, \Delta]]$ is defined, then so is $[[\Gamma, \Delta; \mathrm{id}_\Gamma]]$ which is moreover the projection to the $\Gamma$-part.

3. If $[[\Gamma, \Delta]]$, $[[\Gamma; \alpha]]$ are defined and the variables in $\Delta$ are fresh for $\alpha$, then $[[\Gamma, \Delta; \alpha]]$ is defined and for $\rho \in [[\Gamma, \Delta]](I)$:

$$[[\Gamma; \alpha]]([[\Gamma, \Delta; \mathrm{id}_\Gamma]]\rho) = [[\Gamma, \Delta; \alpha]]\rho$$

**Lemma 21 (Substitution).** For $[[\Gamma]]$, $[[\Delta]]$, $[[\Delta; \sigma]]$, and $[[\Gamma; \alpha]]$ defined with $\mathrm{dom}(\Gamma) = \mathrm{dom}(\sigma)$ (as lists), also $[[\Delta; \alpha\sigma]]$ is defined and for $\rho \in [[\Delta]](I)$:

$$[[\Gamma; \alpha]]([[\Delta; \sigma]]\rho) = [[\Delta; \alpha\sigma]]\rho$$

**Lemma 22.** If $[[\Gamma]]$ is defined and a cubical set, and $[[\Gamma; \alpha]]$ is defined, then $([[(\Gamma; \alpha)]\rho)f = [[\Gamma; \alpha]](\rho f)$.

To state the next theorem let us set $[[\Gamma; \mathbb{I}]] = \Gamma^\top$ and $[[\Gamma; \mathbb{F}]] = \Gamma^\top$ as elements of $\mathrm{Ty}_0([[[\Gamma]]])$.

**Theorem 23 (Soundness).** We have the following implications, and all occurrences of $[[\cdot]]$ in the conclusions are defined. In (3) and (5) we allow $A$ to be $\mathbb{I}$ or $\mathbb{F}$.

<footnote n="5">5 E.g., if $\Gamma$ is $y : B, z : C$, the projection to the $x$-part maps $(b, (c, (a, \delta)))$ to $a$, and the projection to the $\Gamma$-part maps $(b, (c, \delta))$ to $(b, c)$.</footnote>
1. if $\Gamma \vdash$, then $[\Gamma]$ is a cubical set;

2. if $\Gamma \vdash A$, then $[\Gamma; A] \in \text{Ter}([\Gamma]; U_1)$;

3. if $\Gamma \vdash t : A$, then $[\Gamma; t] \in \text{Ter}([\Gamma]; \text{El}([\Gamma; A]))$;

4. if $\Gamma \vdash A = B$, then $[\Gamma; A] = [\Gamma; B]$;

5. if $\Gamma \vdash a = b : A$, then $[\Gamma; a] = [\Gamma; b]$;

6. if $\Gamma \vdash \sigma : \Delta$, then $[\Gamma; \sigma]$ restricts to a natural transformation $[\Gamma] \to [\Delta]$.

# 9 Extensions: Identity Types and Higher Inductive Types

In this section we consider possible extensions to cubical type theory. The first is an identity type defined using path types whose elimination principle holds as a judgmental equality. The second are two examples of higher inductive types.

## 9.1 Identity Types

We can use the path type to represent equalities. Using the composition operation, we can indeed build a substitution function $P(a) \to P(b)$ from any path between $a$ and $b$. However, since we don't have in general the judgmental equality $\text{transp}^i A a_0 = a_0$ if $A$ is independent of $i$ (which is an equality that we cannot expect geometrically in general, as shown in Appendix C), this substitution function does not need to be the constant function when the path is constant. This means that, as in the previous model [6, 13], we don't get an interpretation of Martin-Löf identity type [19] with the standard judgmental equalities.

However, we can define another type which does give an interpretation of this identity type following an idea of Andrew Swan.

### Identity Types

The basic idea of $\text{Id} A a_0 a_1$ is to define it in terms of Path $A a_0 a_1$ but also mark the paths where they are known to be constant. Formally, the formation and introduction rules are

$$ \frac{\Gamma \vdash A \qquad \Gamma \vdash a_0 : A \qquad \Gamma \vdash a_1 : A \quad \Gamma \vdash \omega : \text{Path} A a_0 a_1 [\varphi \mapsto \langle i \rangle a_0]}{\Gamma \vdash \text{Id} A a_0 a_1} \qquad \Gamma \vdash (\omega, \varphi) : \text{Id} A a_0 a_1 $$

and we can define $\text{ra} = (1_a, 1_\mathbb{F}) : \text{Id} A a a$ for $a : A$. The elimination rule, given $\Gamma \vdash a : A$, is

$$ \frac{\Gamma, x : A, \alpha : \text{Id} A a x \vdash C \qquad \Gamma \vdash d : C(x/a, \alpha/ra) \qquad \Gamma \vdash b : A \qquad \Gamma \vdash \beta : \text{Id} A a b}{\Gamma \vdash J_{x,\alpha,C} d b \beta : C(x/b, \alpha/\beta)} $$

together with the following judgmental equality in case $\beta$ is of the form $(\omega, \varphi)$

$$ J d b \beta = \text{comp}^i C(x/\omega i, \alpha/\beta^*(i)) [\varphi \mapsto d] d $$

where $\Gamma, i : \mathbb{I} \vdash \beta^*(i) : \text{Id} A a (\omega i)$ is given by

$$ \beta^*(i) = (\langle j \rangle \omega (i \wedge j), \varphi \vee (i = 0)). $$

Note that with this definition we get $J d a (ra) = d$ as desired.

The composition operation for $\text{Id}$ is explained as follows. Given $\Gamma, i : \mathbb{I} \vdash \text{Id} A a_0 a_1$, $\Gamma, \varphi, i : \mathbb{I} \vdash (\omega, \psi) : \text{Id} A a_0 a_1$, and $\Gamma \vdash (\omega_0, \psi_0) : (\text{Id} A a_0 a_1)(i0)[\varphi \mapsto (\omega(i0), \psi(i0))]$ we have the judgmental equality

$$ \text{comp}^i (\text{Id} A a_0 a_1) [\varphi \mapsto (\omega, \psi)] (\omega_0, \psi_0) = (\text{comp}^i (\text{Path} A a_0 a_1) [\varphi \mapsto \omega] \omega_0, \varphi \wedge \psi(i1)). $$
It can then be shown that the types `Id A a b` and `Path A a b` are (Path)-equivalent. In particular, a type is (Path)-contractible if, and only if, it is (Id)-contractible. The univalence axiom, proved in Section 7.2 for the Path-type, hence holds as well for the Id-type.<fnref n="6" />

## Cofibration-Trivial Fibration Factorization

The same idea can be used to factorize an arbitrary map of (not necessary fibrant) cubical sets $f : A \to B$ into a cofibration followed by a trivial fibration. We define a “trivial fibration” to be a first projection from a total space of a contractible family of types and a “cofibration” to be a map that has the left lifting property against any trivial fibration. For this we define, for $b : B$, the type $T_f(b)$ to be the type of elements $[\varphi \mapsto a]$ with $\varphi \vdash a : A$ and $\varphi \vdash f a = b : B$.

**► Theorem 24.** The type $T_f(b)$ is contractible and the map

$$A \to (b : B) \times T_f(b), \quad a \mapsto (f a, [1_F \mapsto a])$$

is a cofibration.

The definition of the identity type can be seen as a special case of this, if we take the $B$ the type of paths in $A$ and for $f$ the constant path function.

## 9.2 Higher Inductive Types

In this section we consider the extension of cubical type theory with two different higher inductive types: spheres and propositional truncation. The presentation in this section is syntactical, but it can be directly translated into semantic definitions.

### Extension to Dependent Path Types

In order to formulate the elimination rules for higher inductive types, we need to extend the path type to *dependent path type*, which is described by the following rules. If $i : \mathbb{I} \vdash A$ and $\vdash a_0 : A(i_0)$, $a_1 : A(i_1)$, then $\vdash \mathit{Path}^i A a_0 a_1$. The introduction rule is that $\vdash \langle i \rangle t : \mathit{Path}^i A t(i_0) t(i_1)$ if $i : \mathbb{I} \vdash t : A$. The elimination rule is $\vdash p r : A(i/r)$ if $\vdash p : \mathit{Path}^i A a_0 a_1$ with equalities $p 0 = a_0 : A(i_0)$ and $p 1 = a_1 : A(i_1)$.

### Spheres

We define the circle, $S^1$, by the rules:

$$\frac{\Gamma \vdash \quad \Gamma \vdash \quad \Gamma \vdash r : \mathbb{I}}{\Gamma \vdash S^1 \quad \Gamma \vdash \text{base} : S^1 \quad \Gamma \vdash \text{loop}(r) : S^1}$$

with the equalities $\text{loop}(0) = \text{loop}(1) = \text{base}$.

Since we want to represent the *free* type with one base point and a loop, we add composition as a *constructor* operation $\mathit{hcomp}^i$:

$$\frac{\Gamma, \varphi, i : \mathbb{I} \vdash u : S^1 \quad \Gamma \vdash u_0 : S^1[\varphi \mapsto u(i_0)]}{\Gamma \vdash \mathit{hcomp}^i [\varphi \mapsto u] u_0 : S^1}$$

with the equality $\mathit{hcomp}^i [1_F \mapsto u] u_0 = u(i_1)$.

<footnote n="6">⁶ This has been formally verified using the HASKELL implementation: https://github.com/mortberg/cubicaltt/blob/v1.0/examples/idtypes.ctt</footnote>
5:26 Cubical Type Theory

Given a dependent type $x : S^1 \vdash A$ and $a : A(x/\text{base})$ and $l : \text{Path}^i A(x/\text{loop}(i))$ we can define a function $g : (x : S^1) \to A$ by the equations$^7 g_{\text{base}} = a$ and $g_{\text{loop}}(r) = l r$ and

$$g (\text{hcomp}^i [\varphi \mapsto u] u_0) = \text{comp}^i A(x/v) [\varphi \mapsto g u] (g u_0)$$

where $v = \text{fill}^i S^1 [\varphi \mapsto u] u_0 = \text{hcomp}^j [\varphi \mapsto u(i/i \wedge j), (i=0) \mapsto u_0] u_0$.

This definition is non ambiguous since $l=0 = l=1 = a$.

We have a similar definition for $S^n$ taking as constructors base and loop($r_1, \dots, r_n$).

Propositional Truncation

We define the propositional truncation, $\text{inh} A$, of a type $A$ by the rules:

$$\frac{\Gamma \vdash A \qquad \Gamma \vdash a : A \qquad \Gamma \vdash u_0 : \text{inh } A \qquad \Gamma \vdash u_1 : \text{inh } A \qquad \Gamma \vdash r : \mathbb{I}}{\Gamma \vdash \text{inh } A \qquad \Gamma \vdash \text{inc } a : \text{inh } A \qquad \Gamma \vdash \text{squash}(u_0, u_1, r) : \text{inh } A}$$

with the equalities $\text{squash}(u_0, u_1, 0) = u_0$ and $\text{squash}(u_0, u_1, 1) = u_1$.

As before, we add composition as a constructor, but only in the form$^8$

$$\frac{\Gamma, \varphi, i : \mathbb{I} \vdash u : \text{inh } A \qquad \Gamma \vdash u_0 : \text{inh } A[\varphi \mapsto u(i_0)]}{\Gamma \vdash \text{hcomp}^i [\varphi \mapsto u] u_0 : \text{inh } A}$$

with the equality $\text{hcomp}^i [1_{\mathbb{F}} \mapsto u] u_0 = u(i_1)$.

This provides only a definition of $\text{comp}^i$ ($\text{inh } A$) $[\varphi \mapsto u] u_0$ in the case where $A$ is independent of $i$, and we have to explain how to define the general case.

In order to do this, we define first two operations

$$\frac{\Gamma, i : \mathbb{I} \vdash A \qquad \Gamma \vdash u_0 : \text{inh } A(i_0)}{\Gamma \vdash \text{transp } u_0 : \text{inh } A(i_1)} \qquad \frac{\Gamma, i : \mathbb{I} \vdash A \qquad \Gamma, i : \mathbb{I} \vdash u : \text{inh } A}{\Gamma \vdash \text{squeeze}^i u : \text{Path} (\text{inh } A(i_1)) (\text{transp } u(i_0)) u(i_1)}$$

by the equations

$\text{transp} (\text{inc } a) \quad = \quad \text{inc} (\text{comp}^i A [] a)$

$\text{transp} (\text{squash}(u_0, u_1, r)) \quad = \quad \text{squash}(\text{transp } u_0, \text{transp } u_1, r)$

$\text{transp} (\text{hcomp}^j [\varphi \mapsto u] u_0) \quad = \quad \text{hcomp}^j [\varphi \mapsto \text{transp } u] (\text{transp } u_0)$

$\text{squeeze}^i (\text{inc } a) \quad = \quad \langle i \rangle \text{inc} (\text{comp}^j A(i \vee j) [(i=1) \mapsto a(i_1)] a)$

$\text{squeeze}^i (\text{squash}(u_0, u_1, r)) \quad = \quad \langle k \rangle \text{squash}(\text{squeeze}^i u_0 k, \text{squeeze}^i u_1 k, r(i/k))$

$\text{squeeze}^i (\text{hcomp}^j [\varphi \mapsto u] v) \quad = \quad \langle k \rangle \text{hcomp}^j S (\text{squeeze}^i v k)$

where $S$ is the system

$$[\delta \mapsto \text{squeeze}^i u k, \varphi(i/k) \wedge (k=0) \mapsto \text{transp } u(i_0), \varphi(i/k) \wedge (k=1) \mapsto u(i_1)]$$

and $\delta = \forall i.\varphi$, using Lemma 2.

Using these operations, we can define the general composition

$$\frac{\Gamma, i : \mathbb{I} \vdash A \qquad \Gamma, \varphi, i : \mathbb{I} \vdash u : \text{inh } A \qquad \Gamma \vdash u_0 : \text{inh } A(i_0)[\varphi \mapsto u(i_0)]}{\Gamma \vdash \text{comp}^i (\text{inh } A) [\varphi \mapsto u] u_0 : \text{inh } A(i_1)[\varphi \mapsto u(i_1)]}$$

<footnote>$^7$ For the equation $g \text{loop}(r) = l r$, it may be that $l$ and $r$ are dependent on the same name $i$, and we could not have followed this definition in the framework of [6].</footnote>

<footnote>$^8$ This restriction on the constructor is essential for the justification of the elimination rule below.</footnote>
by $\Gamma \vdash \text{comp}^i (\text{inh } A) [\varphi \mapsto u] u_0 = \text{hcomp}^j [\varphi \mapsto \text{squeeze}^i u j] (\text{transp } u_0) : \text{inh } A(i1)$.

Given $\Gamma \vdash B$ and $\Gamma \vdash q : (x y : B) \rightarrow \text{Path } B x y$ and $f : A \rightarrow B$ we define $g : \text{inh } A \rightarrow B$ by the equations

$$ 
\begin{align*}
g (\text{inc } a) &= f a \\
g (\text{squash}(u_0, u_1, r)) &= q (g u_0) (g u_1) r \\
g (\text{hcomp}^j [\varphi \mapsto u] u_0) &= \text{comp}^j B [\varphi \mapsto g u] (g u_0)
\end{align*}
$$

## 10 Related and Future Work

Cubical ideas have proved useful to reason about equality in homotopy type theory [18]. In cubical type theory these techniques could be simplified as there are new judgmental equalities and better notations for manipulating higher dimensional cubes. Indeed some simple experiments using the HASKELL implementation have shown that we can simplify some constructions in synthetic homotopy theory.<fnref n="9" />

Other approaches to extending intensional type theory with extensionality principles can be found in [2, 23]. These approaches have close connections to techniques for internalizing parametricity in type theory [5]. Further, nominal extensions to λ-calculus and semantical ideas related to the ones presented in this paper have recently also proved useful for justifying type theory with internalized parametricity [4].

The paper [11] provides a general framework for analyzing the uniformity condition, which applies to simplicial and cubical sets.

Large parts of the semantics presented in this paper have been formally verified in NuPrl by Mark Bickford<fnref n="10" />, in particular, the definition of Kan filling in terms of composition as in Section 4.4 and composition for glueing as given in Section 6.2.

Following the usual reducibility method, we expect it to be possible to adapt our presheaf semantics to a proof of normalization and decidability of type checking. A first step in this direction is the proof of canonicity in [14]. We end the paper with a list of open problems and conjectures:

1. Extend the semantics of identity types to the semantics of inductive families.

2. Give a general syntax and semantics of higher inductive types.

3. Extend the system with resizing rules and show normalization.

4. Is there a model where Path and Id coincide?

**Acknowledgements.** This work originates from discussions between the authors around an implementation of a type system corresponding to the model described in [6]. This implementation indicated a problem with the representation of higher inductive types, e.g., the elimination rule for the circle, and suggested the need of extending this cubical model with a diagonal operation. The general framework (uniformity condition, connections, semantics of spheres and propositional truncation) is due to the second author. In particular, the glueing operation with its composition was introduced as a generalization of the operation described in [6] transforming an equivalence into a path, and with the condition $A = \text{Glue} [] A$. In a first attempt, we tried to force “regularity”, i.e., the equation $\text{transp } i A a_0 = a_0$ if A is independent of i (which seemed to be necessary in order to get filling from compositions, and which implies $\text{Path} = \text{Id}$). There was a problem however for getting regularity for the

<footnote n="9">⁹ For details see: https://github.com/mortberg/cubicaltt/tree/master/examples/</footnote>

<footnote n="10">¹⁰For details see: http://www.nuprl.org/wip/Mathematics/cubical!type!theory/</footnote>
universe, that was discovered by Dan Licata (from discussions with Carlo Angiuli and Bob Harper). Thanks to this discovery, it was realized that regularity is actually not needed for the model to work. In particular, the second author adapted the definition of filling from composition as in Section 4.4, the third author noticed that we can remove the condition $A = \text{Glue } [] A$, and together with the last author, they derived the univalence axiom from the glueing operation as presented in the appendix. This was surprising since glueing was introduced a priori only as a way to transform equivalences into paths, but was later explained by a remark of Dan Licata (also presented in the appendix: we get univalence as soon as the transport map associated to this path is path equal to the given equivalence). The second author introduced then the restriction operation $\Gamma, \varphi$ on contexts, which, as noticed by Christian Sattler, can be seen as an explicit syntax for the notion of cofibration, and designed the other proof of univalence in Section 7.2 from discussions between Nicola Gambino, Peter LeFanu Lumsdaine and the third author. Not having regularity, the type of paths is not the same as the `Id` type but, as explained in Section 9.1, we can recover the usual identity type from the path type, following an idea of Andrew Swan.

The authors would like to thank the referees and Martín Escardó, Georges Gonthier, Dan Grayson, Peter Hancock, Dan Licata, Peter LeFanu Lumsdaine, Christian Sattler, Andrew Swan, Vladimir Voevodsky for many interesting discussions and remarks.

References

1. Peter Aczel. On relating type theories and set theories. In Thorsten Altenkirch, Wolfgang Naraschewski, and Bernhard Reus, editors, *Types for Proofs and Programs, International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers*, volume 1657 of *Lecture Notes in Computer Science*, pages 1-18. Springer, 1998. doi:10.1007/3-540-48167-2_1.

2. T. Altenkirch. Extensional equality in intensional type theory. In *Proc. of 14th Ann. IEEE Symp. on Logic in Computer Science, LICS '99*, pages 412-420. IEEE, 1999. doi:10.1109/lics.1999.782636.

3. R. Balbes and P. Dwinger. *Distributive Lattices*. University of Missouri Press, 1974. Reprinted by Abstract Space Publishing in 2011.

4. Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. A presheaf model of parametric type theory. *Electr. Notes Theor. Comput. Sci.*, 319:67-82, 2015. doi:10.1016/j.entcs.2015.12.006.

5. Jean-Philippe Bernardy and Guilhem Moulin. Type-theory in color. In Greg Morrisett and Tarmo Uustalu, editors, *ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013*, pages 61-72. ACM, 2013. doi:10.1145/2500365.2500577.

6. M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In R. Matthes and A. Schubert, editors, *Proc. of 19th Int. Conf. on Types for Proofs and Programs, TYPES 2013*, volume 26 of *Leibniz Int. Proc. in Inform.*, pages 107-128. Dagstuhl Publishing, 2014. doi:10.4230/lipics.types.2013.107.

7. R. Brown, P. J. Higgins, and R. Sivera. *Nonabelian Algebraic Topology: Filtered Spaces, Crossed Complexes, Cubical Homotopy Groupoids*, volume 15 of *EMS Tracts in Mathematics*. Europ. Math. Soc., 2011. doi:10.4171/083.

8. D.-C. Cisinski. Univalent universes for elegant models of homotopy types, 2014. arXiv preprint 1406.0058. URL: https://arxiv.org/abs/1406.0058.

9. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, *Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers*, volume 1158 of *Lecture Notes in Computer Science*, pages 120-134. Springer, 1995. doi:10.1007/3-540-61780-9_66.
10 M. Fourman and D. Scott. Sheaves and logic. In M. Fourman, C. Mulvey, and D. Scott, editors, *Applications of Sheaves*, volume 753 of *Lect. Notes in Math.*, pages 302–401. Springer, 1979. doi:10.1007/bfb0061824.

11 N. Gambino and C. Sattler. Uniform fibrations and the Frobenius condition, 2015. arXiv preprint 1510.00669. URL: https://arxiv.org/abs/1510.00669.

12 M. Hofmann. Syntax and semantics of dependent types. In A. M. Pitts and P. Dybjer, editors, *Semantics and Logics of Computation*, volume 14 of *Publications of the Newton Institute*, pages 79–130. Cambridge University Press, 1997. doi:10.1017/cbo9780511526619.004.

13 S. Huber. *A Model of Type Theory in Cubical Sets*. Licentiate thesis, University of Gothenburg, 2015. URL: http://www.cse.chalmers.se/~simonhu/misc/lic.pdf.

14 S. Huber. Canonicity for cubical type theory, 2016. arXiv preprint 1607.04156. URL: https://arxiv.org/abs/1607.04156.

15 J. A. Kalman. Lattices with involution. *Trans. Amer. Math. Soc.*, 87:485–491, 1958. doi:10.1090/s0002-9947-1958-0095135-x.

16 D. M. Kan. Abstract homotopy I. *Proc. Nat. Acad. Sci. USA*, 41(12):1092–1096, 1955. URL: http://www.pnas.org/content/41/12/1092.full.pdf.

17 C. Kapulkin and P. LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky), 2012. arXiv preprint 1211.2851. URL: https://arxiv.org/abs/1211.2851.

18 D. R. Licata and G. Brunerie. A cubical approach to synthetic homotopy theory. In *Proc. of 30th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS '15*, pages 92–103. IEEE, 2015. doi:10.1109/lics.2015.19.

19 P. Martin-Löf. An intuitionistic theory of types: Predicative part. In *Logic Colloquium '73*, volume 80 of *Studies in Logic and the Foundations of Mathematics*, pages 73–118. North Holland, 1975. doi:10.1016/s0049-237x(08)71945-1.

20 P. Martin-Löf. An intuitionistic theory of types. In G. Sambin and J. M. Smith, editors, *Twenty-Five Years of Constructive Type Theory*, volume 36 of *Oxford Logic Guides*, pages 127–172. Clarendon Press, 1998.

21 A. M. Pitts. *Nominal Sets: Names and Symmetry in Computer Science*, volume 57 of *Cambridge Tracts in Theoretical Computer Science*. Cambridge University Press, 2013. doi:10.1017/cbo9781139084673.

22 A. M. Pitts. Nominal presentation of cubical sets models of type theory. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, *Proc. of 20th Int. Conf. on Types for Proofs and Programs, TYPES 2014*, volume 39 of *Leibniz Int. Proc. in Inform.*, pages 202–220. Dagstuhl Publishing, 2015. doi:10.4230/lipics.types.2014.202.

23 A. Polonsky. Extensionality of $\lambda*$. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, *Proc. of 20th Int. Conf. on Types for Proofs and Programs, TYPES 2014*, volume 39 of *Leibniz Int. Proc. in Inform.*, pages 221–250. Dagstuhl Publishing, 2015. doi:10.4230/lipics.types.2014.221.

24 T. Streicher. *Semantics of Type Theory: Correctness, Completeness and Independence Results*. Progress in Theoretical Computer Science. Birkhäuser, 1991. doi:10.1007/978-1-4612-0433-6.

25 A. Swan. An algebraic weak factorisation system on 01-substitution sets: A constructive proof, 2014. arXiv preprint 1409.1829. URL: https://arxiv.org/abs/1409.1829.

26 The Univalent Foundations Program. *Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.

27 V. Voevodsky. The equivalence axiom and univalent models of type theory (talk at CMU on feb. 4, 2010), 2014. arXiv preprint 1402.5556. URL: https://arxiv.org/abs/1402.5556.
<figure><img src="image_8.png" /><figcaption>Figure 5 Composition for glueing.</figcaption></figure>

**A** Details of Composition for Glueing

We build the element $\Gamma \vdash b_1 = \text{comp}^i B [\psi \mapsto b] b_0 : (\text{Glue} [\varphi \mapsto (T, f)] A)(i1)$ as the element glue $[\varphi(i1) \mapsto t_1] a_1$ where

$$ \Gamma, \varphi(i1) \vdash t_1 : T(i1)[\psi \mapsto b(i1)] $$

$$ \Gamma \vdash a_1 : A(i1)[\varphi(i1) \mapsto f(i1) t_1, \psi \mapsto (\text{unglue } b)(i1)] $$

As intermediate steps, we gradually build elements that satisfy more and more of the equations that the final elements $t_1$ and $a_1$ should satisfy. The construction of these is given in five steps.

Before explaining how we can define them and why they are well defined, we illustrate the construction in Figure 5, with $\psi = (j = 1)$ and $\varphi = (i = 0) \lor (j = 1) \lor (i = 1)$.

We pose $\delta = \forall i.\varphi$ (cf. Section 3), so that we have that $\delta$ is independent from $i$, and in our example $\delta = (j = 1)$ and it represents the right-hand side of the picture.

1. The element $a'_1 : A(i1)$ is a first approximation of $a_1$, but $a'_1$ is not necessarily in the image of $f(i1)$ in $\Gamma, \varphi(i1)$;

2. the partial element $\delta \vdash t'_1 : T(i1)$, which is a partial final result for $\varphi(i1) \vdash t_1$;

3. the partial path $\delta \vdash \omega$, between $a'_1$ and the image of $t'_1$;

4. both the final element $\varphi(i1) \vdash t_1$ and a path $\varphi(i1) \vdash \alpha$ between $a'_1$ and $f(i1) t_1$;

5. finally, we build $a_1$ from $a'_1$ and $\alpha$.

We define:

$$ \Gamma, \psi, i : \mathbb{I} \vdash a = \text{unglue } b : A[\varphi \mapsto f b] $$

$$ \Gamma \vdash a_0 = \text{unglue } b_0 : A(i0)[\varphi(i0) \mapsto f(i0) b_0, \psi \mapsto a(i0)] $$

**Step 1** We define $a'_1$ as the composition of $a$ and unglue $b_0$, in the direction $i$, which is well defined since unglue $b_0 = (\text{unglue } b)(i0)$ over the extent $\psi$

$$ \Gamma \vdash a'_1 = \text{comp}^i A [\psi \mapsto a] a_0 : A(i1)[\psi \mapsto a(i1)] \quad (4) $$
**Step 2** We also define $t'_1$ as the composition of $b$ and $b_0$, in the direction $i$:

$$ \Gamma, \delta \vdash t'_1 = \mathbf{comp}^i T [\psi \mapsto b] b_0 : T(i1)[\psi \mapsto b(i1)] \quad (5) $$

$$ \text{which is well defined because} \quad \begin{cases} \Gamma, \delta, i : \mathbb{I}, \psi \vdash b : T & \text{by Lemma 3} \\ \Gamma, \delta \vdash b_0 : T(i0)[\psi \mapsto b(i0)] & \text{as } \delta \le \varphi(i0) \end{cases} $$

Moreover, since

$$ \left\{ \begin{array}{ll} \Gamma, \delta, \psi, i : \mathbb{I} \vdash a = f b & \text{by } \delta \le \varphi \\ \Gamma, \delta \vdash a_0 = f(i0) b_0 & \text{by } \delta \le \varphi(i0) \end{array} \right. $$

we can re-express $a'_1$ on the extent $\delta$

$$ \Gamma, \delta \vdash a'_1 = \mathbf{comp}^i A [\psi \mapsto f b] (f(i0) b_0) $$

**Step 3** We can hence find a path $\omega$ connecting $a'_1$ and $f(i1)$ $t'_1$ in $\Gamma, \delta$ using Lemma 6:

$$ \Gamma, \delta \vdash \omega = \mathbf{pres}^i f [\psi \mapsto b] b_0 : (\mathbf{Path} A(i1) a'_1 (f(i1) t'_1)) [\psi \mapsto \langle j \rangle a(i1)] $$

Picking a fresh name $j$, we have

$$ \Gamma, \delta, j : \mathbb{I} \vdash \omega j : A(i1)[(j = 0) \mapsto a'_1, (j = 1) \mapsto f(i1) t'_1, \psi \mapsto a(i1)] \quad (6) $$

**Step 4** Now we define the final element $t_1$ as the inverse image of $a'_1$ by $f(i1)$, together with the path $\alpha$ between $a'_1$ and $f(i1)$ $t_1$, in $\Gamma, \varphi(i1) \vdash$, using Lemma 7:

$$ \Gamma, \varphi(i1) \vdash (t_1, \alpha) = \mathbf{equiv} f(i1) [\delta \mapsto (t'_1, \omega), \psi \mapsto (b(i1), \langle j \rangle a'_1)] a'_1 $$

$$ \text{with} \quad \begin{cases} \Gamma, \varphi(i1) \vdash t_1 : T(i1)[\delta \mapsto t'_1, \psi \mapsto b(i1)] \\ \Gamma, \varphi(i1) \vdash \alpha : (\mathbf{Path} A(i1) a'_1 (f(i1) t_1)) [\delta \mapsto \omega, \psi \mapsto \langle j \rangle a'_1] \end{cases} $$

These are well defined because the two systems in $\delta$ and $\psi$ are compatible:

$$ \left\{ \begin{array}{ll} \Gamma, \delta, \psi \vdash t'_1 = b(i1) & \text{by (5)} \\ \Gamma, \delta, \psi \vdash \omega = \langle j \rangle a'_1 & \text{by (6) and (4)} \end{array} \right. $$

Picking a fresh name $j$, we have

$$ \Gamma, \varphi(i1), j : \mathbb{I} \vdash \alpha j : A(i1)[(j = 0) \mapsto a'_1, (j = 1) \mapsto f(i1) t_1, \delta \mapsto a'_1, \psi \mapsto a(i1)] \quad (7) $$

**Step 5** Finally, we define $a_1$ by composition of $\alpha$ and $a'_1$:

$$ \Gamma \vdash a_1 := \mathbf{comp}^j A(i1) [\varphi(i1) \mapsto \alpha j, \psi \mapsto a(i1)] a'_1 : A(i1)[\varphi(i1) \mapsto \alpha 1, \psi \mapsto a(i1)] $$

$$ \text{which is well defined because} \quad \begin{cases} \Gamma, j : \mathbb{I}, \varphi(i1), \psi \vdash \alpha j = a(i1) & \text{by (7)} \\ \Gamma, \varphi(i1) \vdash \alpha 0 = a'_1 & \text{by (7)} \\ \Gamma, \psi \vdash a(i1) = a'_1 & \text{by (4)} \end{cases} $$

and since $\Gamma, \varphi(i1) \vdash \alpha 1 = f(i1) t_1$, we can re-express the type of $a_1$ in the following way:

$$ \Gamma \vdash a_1 : A(i1)[\varphi(i1) \mapsto f(i1) t_1, \psi \mapsto a(i1)] $$
Which is exactly what we needed to build $\Gamma \vdash b_1 := \text{glue} [\varphi(i1) \mapsto t_1] a_1 : B(i1)[\psi \mapsto b(i1)]$.

Finally we check that $b_1 = \text{comp}^i T [\psi \mapsto b] b_0$ on $\delta$:

$$ 
\begin{align*}
b_1 &= \text{glue} [\varphi(i1) \mapsto t_1] a_1 && \text{by def.} \\
&= t_1 : T(i1)[\delta \mapsto t'_1, \psi \mapsto b(i1)] && \text{as } \varphi(i1) = 1_F \\
&= t'_1 && \text{as } \delta = 1_F \\
&= \text{comp}^i T [\psi \mapsto b] b_0 && \text{by def.}
\end{align*}
$$

**B Univalence from Glueing**

We also give two alternative proofs of the univalence axiom for Path only involving the glue construction.<fnref n="11" /> The first is a direct proof of the standard formulation of the univalence axiom while the second goes through an alternative formulation as in Corollary 10.<fnref n="12" />

**Lemma 25.** For $\Gamma \vdash A : U$, $\Gamma \vdash B : U$, and an equivalence $\Gamma \vdash f : \text{Equiv } A B$ we have the following constructions:

1. $\Gamma \vdash \text{eqToPath } f : \text{Path } U A B$;

2. $\Gamma \vdash \text{Path } (A \to B) (\text{transp}^i(\text{eqToPath } f i))$ f.1 is inhabited; and

3. if $f = \text{equiv}^i(P i)$ for $\Gamma \vdash P : \text{Path } U A B$, then the following type is inhabited:

$$ \Gamma \vdash \text{Path } (\text{Path } U A B) (\text{eqToPath } (\text{equiv}^i(P i))) P $$

**Proof.** For (1) we define

$$ \text{eqToPath } f = \langle i \rangle \text{ Glue} [(i = 0) \mapsto (A, f), (i = 1) \mapsto (B, \text{equiv}^k B)] B. \qquad (8) $$

Note that here $\text{equiv}^k B$ is an equivalence between $B$ and $B$ (see Section 7.1). For (2) we have to closely look at how the composition was defined for Glue. By unfolding the definition, we see that the left-hand side of the equality is equal f.1 composed with multiple transports in a constant type; using filling and functional extensionality, these transports can be shown to be equal to the identity; for details see the formal proof.

The term for (3) is given by:

$$ 
\begin{align*}
\langle j \rangle \langle i \rangle \text{ Glue} [(i = 0) &\mapsto (A, \text{equiv}^k(P k)), \\
(i = 1) &\mapsto (B, \text{equiv}^k B), \\
(j = 1) &\mapsto (P i, \text{equiv}^k(P(i \vee k)))] \\
B &
\end{align*}
$$

**Corollary 26 (Univalence axiom).** For the canonical map

$$ \text{pathToEq} : (A B : U) \to \text{Path } U A B \to \text{Equiv } A B $$

we have that $\text{pathToEq } A B$ is an equivalence for all $A : U$ and $B : U$.

<footnote n="11">¹¹ The proofs of the univalence axiom have all been formally verified inside the system using the HASKELL implementation. We note that the proof of Theorem 9 can be given such that it extends f.2 and hence in Corollary 10 we do not need the fact that isEquiv X A f.1 is a proposition. For details see: https://github.com/mortberg/cubicaltt/blob/v1.0/examples/univalence.ctt</footnote>

<footnote n="12">¹² The second of these proofs is inspired by a proof by Dan Licata from: https://groups.google.com/d/msg/homotopytypetheory/j2KBIvDw53s/YTDK4D0NFQAJ</footnote>
**Proof 1.** Let us first show that the canonical map pathToEq is path equal to:

$$ \text{equiv} = \lambda A B : U. \lambda P : \text{Path} U A B. \text{equiv}^i(P i) $$

By function extensionality, it suffices to check this pointwise. Using path-induction, we may assume that $P$ is convexity. In this case pathToEq $A A 1_A$ is the identity equivalence by definition. Because being an equivalence is a proposition, it thus suffices that the first component of $equiv^i A$ is propositionally equal to the identity. By definition, this first component is given by transport (now in the constant type $A$) which is easily seen to be the identity using filling (see Section 4.4).

Thus it suffices to prove that $equiv A B$ is an equivalence. To do so it is enough to give an inverse (see Theorems 4.2.3 and 4.2.6 of [26]). But eqToPath is a left inverse by Lemma 25 (3), and a right inverse by Lemma 25 (2) using that being an equivalence is a proposition. ◀

**Proof 2.** Points (1) and (2) of Lemma 25 imply that $\text{equiv} A B$ is a retract of $\text{Path} U A B$. Hence $(X : U) \times \text{equiv} A X$ is a retract of $(X : U) \times \text{Path} U A X$. But $(X : U) \times \text{Path} U A X$ is contractible, so $(X : U) \times \text{equiv} A X$ is also contractible as a retract of a contractible type. As discussed in Section 7.2 this is an alternative formulation of the univalence axiom and the rest of this proof follows as there. ◀

Note that the first proof uses all three of the points of Lemma 25 while the second proof only uses the first two. As the second proof only uses the first two points it is possible to prove it if point (1) is defined as in Example 8 leading to a slightly simpler proof of point (2).

# C Singular Cubical Sets

Recall the functor $C \to \text{Top}$, $I \mapsto [0, 1]^I$ given at (1) in Section 8.1. In particular, the face maps $(ib): I - i \to I$ (for $b = 0_{\mathbb{I}}$ or $1_{\mathbb{I}}$) induce the maps $(ib): [0, 1]^{I-i} \to [0, 1]^I$ by $i(ib)u = b$ and $j(ib)u = ju$ if $j \neq i$ is in $I$. If $\psi$ is in $\mathbb{F}(I)$ and $u$ in $[0, 1]^I$, then $\psi u$ is a truth value.

We assume given a family of idempotent functions $r_I: [0, 1]^I \times [0, 1] \to [0, 1]^I \times [0, 1]$ such that

1. $r_I(u, z) = (u, z)$ iff $\partial_I u = 1$ or $z = 0$, and

2. for any strict $f$ in $\text{Hom}(I, J)$ we have $r_J(f \times \text{id})r_I = r_J(f \times \text{id})$.

Such a family can for instance be defined as in the following picture ("retraction from above center"). If the center has coordinate $(1/2, 2)$, then $r_I(u, z) = r_I(u', z')$ is equivalent to $(2 - z')( -1 + 2u) = (2 - z)( -1 + 2u')$.

<figure><img src="image_9.png" /></figure>

Property (1) holds for the retraction defined by this picture. The property (2) can be reformulated as $r_I(u, z) = r_I(u', z') \to r_J(fu, z) = r_J(fu', z')$. It also holds in this case,
5:34 Cubical Type Theory

since $r_I(u, z) = r_I(u', z')$ is then equivalent to $(2-z')(-1+2u) = (2-z)(-1+2u')$, which implies $(2-z')(-1+2fu) = (2-z)(-1+2fu')$ if $f$ is strict.

Using this family, we can define for each $\psi$ in $\mathbb{F}(I)$ an idempotent function

$$r_{\psi} : [0, 1]^I \times [0, 1] \to [0, 1]^I \times [0, 1]$$

having for fixed-points the element $(u, z)$ such that $\psi u = 1$ or $z = 0$. This function $r_{\psi}$ is completely characterized by the following properties:

1. $r_{\psi} = \mathrm{id}$ if $\psi = 1$

2. $r_{\psi} = r_{\psi}r_I$ if $\psi \neq 1$

3. $r_{\psi}(u, z) = (u, z)$ if $z = 0$

4. $r_{\psi}((ib) \times \mathrm{id}) = ((ib) \times \mathrm{id})r_{\psi}(ib)$

These properties imply for instance $r_{\partial_I}(u, z) = (u, z)$ if $\partial_I u = 1$ or $z = 0$ and so they imply $r_{\partial_I} = r_I$. They also imply that $r_{\psi}(u, z) = (u, z)$ if $\psi u = 1$.

From these properties, we can prove the uniformity of the family of functions $r_{\psi}$.

**Theorem 27.** If $f$ is in $\mathrm{Hom}(I, J)$ and $\psi$ is in $\mathbb{F}(J)$, then $r_{\psi}(f \times \mathrm{id}) = (f \times \mathrm{id})r_{\psi f}$.

This is proved by induction on the number of element of $I$ (the result being clear if $I$ is empty).

A particular case is $r_J(f \times \mathrm{id}) = (f \times \mathrm{id})r_{\partial_J f}$. Note that, in general, $\partial_J f$ is not $\partial_I$.

A direct consequence of the previous theorem is the following.

**Corollary 28.** The singular cubical set associated to a topological space has a composition structure.