# Model structure on the universe in a two level type theory

Simon Boulier, Nicolas Tabareau

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

To cite this version:

Simon Boulier, Nicolas Tabareau. Model structure on the universe in a two level type theory. 2017. [hal-01579822](https://hal.science/hal-01579822)

HAL Id: hal-01579822

https://hal.science/hal-01579822

Preprint submitted on 31 Aug 2017

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Model structure on the universe in a two level type theory

Simon Boulier¹ and Nicolas Tabareau²

1 IMT Atlantique

2 Inria, Nantes

## Abstract

There is an on-going connection between type theory and homotopy theory, based on the similarity between types and the notion of homotopy types for topological spaces. This idea has been made precise by exhibiting the category `cSet` of cubical sets as a model of homotopy type theory. It is natural to wonder, conversely, to what extend this model can be reflected in a type theory. The homotopy structure of `cSet` is given by a model structure; that is, a definition of three classes of maps—fibrations, cofibrations and weak equivalences—satisfying various properties. In this article, we internalize the notion of model structure in Martin-Löf type theory with a strict equality and formalize a model structure on the category of fibrant types in a type theory with two equalities (à la Voevodsky's Homotopy Type System). This formalization is conducted in Coq, taking advantage of type class inference to emulate fibrancy. We then propose a refinement of the notion of fibrancy—justified in the cubical model—by distinguishing between degenerate and regular fibrant families. In this system, a fibrant replacement is admissible (which is an open issue in the community) and gives rise to a model structure on the universe of all types.

1998 ACM Subject Classification F.4.1 Mathematical logic

Keywords and phrases HoTT; Homotopy Type System; model category; simplicial set; Coq

## 1 Introduction

There is an on-going connection between type theory and homotopy theory, based on the similarity between types and the notion of homotopy types for topological spaces. This connection has been made precise by the advent of a univalent Homotopy Type Theory (HoTT) whose theory is justified by a model in the presheaf category `sSet` of simplicial sets [15], which has later been rephrased more computationally in the presheaf category of cubical sets `cSet` [7, 9]. Conversely, one of the goals of HoTT is synthetic homotopy theory, which consists in formalizing internally proofs of homotopy theory, and ideally to compute complex objects such as homotopy groups of spheres. It is thus natural to wonder to what extend the simplicial or cubical model can be reflected in HoTT or any extension thereof. Indeed, HoTT is already an extension of Martin-Löf type theory to account for the existence of very powerful homotopical principles: the fact that equivalences of types can be reflected as equalities in the theory. To go beyond and account for the fact that there also exists a notion of strict equality in the model, Voevodsky has proposed an extension of HoTT called Homotopy Type System (HTS) [19]. In HTS, there are two notions of equality, a strict one and a univalent one. To avoid a direct collapse between the two equalities, a new class of types, called *fibrant types* has been introduced to reflect the fact that the homotopical equality in homotopical models can only be eliminated over fibrations. Thus, HTS makes more explicit the connection between HoTT and the homotopy structure of `cSet` (or in the same way, of `sSet`). This homotopy structure is given by a model structure: a definition of

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

© Simon Boulier and Nicolas Tabareau;
licensed under Creative Commons License CC-BY

Leibniz International Proceedings in Informatics

LIPICS Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
three classes of maps—fibrations, cofibrations and weak equivalences—satisfying various
properties. The goal of this article is to study the following question:

> "To what extend the model structure of cubical sets can be reflected in HoTT, HTS or another extension of Martin-Löf type theory?"

To answer this question, we first formalize in Section 2 the notion of model structure in a Martin-Löf type theory with a strict equality.

Gambino and Garner [10] and Lumsdaine [16], have shown that the category of contexts of a dependent type theory with identity types and Higher Inductive Types (HIT), enjoys two weak factorization systems. In Section 3, we synthesize their work internally in a two-level type theory, which is a variation of HTS as proposed by Altenkirch et al. [4, 8]. We show that they give rise to a model structure, but only on the category of fibrant types, not on bare types. In this model structure, weak equivalences are given by type equivalences as defined in the HoTT book [18], fibrations are captured by fibrant predicates, and cofibrations are captured by a specific HIT called a (mapping) *cylinder*. We formalize our result in Coq by using type class inference to encode fibrancy (Section 3.2). To understand the interplay between the model structure of fibrant types and the one of *cSet*, we then give an interpretation of HTS in the Bezem-Coquand-Huber model [7] (Section 3.3).

In Section 4, we turn to the problem of defining a model structure on the category of all types. This requires to consider the fibrant replacement type former, which is known to be inconsistent in HTS (see [1] and [8, Thm. 4.3.1.] for two independent explanations). In this paper, we solve this issue by distinguishing between degenerate and regular fibrant families, both having a clear interpretation in the cubical model. This refinement allows us to consider a fibrant replacement operator with enough properties to lift the model structure on the category of all types, which is known to be a difficult issue in traditional homotopical models and was open in the context of HoTT. The definition of a model structure on all types opens a way to study formally the definition of homotopy limits and colimits in HoTT, justifying the current proposition on graphs (without composition) and extending it to more complex limits and colimits on Reedy categories.

Both model structures have been formalized in the Coq proof assistant and are available online at https://github.com/CoqHott/model-structures-Coq.

## 2 Model Structures in MLTT

### 2.1 MLTT with a Strict Equality

The first system we consider is Martin-Löf type theory with a strict equality $\equiv$ (i.e., satisfying functional extensionality and Uniqueness of Identity Proofs (UIP), as in [12] and [4]). We present it with a syntax à la Calculus of Constructions (terms and types belong to the same syntactic class) and with a cumulative hierarchy of universes indexed by natural numbers. As this type theory is now well-known, we don't detail it and only give the typing rules to fix the notations (Fig. 1). We write $\simeq_{\beta\eta}$ for the conversion, which encompasses: $\alpha$-equivalence, $\beta$- and $\eta$-equivalences for $\Pi$ types and $\Sigma$ types, $\beta$-equivalence for equality types ($J\equiv(A, \text{y.e.P}, t, t, \mathbf{1}_t, u) \simeq_{\beta\eta} u$).

Throughout this paper, we write MLTT for "Martin-Löf type theory with a strict equality".

### 2.2 Categories

Defining the right notion of category in HoTT with a relevant equality is quite intricate as several choices can be made to tame higher coherences [2]. There is no such shilly-shallying
<figure><img src="image_4.png" /><figcaption>**Figure 1** Typing rules for Martin-Löf type theory with a strict equality</figcaption></figure>

in a type theory where the equality is irrelevant, as already noticed in [3, 4]:

► Definition 1. A category consists of:

- a type $A$ of objects,

- for all $a, b : A$, a type $\operatorname{Hom}(a, b)$ of arrows

- for all $a : A$, an identity arrow $\mathrm{id}_a : \operatorname{Hom}(a, a)$

- for all $a, b, c : A$, a composition function $\circ : \operatorname{Hom}(b, c) \to \operatorname{Hom}(a, b) \to \operatorname{Hom}(a, c)$

- for all $f : \operatorname{Hom}(a, b)$, a proof of $f \circ \mathrm{id}_a \equiv f$ and $\mathrm{id}_b \circ f \equiv f$

- for all $f : \operatorname{Hom}(a, b)$, $g : \operatorname{Hom}(b, c)$, $h : \operatorname{Hom}(c, d)$, a proof of $h \circ (g \circ f) \equiv (h \circ g) \circ f$.

The definition of a category is universe-polymorphic: it depends on a universe $\mathcal{U}_j$ in which all types involved live. In the rest of the paper, all definitions are implicitly universe-polymorphic.

The main interest of defining categories with a strict equality is that each universe $\mathcal{U}_i$ is a category, where the $\operatorname{Hom}(A, B)$ is given by $A \to B$, identity and composition are those of functions, and the laws are given by $\beta\eta$-conversion.

## 2.3 Model Structures

Model categories are used in mathematics to describe higher homotopies on a category (standard references are [11, 13]). A model category is a particular case of category with weak equivalences. Those categories are models of homotopy theory in the following sense: each category with weak equivalences presents an $(\infty, 1)$-category by localization. Compared to
4 Model structure on the universe in a two level type theory

simple weak equivalence categories, model categories are easier to work with (for instance
to compute the localization). Besides, model categories play a great role in comparing
the models of homotopy theory as they permit to compare different definitions of higher
categories via Quillen equivalences. The prototypical examples of model categories are
**Top** (the category of topological spaces), **sSet** and **cSet**. Here, we present directly the type
theoretic version of model categories.

Let $\mathcal{C}$ be a category (in the sense of definition 1).

► **Definition 2.** Let $f : \operatorname{Hom}(X, Y)$ and $g : \operatorname{Hom}(X', Y')$ be arrows of $\mathcal{C}$. We say that $f$ is a *retract* of $g$ if there exist $1$ arrows $s, r, s'$ and $r'$ such that the following diagram commutes:

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

By a class of arrows of $\mathcal{C}$, we simply mean a predicate $P : \Pi X, Y : A$. $\operatorname{Hom}(X, Y) \to \mathcal{U}_i$ (for an arbitrarily high universe $\mathcal{U}_i$). We write $f \in P$ for all function such that $P f$ is inhabited. If $Q$ is another class, we write $P \simeq Q$ if we have $\Pi X, Y$. $\Pi f : \operatorname{Hom}(X, Y) \to P f \Leftrightarrow Q f$; and $P \cap Q$ for the conjunction of the two classes.

► **Definition 3.** A class $P$ of arrows of $\mathcal{C}$ satisfies the 2-out-of-3 property if, for all arrows $X \xrightarrow{f} Y \xrightarrow{g} Z$ such that two of $f$, $g$ and $g \circ f$ belong to $P$, so does the third. More precisely, it means that we have three functions:

■ $\Pi f, g. P f \to P g \to P (g \circ f)$

■ $\Pi f, g. P (g \circ f) \to P f \to P g$

■ $\Pi f, g. P g \to P (g \circ f) \to P f$

► **Definition 4.** Let $f : \operatorname{Hom}(X, Y)$ and $g : \operatorname{Hom}(X', Y')$ be arrows of $\mathcal{C}$. It is said that $f$ has the *left lifting property* (LLP) with respect to $g$ (and that $g$ has the *right lifting property* (RLP) with respect to $f$) if, for all arrows $F : \operatorname{Hom}(X, X')$ and $G : \operatorname{Hom}(Y, Y')$ such that the square below commutes, there exists an arrow $\gamma : \operatorname{Hom}(Y, X')$ filling the diagonal:

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

We then say that an arrow $f$ has the LLP (resp. the RLP) with respect to a class of arrows $P$ if it has it with respect to all arrows of $P$. We write $\mathbf{LLP}(P)$ (resp. $\mathbf{RLP}(P)$) the class of such arrows.

► **Definition 5.** A weak factorization system (wfs) on $\mathcal{C}$ consists of two classes of arrows $L$ and $R$ such that:

1. every arrow $f$ of $\mathcal{C}$ can be factorized as $f \equiv r \circ l$ with $l \in L$ and $r \in R$

2. $L$ is exactly the class of arrows of $\mathcal{C}$ which have the LLP with respect to $R : L \simeq \mathbf{LLP}(R)$

3. $R$ is exactly the class of arrows of $\mathcal{C}$ which have the RLP with respect to $L : R \simeq \mathbf{RLP}(L)$

<footnote n="1">¹ In this paper “exists” is always understood in the constructive sense, i.e. as a sigma type and not as the squashed sigma type.</footnote>
The classes L and R of a weak factorization system enjoy several good properties: they contain all isomorphisms, they are closed under retract, L is closed under pushouts, R is closed under pullbacks, ... We can now state what a model structure is:

► **Definition 6.** A *model structure on C* consists of three classes of arrows *F*, *C* and *W* (the *fibrations*, the *cofibrations* and the *weak equivalences*) such that:

1. *W* satisfies the 2-out-of-3 property

2. (AC, F) and (C, AF) are two weak factorization systems,
where AC := C ∩ W and AF := F ∩ W.

The arrows of *AC* (resp. *AF*) are called the *acyclic cofibrations* (resp. *acyclic fibrations*).

If $\mathcal{C}$ has a terminal object $1$, we say that an object $X$ is *fibrant* if the map $X \to 1$ is a fibration.

► **Definition 7.** A *model category* is a category equipped with a model structure which is complete (it has all small limits) and cocomplete (it has all small colimits).

3 Model Structure on Fibrant Types

In the cubical model, the universe $\mathcal{U}$ is roughly interpreted by **cSet**, the category of cubical sets. We look for an extension of MLTT reflecting enough homotopy structure of the model so that we can equip $\mathcal{U}$ with a model structure mimicking the model structure of **cSet**. We start our investigations with a variant of Voevodsky's Homotopy Type System (HTS) [19] which allows us to define a model structure on the category of fibrant types. We call this variant MLTT$_2$ as it constitutes a 2-level type theory in the sense of [4].

**3.1 MLTT<sub>2</sub>**

Homotopy Type System consists in MLTT enriched with a univalent equality (written =). As univalence and UIP are contradictory [18, ex 3.1.19], HTS requires a mechanism to prevent the strict equality and the univalent equality from collapsing. This is achieved by introducing the notion of *fibrant types* (the terminology comes from their interpretations in homotopical models, see Section 3.3). In this paper, we call *identity types* the types $t = t'$, in opposition to strict equality types $t \equiv t'$.

In the end, there is a new judgment $\Gamma \vdash A \textbf{Fib}$ which expresses that a type is *fibrant*. All usual types are fibrant, except strict equality types. The rules to derive fibrancy are given in Figure 3. Then, the elimination of univalent equality is restricted to fibrant types (Fig. 2). As a result we have $t \equiv t' \to t = t'$ but $t = t' \nvdash t \equiv t'$. A new hierarchy $\mathcal{U}\mathcal{F}_i$ of universes of fibrant types is also introduced.

$$
\frac{\Gamma \vdash A : \mathcal{U}_i \qquad \Gamma \vdash t, t' : A}{\Gamma \vdash t =_A t' : \mathcal{U}_i}
\qquad
\frac{\Gamma \vdash t : A}{\Gamma \vdash \mathbf{refl}_t : t =_A t}
\qquad
\frac{\Gamma \vdash A : \mathcal{U}_i \qquad \Gamma \vdash A \textbf{Fib}}{\Gamma \vdash A : \mathcal{U}\mathcal{F}_i}
\\[2ex]
\frac{\Gamma \vdash A \textbf{Fib} \qquad \Gamma \vdash t, t' : A \qquad \Gamma \vdash p : t =_A t'}{\Gamma, y : A, q : t =_A y \vdash P \textbf{Fib} \qquad \Gamma \vdash u : P \{y := t, q := \mathbf{refl}_t\}}
\qquad
\frac{\Gamma \vdash A : \mathcal{U}\mathcal{F}_i}{\Gamma \vdash J_=(A, y.q.P, t, t', p, u) : P \{y := t', q := p\}}
$$

<caption>■ **Figure 2** Typing rules of the fibrant equality and the fibrant universes</caption>
<figure><img src="image_7.png" /><figcaption>Figure 3 Rules for fibrancy</figcaption></figure>

The main variation in our presentation of MLTT₂ with respect to HTS is that, exactly as in [4], we don't consider the reflection rule which says that x ≡ y implies x ≁ₐ y. This allows to retain a decidable type checking and to implement MLTT₂ in Coq (Section 3.2). We also allow forming identity types and reflexivity on non necessarily fibrant types. This is justified by the cubical sets model in Section 3.3.

► Remark. We don't add the univalence axiom (for the univalent equality) because we don't need it in our formalization. To get univalence in the model, we would instead have to consider cubical sets with connections, which would unnecessarily complicate our presentation.

## 3.2 Implementation in Coq

We found a way to emulate MLTT₂ in the Coq proof assistant using type class inference. First we define a type class *Fibrant* to keep track of fibrant types. The same technique has already been used in the HoTT library [6] to keep track of the use of functional extensionality and univalence axioms.

Axiom *Fibrant*: Type → Type.

Existing Class *Fibrant*.

As *Fibrant* is declared as an axiom, the only way to inhabit this class is to use postulated fibrancy rules. For instance, the rule for the dependent product is:

Axiom *fibrant_forall*: ∀ (A:Type) (B: A → Type),
Fibrant A → (∀ x, Fibrant (B x)) → Fibrant (∀ x, B x).

Note that each time we declare a new inductive type, we need to add an axiom corresponding to its fibrancy rule. Then we define the identity types as a private inductive type<fnref n="2" /> to forbid the use of its elimination principle when the predicate and the type are not fibrant:

Private Inductive paths {A : Type} (x : A) : A → Type := idpath : paths x x.

Definition paths_ind (A : Type) (FibA: Fibrant A) (x : A) (P : ∀ y : A, paths x y → Type)
(FibP : ∀ y p, Fibrant (P y p)) (u : P x idpath) (y : A) (p : paths x y) : P y p
:= match p with idpath ⇒ u end.

The fibrancy conditions are checked automatically by type class inference. The universe of fibrant types is defined using a coercion:

<footnote n="2">² Private inductive types have been introduced in Coq to allow a similar trick for higher inductive types.</footnote>
Record TypeF := { TypeF_T : Type ; TypeF_F : Fibrant TypeF_T } .

Coercion TypeF_T : TypeF ↦→ Sortclass.

The only drawback with this presentation is that the use of a private inductive type breaks some Coq tactics to reason on equality (especially `destruct` and `rewrite`). We circumvented this by defining a tactic `destruct_path` and a Coq plugin to fix `rewrite` (c.f. the documentation of the formalization).

## 3.3 Model in cubical sets

Models of HTS are usually given as refinements of the simplicial or cubical models. For simplicity, we choose to give a model of MLTT₂ in the Bezem-Coquand-Huber category of cubical sets without connections [7]. We mainly follow Huber’s thesis [14], which provides a clear exposition of this model. In [4], Altenkirch et al. have defined a model for a 2-level type theory to be a pair of categories with families (CwF) with a structure-preserving morphism between them. Here the CwF for strict equality is given by cubical sets (it is a CwF as a presheaf model), and the CwF for univalent equality is given by the subcategory of uniform Kan cubical sets (shown to be a CwF in [14]).

We only recall the definitions of the cubical sets model needed to understand the difference between MLTT₂ and the refined system of Section 4; we refer the reader to Huber’s thesis for a comprehensive presentation.

### Cubical sets

We suppose given an infinite set of names or dimensions x, y, z... For each finite set *I* of names, we suppose given a chosen fresh name $x_I \notin I$. We write $I, x$ and $I \setminus x$ for the union and the difference with the singleton $\{x\}$. **2** is the set $\{0, 1\}$.

* Definition 8. The cube category $\Box$ has for objects $I, J, \dots$ the finite sets of names. The morphisms $f : I \to J$ are set theoretic function $f : I \to J \sqcup 2$ which are injective on the set of their defined elements: $\text{def}(f) = f^{-1}(J) = \{x \in I | f(x) \notin 2\}$. Composition is defined as in a monad. For $f : I \to J$ and $g : J \to K$, we write $fg = g \circ f$ the composition in reverse order. For $f : I \to J, x \notin I$ and $c \in J \sqcup 2$, we write $(f, x = c) : I, x \to J$ for $f$ extended with $x \mapsto c$.

* Definition 9. The face maps are the morphisms $(x = 0), (x = 1) : I \to I \setminus x$ for $x \in I$. A degeneracy map is an inclusion $J \to I$ for $J \subseteq I$. For $x \notin I$ the degeneracy associated to $I \subseteq I, x$ is written $s_x : I \to I, x$.

* Definition 10. A cubical set $\Gamma$ is functor $\Gamma : \Box \to \text{Set}$. In other words, a cubical set is a presheaf over $\Box^{\text{op}}$. We write $\text{cSet}$ the category of cubical sets.

Given a cubical set $\Gamma$, an element $\rho \in \Gamma(I)$ is called an *I-cube*. For $x \in I$, $\rho$ is said to be *degenerate* along $x$ if it can be written $\rho = \rho's_x$, in such a case $\rho' = \rho(x=0) = \rho(x=1)$.
As a presheaf category, $\text{cSet}$ constitutes a category with families (and hence a model of type theory) which supports $\Pi$ types, $\Sigma$ types, strict equality, ... Let's recall how types and terms are interpreted in such a model:

* Definition 11. Given a cubical set $\Gamma$, a cubical family $\Gamma \vdash A$, is given by:

- a set $A(I, \rho)$ for each $I \in \Box$ and $\rho \in \Gamma(I)$

- a restriction $A(I, \rho) \to A(J, \rho f)$, $a \mapsto af$ for each $f : I \to J$ and $\rho \in \Gamma(I)$

- such that for all $a \in A(I, \rho)$, $a \text{id}_I = a$ and $(af)g = a(fg)$
We freely use $A\rho$, $A(\rho)$ or $A(I, \rho)$ to denote the same set. The same goes for terms.

► Definition 12. A term $\Gamma \vdash t : A$ inhabiting a family $\Gamma \vdash A$ is given by:

- for each $I \in \square$ and $\rho \in \Gamma(I)$, an $I$-cube $t\rho \in A\rho$

- such that for all $f : I \to I'$, $(t\rho)f = t(\rho f)$

## Kan cubical families

Bare types are interpreted as cubical families. Concerning fibrant types, they are interpreted by uniform Kan families. To define them we need the notions of shape and open-box.

► Definition 13. Let $I \in \square$ and $x \in I$. A shape $S$ on $I$ of direction $x$ is a tuple $(I; (x, a); J)$ with $x \in I$, $a \in \mathbf{2}$ and $J \subseteq I \setminus x$.

The indices of $S$ are defined by $\langle S \rangle = \{(x, \bar{a})\} \sqcup J \times \mathbf{2}$ (with $\bar{a}$ the negation of $a$). And the principal face of $S$ is $(x, a)$. Given a morphism $f : I \to I'$ with $J, x \subseteq \text{def}(f)$, we define $Sf = (I'; (f(x), a); f(J))$ which is a shape on $I'$ of direction $f(x)$.

► Definition 14. Given a family $\Gamma \vdash A$. Given $I \in \square$, $S$ a shape on $I$ of direction $x$ and $\rho \in \Gamma(I)$, an open-box $\bar{u}$ of shape $S$ in $A\rho$ is given by:

- for all $(y, b) \in \langle S \rangle$, an $I \times y$-cube $u_{yb} \in A(\rho(y = b))$

- such that for all $(y, b), (z, c) \in \langle S \rangle$ with $y \neq z$, $u_{yb}(z = c) = u_{zc}(y = b)$

Given $f : I \to I'$ with $J, x \subseteq \text{def}(f)$, $\bar{u}f$ is an open-box of shape $Sf$ in $A(\rho f)$.

► Definition 15. Given a family $\Gamma \vdash A$, a uniform Kan structure over $A$ is given by:

- for all $I \in \square$, $\rho \in \Gamma(I)$, $S$ shape on $I$ of direction $x$ and $\bar{u}$ open-box of shape $S$ in $A\rho$, an $I$-cube $[A\rho]_S\bar{u} \in A\rho$ called the filler of $\bar{u}$

- such that for all $(y, b) \in \langle S \rangle$, $([A\rho]_S\bar{u})(y = b) = u_{yb}$

- and such that for each $f : I \to I'$ with $J, x \subseteq \text{def}(f)$, $([A\rho]_S\bar{u})f = [A(\rho f)]_{Sf}(\bar{u}f)$

The last condition is the uniformity condition. And the $I \times x$-cube $([A\rho]_S\bar{u})(x = a)$ is called the composition of $\bar{u}$.

We write $\Gamma \vdash A$ **Kan** when $A$ is equipped with such a structure.

A fibrant type of MLTT₂ is interpreted by a cubical family equipped with a uniform Kan structure.

## Identity types and universes

We recall here how identity types are interpreted using $I$-cubes of higher dimension.

► Definition 16. Let $\Gamma \vdash A$ be a family, and $\Gamma \vdash t, t' : A$ two terms inhabiting $A$. The identity type between $t$ and $t'$ is the family $\Gamma \vdash \mathbf{Id}_A(t, t')$ given by

$$ \mathbf{Id}_A(t, t')\rho = \{ \omega \in A(I, x_I, \rho_{s_{x_I}}) \mid \omega(x_I = 0) = t\rho \text{ and } \omega(x_I = 1) = t'\rho \} $$

The restriction induced by $f : I \to I'$ is given by $\omega f = \omega(f, x_I = x_{I'})$ (restriction in $\mathbf{Id}_A$ on the left and in $A$ on the right).

In [14], this cubical family is shown to model properly the identity types in MLTT₂. That is: $\mathbf{Id}_A$ commutes with substitutions and hence is a type former; there is always a term inhabiting $\mathbf{Id}_A(t, t)$; if $A$ is a Kan family so is $\mathbf{Id}_A(t, t')$; and the identity types support an eliminator $J$. To define $J$, Huber starts by defining a (non dependent) transport which requires only $P$ to be Kan (but not $A$). Then, using that singletons of $A$ are contractible when $A$ is Kan, it is shown that the full eliminator can be derived.
A cumulative hierarchy of universes of cubical sets ($\mathcal{U}_i$) and another of Kan cubical sets ($\mathcal{UF}_i$) can be defined (see Appendix C). As remarked in [14], the category of cubical sets enjoy a fibrant replacement, however, it does not lift to a type theoretic operator as it does not commute with substitutions (see Appendix E and Section 4.3).

## 3.4 Homotopy Fibers and Cylinders

The model structure on $\mathcal{UF}_i$ requires the two dual notions of homotopy fibers and mapping cylinders. Homotopy fibers are definable using $\Sigma$-types and identity types [18]. Let $f: A \to B$ be a function. The *homotopy fibers* of $f$ are defined by the type family $\mathbf{fib}_f: B \to \mathcal{U}_i$ with

$$ \mathbf{fib}_f := \lambda y. \Sigma x : A. f x = y $$

Cylinders are defined as an Higher Inductive Type (HIT, see [18] for an introduction). They were introduced in [17] and [16]. The formation and introduction rules for cylinders are given as follows (all the rules have $\Gamma \vdash A, B : \mathcal{U}_i$ and $\Gamma \vdash f : A \to B$ as additional premises).

$$ \Gamma \vdash \mathbf{Cyl}_f : B \to \mathcal{U}_i \qquad \frac{\Gamma \vdash A, B \ \mathbf{Fib} \qquad \Gamma \vdash t : B}{\Gamma \vdash \mathbf{Cyl}_f t \ \mathbf{Fib}} \qquad \Gamma \vdash \mathbf{top}_f : \Pi x : A. \mathbf{Cyl}_f(f x) $$

$$ \Gamma \vdash \mathbf{base}_f : \Pi y : B. \mathbf{Cyl}_f y \qquad \Gamma \vdash \mathbf{cyl\_eq}_f : \Pi x : A. \mathbf{top}_f x = \mathbf{base}_f(f x) $$

This expresses that there are two ways to inhabit a cylinder, with **top** and **base**, and that those two ways coincide on $f x$. The elimination rule is given by:

$$ \begin{gathered} \Gamma \vdash A, B \ \mathbf{Fib} \qquad \Gamma, y : B, w : \mathbf{Cyl}_f y \vdash P \ \mathbf{Fib} \\ \Gamma \vdash \mathbf{top}' : \Pi x : A. P(fx) \ (\mathbf{top} x) \qquad \Gamma \vdash \mathbf{base}' : \Pi y : B. P y \ (\mathbf{base} y) \\ \Gamma \vdash \mathbf{cyl\_eq}' : \Pi x : A. (\mathbf{cyl\_eq} x) \# (\mathbf{base}'(fx)) = \mathbf{top}' x \\ \frac{\Gamma \vdash \mathbf{cyl\_ind}(P, \mathbf{top}', \mathbf{base}', \mathbf{cyl\_eq}') : \Pi y : B. \Pi w : \mathbf{Cyl}_f y. P y w}{\Gamma \vdash \mathbf{cyl\_ind}(P, \mathbf{top}', \mathbf{base}', \mathbf{cyl\_eq}') : \Pi y : B. \Pi w : \mathbf{Cyl}_f y. P y w} \end{gathered} $$

where # denotes transport along identity types and **ap** is the action of a function on identity types (as in [18]). The computation rules are given in Appendix A.

As for the identity type, cylinders are fibrant when the underlying types are and we restrict the elimination of cylinders to fibrant predicates and fibrant underlying types. We left for future work the constructions of cylinders in the cubical model.

## 3.5 Model Structure on $\mathcal{UF}_i$

We now describe a model structure on the universe of fibrant types $\mathcal{UF}_i$. In [10], Gambino and Garner define the (AC,F)-wfs, and in [16] (and also in [5, Section 3.2]), Lumsdaine define the (C,AF)-wfs. One can see this section as a synthesis and formalization of those works in MLTT₂. Our work emphasizes the fact that those factorization systems are only defined for *fibrant types*. Throughout this section, A and B denote fibrant types.

### Weak Equivalences.

Weak equivalences are defined as type equivalences in the sense of [18, Chapter 4]:

* Definition 17. A function $f: A \to B$ is a *type equivalence* if there exists $g: B \to A$ and

* $\theta: \Pi x : A. g (fx) = x$

* $\epsilon: \Pi y : B. f (gy) = y$

* $\alpha: \Pi x : A. \mathbf{ap} f (\theta x) = \epsilon (fx)$.
(AC, F)-WFS.

The (AC, F)-wfs system is given by homotopy fibers. Every function $f$ factorizes as:

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

► Remark. As we now have two equalities, we have to be careful about what we mean by "being equal" or "commuting". In the following, all commutations of diagrams are required to be with respect to strict equality.

► Definition 18. A function $f : A \to B$ is said to be a *fibration* if there exists a fibrant type family $P : A' \to \mathcal{U}F_i$ such that $f$ is a retract of $\pi_1 : \Sigma_x P x \to A'$.
We write $F$ the class of fibrations. The class of acyclic cofibrations is defined as **LLP**(*F*).

► Proposition 1. (LLP(*F*), *F*) is a weak factorization system on *U*F<sub>*i*</sub>.

**Proof.** We have to check that:

$$
\text{ for all } f, f' := \lambda x. (f x, x, \textbf{refl}_{f x}) \in \mathbf{LLP}(F)
$$

$$
\text{ RLP}(\text{LLP}(F)) \subseteq F
$$

We only sketch the proof of the first point. All other proofs of this section are similar and
can be found in the formalization.

As the lifting property is stable under retracts, to show that $f' \in \text{LLP}(F)$ we only have to
solve the following lifting problem:

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

We define $\gamma$ as the composition $\Sigma_{y:B} \mathbf{fib}_f y \xrightarrow{\alpha} \Sigma_{y:B} P(Gy) \xrightarrow{\beta} \Sigma_{x:A'} P x$ where
$\alpha := \lambda (y, x, p). ((y, x, p), \pi_2(Fx))$ and $\beta := \lambda (w, z). (Gw, z)$ (modulo the transports
along strict equalities). We can check that both triangles commute.
$\quad$

(C, AF)-WFS

The (C, AF)-wfs is given by cylinders. Every function $f$ factorizes as:

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

To define cofibrations, we first characterize acyclic fibrations:

► Proposition 2. A function $f : A \to B$ is an acyclic fibration (i.e. both a fibration and a weak equivalence) iff there exists a fibrant type family $P : A' \to \mathcal{U}F_i$ such that for all $x$, $P x$ is *contractible* (i.e. weakly equivalent to unit 1) and $f$ is a retract of $\pi_1 : \Sigma_x P x \to A'$.
We write $AF$ the class of acyclic fibrations. The class of cofibrations is defined as $\mathbf{LLP}(AF)$.

► Proposition 3. (*AF*, **LLP**(*AF*)) is a weak factorization system on *U*F<sub>*i*</sub>.
► Theorem 4. There is a model structure on $\mathcal{U}F_i$ with the weak equivalences, fibrations and cofibrations as previously defined. Remark that $\mathcal{U}F_i$ is not a model categories as MLTT$_2$ as not all small colimits (it would need some quotient types).

Note that it is possible to state a simpler characterizations of the classes of maps. The two factorization systems give prototypical examples of maps which are (acyclic) fibration and (acyclic) cofibrations. We proved that, in fact, all (acyclic) fibrations and (acyclic) cofibrations arise as retracts (in a canonical sense) of such maps. Diagrammatically, we have (see also Appendix B for a type theoretic statement):

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

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

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

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

where $f'$ is $\lambda x$. ($f x, x, \text{refl}_{f x}$) and $\text{top}'$ is $\lambda x$. ($x, \text{top}_{f} x$).

# 4 Model Structure on Types

In Section 3, we have given a model structure on $\mathcal{U}F_i$ in MLTT$_2$. Unfortunately, this does not extend to the whole universe $U_i$ because there is no fibrant replacement in MLTT$_2$. To circumvent this issue, we propose MLTT$_2^F$: a refinement of MLTT$_2$ where the notion of fibrancy is finer; a type family can be either *degenerately fibrant* or *regularly fibrant*. This distinction allows us to define a fibrant replacement in MLTT$_2^F$, and then to extend the model structure on $U_i$.

## 4.1 A Context-Dependent Notion of Fibrancy

MLTT$_2^F$ is equipped with a new typing judgment $\Gamma; \Delta \vdash A \textbf{Fib}$ ($\Delta$ is another context), replacing the fibrancy judgment of MLTT$_2$. We thus distinguish two levels of context. When this judgment is derivable, we say that, in the context $\Gamma$, the type family $\Delta \vdash A$ is *regularly fibrant*. In the case where only $\Gamma, \Delta; . \vdash A \textbf{Fib}$ is derivable, we say that $\Delta \vdash A$ is *degenerately fibrant*—which is a weaker condition. Indeed, regular fibrancy implies degenerate fibrancy but the converse does not hold.

All typing rules of MLTT$_2$ are still valid, except when they mention the fibrancy judgment, in which case they must be modified to take the new notion of fibrancy into account. The rules for fibrancy are given in Figure 4, with the notation $\Gamma \vdash A \textbf{Fib}$ for $\Gamma; . \vdash A \textbf{Fib}$. As in MLTT$_2$, the only non fibrant types are strict equality types, and the fibrancy commutes with all other type constructors. The universes of types and fibrant types remain fibrant. Note the additional presence of a rule for substitutions (bottom right corner) where $\sigma : \Delta' \rightarrow \Delta$ is a context morphism and $A\sigma$ the substituted type. This is because this rule is not admissible anymore in the presence of a fibrant replacement.
$$ (\text{rules for } \mathcal{U}_i \text{ and } \mathcal{U}\mathcal{F}_i \text{ are unchanged}) \qquad \frac{\Gamma; \Delta \vdash A \ \mathbf{Fib} \qquad \Gamma; \Delta, x : A \vdash B \ \mathbf{Fib}}{\Gamma; \Delta \vdash \Pi x : A. B \ \mathbf{Fib}} $$

$$ \frac{\Gamma; \Delta \vdash A \ \mathbf{Fib} \qquad \Gamma; \Delta, x : A \vdash B \ \mathbf{Fib}}{\Gamma; \Delta \vdash \Sigma x : A. B \ \mathbf{Fib}} $$

$$ \frac{\Gamma; \Delta \vdash A \ \mathbf{Fib} \qquad \Gamma, \Delta \vdash t, t' : A}{\Gamma; \Delta \vdash t =_A t' \ \mathbf{Fib}} $$

$$ \frac{\Gamma; \Delta \vdash A \ \mathbf{Fib} \qquad \Gamma; \Delta \vdash B \ \mathbf{Fib}}{\Gamma, \Delta \vdash f : A \to B} $$

$$ \frac{\Gamma, \Delta \vdash t : A \to B \qquad \Gamma, \Delta \vdash t : A}{\Gamma; \Delta \vdash \text{Cyl}_f t \ \mathbf{Fib}} $$

$$ \frac{\Gamma; \Delta \vdash A \ \mathbf{Fib} \qquad \Gamma \vdash \sigma : \Delta' \to \Delta}{\Gamma; \Delta' \vdash A \sigma \ \mathbf{Fib}} $$

■ **Figure 4** Rules for fibrancy in MLTT<sub>2</sub><sup>F</sup>

We now refine the elimination rule for identity types:

$$ \frac{\Gamma \vdash A \ \mathbf{Fib} \qquad \Gamma \vdash t, t' : A \qquad \Gamma \vdash p : t =_A t'}{\Gamma; y : A, q : t =_A y \vdash P \ \mathbf{Fib} \qquad \Gamma \vdash u : P \{y := t, q := \mathbf{refl}_t\}} \qquad \frac{\Gamma \vdash J = (A, y.q.P, t, t', p, u) : P \{y := t', q := p\}}{\Gamma \vdash J = (A, y.q.P, t, t', p, u) : P \{y := t', q := p\}} $$

The family $P$ along which we eliminate a path equality is required to be **regularly** fibrant with respect to $y$ and $p$.

The elimination rule for the cylinder have to be refined exactly in the same way: the family $P$ along which we eliminate is required to be regularly fibrant with respect to $y$ and $w$.

## Fibrant replacement

Last, we introduce a fibrant replacement in MLTT<sub>2</sub><sup>F</sup>. The fibrant replacement is an operator that turns any type $A$ into a **degenerately** fibrant type $\bar{A}$. Asking only for a degenerately fibrant replacement is the key to avoid inconsistency. There is a canonical way to embed an element of $A$ into $\bar{A}$ given by $\eta_A$, and there is an eliminator **repl_ind**.

$$ \frac{\Gamma \vdash A : \mathcal{U}_i}{\Gamma \vdash \bar{A} : \mathcal{U}_i} $$

$$ \frac{\Gamma \vdash A : \mathcal{U}_i}{\Gamma; . \vdash \bar{A} \ \mathbf{Fib}} $$

$$ \frac{\Gamma \vdash A : \mathcal{U}_i}{\Gamma \vdash \eta_A : A \to \bar{A}} $$

$$ \frac{\Gamma; z : \bar{A} \vdash P(z) \ \mathbf{Fib} \qquad \Gamma \vdash t : \Pi x : A. P(\eta_A x)}{\Gamma \vdash \text{repl\_ind}_p t : \Pi z : \bar{A}. P(z)} $$

$$ \text{repl\_ind}_p t (\eta_A x) \approx_{\beta\eta} t x $$

Such a fibrant replacement can be used as the base type in the elimination of the identity type but can not directly appear in the predicate of the elimination. This is why we can not replay the usual proofs of inconsistency [1, 8] (both rely on the existence of a map $t = t' \to t \equiv t'$); we can however use the elimination of the identity type to prove, for instance, the $w$-groupoid laws on $\bar{A}$.

Using **repl_ind**, it is possible to define a non dependent eliminator

$$ \text{repl\_rec}_{A,B} : (A \to B) \to (\bar{A} \to B) $$

for any fibrant type $B$ and a function $\bar{f} : \bar{A} \to \bar{B}$ for any function $f : A \to B$. Moreover, the construction $\bar{f}$ satisfies the following strict equalities:

$$ \overline{\text{id}}_A \equiv \overline{\text{id}}_{\bar{A}} $$

$$ \overline{g \circ f} \equiv \overline{g} \circ \overline{f} $$
Note that it has already be noticed in [7, Section 8.5] that the fibrant replacement is not universal (which means that there is no $\eta$-rule for **repl_ind**) but it is on functions preserving the Kan structure (hence the two strict equalities above). However, fibrant replacement is weakly universal, which turns it into a modality in the sense of [18, Section 7.7].

Last, **repl_rec** satisfies the following fibrancy rule which says that given a regularly fibrant family $P : A \to \mathcal{U}_i$, the induced family $\bar{A} \to \mathcal{U}_i$ is still regularly fibrant:

$$ \frac{\Gamma \vdash P : A \to \mathcal{U}_i \quad \Gamma; x : A \vdash P x \text{ Fib} \\ \Gamma; z : \bar{A} \vdash \text{repl\_rec}_{A, \mathcal{U}_i} P z \text{ Fib}} $$

This rule is quite strong as it allows to define the transport of a property $P(x)$ along a proof of $\eta t = \eta t'$ as long as $P$ is sufficiently fibrant. More precisely, if $\Gamma; x : A \vdash P(x) \text{ Fib}$, then from $\eta t = \eta t'$ you can get a term of type $P(t) \to P(t')$. However, this rule is justified in the cubical model of Section 4.3.

## 4.2 Implementation

The implementation of MLTT<sub>2</sub><sup>F</sup> is very similar to the one of MLTT<sub>2</sub>. The only difference is that we have to make explicit the second part of the context $(\Delta)$ in the type class FibrantF keeping track of fibrant families.

Axiom FibrantF : $\forall \{\Delta : \text{Type}\}, (\Delta \to \text{Type}) \to \text{Type}$.
Existing Class FibrantF.

## 4.3 Model of MLTT<sub>2</sub><sup>F</sup>

We now give a model of MLTT<sub>2</sub><sup>F</sup> in cubical sets by refining the notion of Kan structure. A fibrant type of MLTT<sub>2</sub><sup>F</sup> is interpreted by a cubical set family equipped with a uniform degenerate Kan structure:

► **Definition 19.** Given a family $\Gamma$, $\Delta \vdash A$, a uniform degenerate Kan structure over $A$ relative to $\Gamma$ is given by:

- for all $I \in \square$, $S$ shape on $I$ of direction $x, \rho \in \Gamma(I)$ **degenerate along** $x, \delta \in \Delta(\rho)$ and $\bar{u}$ open-box of shape $S$ in $A(\rho, \delta)$, a **filler** $[A(\rho, \delta)]_{S\bar{u}} \in A(\rho, \delta)$

- such that for all $(y, b) \in \langle S \rangle$, $([A\rho]_{S\bar{u}})(y = b) = u_{yb}$

- and such that for each $f : I \to I'$ with $J, x \subseteq \text{def}(f)$ ($\rho f$ is thus degenerate along $f(x)$), $([A(\rho, \delta)]_{S\bar{u}})f = [A(\rho f, \delta f)]_{Sf}(\bar{u}f)$

The only difference with a bare Kan structure (Definition 15) is that the quantification on the elements in the first part of the context is restricted to degenerate elements. We write $\Gamma; \Delta \vdash A$ **Kan** when the family $A$ is equipped with such a structure. Fibrancy rules of Figure 4 hold in the model (see Appendix D).

The structure $\Gamma; A \vdash P$ **Kan** is actually the maximal way of relaxing the notion of Kan structure and still get the transport of a path equality in $A$ along $P$. The transport generalizes to the $J$-rule using the same technique as in [14].

► **Proposition 5.** Let $\Gamma; A \vdash P$ **Kan** be a fibrant family. And let $\Gamma \vdash t, t' : A, \Gamma \vdash p : \text{Id}_A(t, t')$ and $\Gamma \vdash u : P[t]$ be terms. We can then define an element $\Gamma \vdash p^{\#P} u : P[t']$.

**Proof.** The proof is similar to the case of bare Kan structure [14]. The only point to remark is that fillers are only used on degenerate elements of $\Gamma$.
14 Model structure on the universe in a two level type theory

Let $I \in \square$ and $\rho \in \Gamma(I)$, we want to define $(p^{\#P} u)\rho \in P(\rho, t'\rho)$. We consider the fresh direction $x_I$ and the shape $S$ given by $(I, x_I; (x_I, 1); \emptyset)$. Then we have an open-box $\tilde{w}$ on $S$ in $P(\rho_{s_{x_I}}, p\rho)$ given by $w_{x_I 0} = u\rho$. As $\rho_{s_{x_I}}$ is degenerate along $x_I$, we can define $(p^{\#P} u)\rho$ as the composition operation:

$$ (p^{\#P} u)\rho := ([P(\rho_{s_{x_I}}, p\rho)]_S \tilde{w})(x_I = 1) $$

The naturality conditions for $p^{\#P} u$ follows from the uniformity of fillers.

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

Let's now move on to the definition of fibrant replacement. In his thesis, Huber defines the fibrant replacement of a cubical sets and remarks that the generalization to a cubical family does not commute with substitution. The problem comes from the fact that Huber defines a regular fibrant replacement whereas the only one that commutes with substitution is a degenerate fibrant replacement. Both fibrant replacements coincide on cubical sets, but they differ when contexts are taken into account.

The definition is based on an inductive-recursive set by freely adding filling and composition operations. The "recursive" part is used to define restrictions.

► Definition 20. Let $\Gamma \vdash A$ be a family. The family $\Gamma \vdash \bar{A}$, the degenerate fibrant replacement of $A$, is given by the sets and restrictions defined by induction-recursion as follow:

- for each $I \in \square$, $\rho \in \Gamma(I)$ and $u \in A\rho$, $\eta(u) \in \bar{A}\rho$

- for each $I \in \square$, $S = (I; (x, a); J)$, $\rho \in \Gamma(I)$ degenerate along $x, \tilde{u}$ in $\bar{A}\rho$, $\text{fill}_S(\tilde{u}) \in \bar{A}\rho$

- for each $I \in \square$, $S = (I; (x, a); J)$, $\rho \in \Gamma(I)$ deg. along $x, \tilde{u}$ in $\bar{A}\rho$, $\text{comp}_S(\tilde{u}) \in \bar{A}\rho(x = a)$ and:

- for $f : I \to I'$, $(\eta(u))f := \eta(uf)$

- for $f : I \to I'$,

$$ (\text{fill}_S(\tilde{u}))f := \begin{cases} u_{yb}f' & \text{if } f = (f', y = b) \text{ for some } (y, b) \in \langle S \rangle \\ (\text{comp}_S(\tilde{u}))f' & \text{if } f = (f', x = a) \text{ for } (x, a) \text{ the principal face} \\ \text{fill}_{Sf}(\tilde{u}f) & \text{otherwise} \end{cases} $$

- for $f : I \setminus x \to I'$,

$$ (\text{comp}_S(\tilde{u}))f := \begin{cases} u_{yb}(x = a)f' & \text{if } f = (f', y = b) \text{ for some } (y, b) \in \langle S \rangle \\ \text{comp}_{Sf'}(\tilde{u}f') & \text{otherwise, with } f' = (f, x = x_I) \end{cases} $$

► Proposition 6. The degenerate fibrant replacement lifts to a type operator: it commutes with substitutions. For all context morphism $\sigma : \Gamma' \to \Gamma$, $\bar{A}\sigma = \bar{A}\sigma$ as Kan families. (Proof in Appendix E).

## 4.4 Model Structure on $U_i$

We can now extend the definitions of fibrations, cofibrations and weak equivalences to encompass non fibrant types:

- a *fibration* (in a context $\Gamma$) is a retract of a map $\pi_1 : \Sigma_x P x \to A'$ where $P$ is **regularly** fibrant, that is when $\Gamma$; $x : A' \vdash P x$ **Fib** holds

- an *acyclic fibration* is a fibration such that for all $x : A'$, $P x$ is contractible

- a *weak equivalence* is a map $f : A \to B$ such that $\bar{f} : \bar{A} \to \bar{B}$ is a type equivalence (def. 17)

- cofibrations and acyclic cofibrations are still defined as **LLP(AF)** and **LLP(F)**
Fibrant replacement is used to lift the model structure from fibrant to bare types in the same way as geometric realization is used in the classical model structure on simplicial sets. Given a map $f : A \to B$, its homotopy fiber in $y : B$ is now $\mathbf{fib}_{\bar{f}}(\eta y)$. And the two wfs on $U_i$ are given by:

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

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

The development goes exactly the same way as for fibrant types and we get:

► Theorem 7. The two factorization systems given above form a model structure on $U_i$.

Again, characterizations of (acyclic) fibrations and cofibrations can be derived (Appendix B).

References

1. The nLab wiki. https://ncatlab.org/homotopytypetheory/show/Homotopy+Type+System, 2016.

2. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. *Mathematical Structures in Computer Science*, Volume 25, 2015.

3. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Infinite structures in type theory: Problems and approaches. *talk at TYPES*, 2015, Tallinn, Estonia.

4. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. *Computer Science Logic*, 2016, Marseille, France.

5. Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine. Homotopy limits in type theory. *Mathematical Structures in Computer Science*, Volume 25, 2015.

6. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT Library: A Formalization of Homotopy Type Theory in Coq. *Certified Programs and Proofs*, 2017, Paris, France.

7. Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. *Post-proceedings of TYPES 2013, LIPICs Volume 26*, 2014.

8. Paolo Capriotti. Models of type theory with strict equality. *PhD thesis*, 2017.

9. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. *To appear in Post-proceedings of TYPES 2015*, 2016.

10. Nicola Gambino and Richard Garner. The identity type weak factorisation system. *Theoretical Computer Science*, Volume 409, 2008.

11. Philip S Hirschhorn. *Model categories and their localizations*. AMS, 2003.

12. Martin Hofmann. *Extensional Constructs in Intensional Type Theory*. Springer, 1997.

13. Mark Hovey. *Model categories*. American Mathematical Society, 1999.

14. Simon Huber. Cubical interpretations of type theory. *PhD thesis*, 2016.

15. Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The simplicial model of univalent foundations. *arXiv preprint arXiv:1211.2851*, 2012.

16. Peter L.Lumsdaine. *Model Structures from Higher Inductive Types*. Unpublished notes, http://peterlefanulumsdaine.com/research/Lumsdaine-Model-strux-from-HITS.pdf, 2011.

17. Mike Shulman. *Inductive and higher inductive types*. Talk at University of Swansea, http://home.sandiego.edu/~shulman/hottminicourse2012/04induction.pdf, 2012.

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

19. Vladimir Voevodsky. *A simple type system with two identity types*. Unpublished notes, http://uf-ias-2012.wikispaces.com/file/view/HTS.pdf, 2013.
## A Mapping Cylinders

The computation rules of elimination of mapping cylinders are given by:

$$ \mathrm{cyl\_ind}(P, \mathrm{top}', \mathrm{base}', \mathrm{cyl\_eq}', f x, \mathbf{top} x) \cong_{\beta\eta} \mathrm{top}' x $$

$$ \mathrm{cyl\_ind}(P, \mathrm{top}', \mathrm{base}', \mathrm{cyl\_eq}', y, \mathbf{base} y) \cong_{\beta\eta} \mathrm{base}' y $$

$$ \mathbf{ap} \ \mathrm{cyl\_ind}(P, \mathrm{top}', \mathrm{base}', \mathrm{cyl\_eq}', f x) \ (\mathrm{cyl\_eq}_f x) \equiv \mathrm{cyl\_eq}' x $$

## B Characterizations of Fibrations and Cofibrations

### In MLTT₂

* **Proposition 8.** Let A and B be fibrant types.

- $f: A \to B$ is a fibration if and only if there exists $j: \Sigma y. \mathbf{fib}_f y \to A$ such that $f \circ j \equiv \pi_1$ and $j \circ (\lambda x. (fx, x, \mathbf{refl}_{fx})) \equiv \mathbf{id}_A$

- $f: A \to B$ is an acyclic fibration if and only if there exists $j: \Sigma y. \mathbf{Cyl}_f y \to A$ such that $f \circ j \equiv \pi_1$ and $j \circ (\lambda x. (x, \mathbf{top}_f x)) \equiv \mathbf{id}_A$

- $f: A \to B$ is a cofibration if and only if there exists $j: B \to \Sigma y. \mathbf{Cyl}_f y$ such that $j \circ f \equiv \lambda x. (x, \mathbf{top}_f x)$ and $\pi_1 \circ j \equiv \mathbf{id}_B$

- $f: A \to B$ is an acyclic cofibration if and only if there exists $j: B \to \Sigma y. \mathbf{fib}_f y$ such that $j \circ f \equiv \lambda x. (fx, x, \mathbf{refl}_{fx})$ and $\pi_1 \circ j \equiv \mathbf{id}_B$

* **Remark.** There is always a candidate for $j$. For instance, in the diagram of fibrations, $\pi_2$ is one. It makes the upper triangle strictly commute but not the one on the right. Hence, $j$ can be seen as a more constrained $\pi_2$.

Acyclic cofibrations have an even better description. As already noticed by Gambino and Garner [10], they are the injective equivalences:

* **Proposition 9.** Let A and B be fibrant types. A map $f: A \to B$ is an acyclic cofibration if and only if it is an *injective equivalence*, i.e. if an only if there exists $r: B \to A$ and

- $\theta: \Pi x : A. r (fx) \equiv x$

- $\epsilon: \Pi y : B. f (ry) = y$

- $\alpha: \Pi x : A. \mathbf{strict\_to\_path}(\mathbf{ap} \equiv f (\theta x)) = \epsilon (fx)$.

where $\mathbf{strict\_to\_path}$ is the map $t \equiv t' \to t = t'$.

### In MLTT₂<sup>F</sup>

* **Proposition 10.** Let A and B be any types.

- $f: A \to B$ is a fibration if and only if there exists $j: \Sigma y. \mathbf{fib}_f (\eta y) \to A$ such that $f \circ j \equiv \pi_1$ and $j \circ (\lambda x. (fx, \eta x, \mathbf{refl}_{\eta (fx)})) \equiv \mathbf{id}_A$

- $f: A \to B$ is an acyclic fibration if and only if there exists $j: \Sigma y. \mathbf{Cyl}_f (\eta y) \to A$ such that $f \circ j \equiv \pi_1$ and $j \circ (\lambda x. (\eta x, \mathbf{top}_f x)) \equiv \mathbf{id}_A$

- $f: A \to B$ is a cofibration if and only if there exists $j: B \to \Sigma y. \mathbf{Cyl}_f (\eta y)$ such that $j \circ f \equiv \lambda x. (\eta x, \mathbf{top}_f x)$ and $\pi_1 \circ j \equiv \mathbf{id}_B$

- $f: A \to B$ is an acyclic cofibration if and only if there exists $j: B \to \Sigma y. \mathbf{fib}_f (\eta y)$ such that $j \circ f \equiv \lambda x. (fx, \eta x, \mathbf{refl}_{\eta (fx)})$ and $\pi_1 \circ j \equiv \mathbf{id}_B$
And as previously, acyclic cofibrations are injective equivalences, whose definition generalizes as:

► **Definition 21.** Let $A$ and $B$ be any types. A map $f: A \to B$ is an *injective equivalence* if there exists $r: B \to \bar{A}$ and

■ $\theta: \Pi x : A. r (fx) \equiv \eta_A x$

■ $\epsilon: \Pi y : B. \bar{f}(ry) = \eta_B y$

■ $\alpha: \Pi x : A. \mathbf{strict\_to\_path}(\mathbf{ap} \equiv \bar{f}(\theta x)) = \epsilon(fx)$.

### C Universes

In presheaf models, universes are usually interpreted as Grothendieck universes thanks to the Yoneda lemma. We suppose given a hierarchy of Grothendieck universes $\mathbf{Set}_0, \mathbf{Set}_1, \dots$.

► **Definition 22.** For $I \in \square$, let $h^I = \operatorname{Hom}(I, \_)$ be the cubical set given by the Yoneda embedding. The cubical set $\mathcal{U}_I$ is defined by:

$$ \mathcal{U}_I(I) = \{ A \text{ cubical set family over } h^I \mid \forall f: I \to I', A_f \in \mathbf{Set}_I \} $$

And, similarly, Huber defines in [14] a universes $\mathcal{U}\mathcal{F}_I$ of Kan cubical sets.

► **Definition 23.** The cubical set $\mathcal{U}\mathcal{F}_I$ is defined by:

$$ \mathcal{U}\mathcal{F}_I(I) = \{ h^I \vdash A \mathbf{Kan} \mid \forall f: I \to I', A_f \in \mathbf{Set}_I \} $$

► **Proposition 11** ([14] chap. 4). $\mathcal{U}_I$ and $\mathcal{U}\mathcal{F}_I$ are Kan cubical sets.

**Proof.** Huber's proof lifts to $\mathcal{U}_I$ because the Kan structure of the families $h^I \vdash A$ is not used to define the Kan structure on $\mathcal{U}\mathcal{F}_I$ but only to show that the fillers of $\mathcal{U}\mathcal{F}_I$ are themselves Kan.

◀

### D Fibrancy rules in cSet

We now outline some proofs of fibrancy rules in the MLTT<sub>2</sub><sup>F</sup> model of Section 4.3.

► **Proposition 12.** The fibrancy rule for sigma types holds in cSet:

$$ \frac{\Gamma; \Delta \vdash A \mathbf{Kan} \quad \Gamma; \Delta, A \vdash B \mathbf{Kan}}{\Gamma; \Delta \vdash \Sigma A B \mathbf{Kan}} $$

**Proof.** A filler in $\Sigma A B$ is a pair made of a filler in $A$ and a filler in $B$. More formally, $[(\Sigma A B)(\delta)]_{S\bar{u}}$ is given by:

$$ (a, [B(\delta, a)]_S(\pi_2 \bar{u})) $$

$$ \text{where } a := [A(\delta)]_S(\pi_1 \bar{u}). $$

► **Proposition 13.** The fibrancy rule for identity types holds in cSet:

$$ \frac{\Gamma; \Delta \vdash A \mathbf{Kan} \quad \Gamma, \Delta \vdash t, t' : A}{\Gamma; \Delta \vdash \mathbf{Id}_A(t, t') \mathbf{Kan}} $$
18 Model structure on the universe in a two level type theory

**Proof.** Once again, the Huber proof lifts to degenerate fibrancy.

Let $I \in \square$, $S$ a shape on $I$ of direction $x$, $\rho \in \Gamma(I)$ degenerate along $x$, $\delta \in \Delta(\delta)$ and $\vec{u}$ an open-box of shape $S$ in $\mathrm{Id}_A(t, t')(\delta)$. Then for $(y, b) \in \langle S \rangle$:

$$u_{yb} \in \{ \omega \in A(\delta(y=b)s_{x_I}) | \omega(x_I = 0) = t\delta(y=b) \text{ and } \omega(x_I = 1) = t'\delta(y=b) \}$$

Let $S, x_I$ be the shape $S$ with $x_I$ added as a non principal direction. We extend $\vec{u}$ to an open-box on $S, x_I$ in $A(\delta s_{x_I})$ by:

$$u_{x_I 0} := t\delta$$

$$u_{x_I 1} := t'\delta$$

$\rho s_{x_I}$ is still degenerate along $x$ and coherences conditions are indeed satisfied. We thus get $[A(\delta s_{x_I})]_{S, x_I} \vec{u} \in A(\delta s_{x_I})$. We check that $[\mathrm{Id}_A(t, t')(\delta)]_{S} \vec{u} := [A(\delta s_{x_I})]_{S, x_I} \vec{u}$ suits. ◀

E Degenerate Fibrant Replacement in cSet

► Proposition 14. If $\Gamma \vdash A$ then $\Gamma \vdash \overline{A}$ **Kan**, and the fibrant replacement commutes with substitutions: for $\sigma : \Gamma' \to \Gamma$, $\overline{A\sigma} = \overline{A}\sigma$ as Kan cubical families.

**Proof.** First, we show that for all $I \in \square$ and $\rho \in \Gamma'$, the sets $\overline{A}\sigma(I, \rho)$ and $\overline{A}(I, \sigma_I(\rho))$ are equal. We show that each set is a subset of the other. The inclusion $\subseteq$ does not raise any problem, so we focus on the inclusion $\supseteq$. We show by induction on $u$ that:

$$\forall I \in \square, \forall \rho \in \Gamma'(I), \forall u \in \overline{A}(I, \sigma_I(\rho)), \quad u \in \overline{A}\sigma(I, \rho)$$

- If $u = \eta(u_0)$ with $u_0 \in A(\sigma_I(\rho)) = (A\sigma)(\rho)$, then $\eta(u_0)$ also belongs to $\overline{A}\sigma(\rho)$)

- If $u = \text{fill}_S(\vec{u})$ with $S$ on $I$ and $\vec{u}$ in $\overline{A}(\sigma_I(\rho))$. Then each $u_{yb}$ is in $\overline{A}(\sigma_{I,y}(\rho(y=b)))$, and then (by induction), in $\overline{A}\sigma(\rho(y=b))$. Then, $\text{fill}_S(\vec{u})$ also belongs to $\overline{A}\sigma(\rho)$)

- If $u = \text{comp}_S(\vec{u})$. This is the interesting case. Let $x$ be the direction of $S$, then $x \notin I$ and $S$ is on $I, x$. There is also a $\delta \in \Gamma(I, x)$, degenerate along $x$, such that $\delta(x = a) = \sigma_I(\rho)$. As $\delta$ is degenerate, we have $\delta = \sigma_{I,x}(\rho s_x)$. Then each $u_{yb}$ is in $\overline{A}(\sigma_{I,x,y}(\rho s_x(y=b)))$, and then (by induction), in $\overline{A}\sigma(\rho(y=b))$. Then, $\text{comp}_S(\vec{u})$ also belongs to $\overline{A}\sigma(\rho)$.

We remark that, in the last case, it is only because $\delta$ is degenerate that we can expose $u_{yb}$ as an element of $\overline{A}(\sigma_{I,x,y}(\dots))$ and thus apply the induction hypothesis. That is the step that doesn't work when considering the regular fibrant replacement (we give a counterexample in Appendix F).

$\overline{A}\sigma$ and $\overline{A}\sigma$ therefore have the same underlying sets. We easily conclude that they are equals as Kan families, as the restrictions are defined independently of the family, and the Kan structure is given by the **fill** elements in both cases. ◀

► Proposition 15. The rules $\overline{\mathrm{id}}_A \equiv \mathrm{id}_{\overline{A}}$ and $\overline{g} \circ \overline{f} \equiv \overline{g} \circ \overline{f}$ hold in cSet.

**Proof.** Let's consider the first rule for instance, the proof of the other one is similar.

$\overline{\mathrm{id}}_A$ is defined by induction, and sends **fill** and **comp** elements to filler and composition operations of $\overline{A}$. But the fillers and compositions of $\overline{A}$ are also the elements **fill** and **comp**. Hence, $\overline{\mathrm{id}}_A$ is the identity on $\overline{A}$. ◀
► Proposition 16. The following rule holds in cSet:

$$ \frac{\Gamma, A \vdash P : \mathcal{U}_i \quad \Gamma; A \vdash P \textbf{ Kan}}{\Gamma; \bar{A} \vdash \tilde{P} \textbf{ Kan}} $$

where $\tilde{P} := \text{repl\_rec}_{A, \mathcal{U}_i} P$.

**Proof.** We only give the proof that this rule holds in the case where $\Gamma$ is the empty context, and leave for future work the lifting of the proof to its full generality. In fact, in this case, we can directly use a result of Huber to conclude, namely, the fact that the cubical set $\mathcal{U}\mathcal{F}_i$ is itself fibrant [14, Chap. 4].

Given a cubical family $A \vdash Q$ in $\mathbf{Set}_i$, it is not hard to check that $Q$ is fibrant (.; $A \vdash Q$ Kan) if and only if the induced morphism of cubical sets $Q : A \to \mathcal{U}_i$ factorizes as:

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

Thus, we know that $P$ factorizes through $P'$ and we want also to factorize $\tilde{P}$ to get the following commuting diagram:

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

The dashed arrow is given by lifting $P'$ as a function from $\bar{A}$ to $\mathcal{U}\mathcal{F}_i$, using the fact that $\mathcal{U}\mathcal{F}_i$ is fibrant. The right triangle commutes because fillers of $\mathcal{U}\mathcal{F}_i$ and $\mathcal{U}_i$ are the same (and thus preserved by the inclusion). ◀

## F Counter example for the regular Fibrant Replacement

We give a counter example showing that the regular fibrant replacement does not commute with substitutions. This has already been noticed by various authors [1, 14, 8] but we provide an example (based on the proof of [1]) internally in cSet to get a better understanding of what goes wrong, in this particular setting, with the regular fibrant replacement. The regular fibrant replacement $\tilde{A}$ is defined as the degenerate one (Def. 20) but removing the degeneracy restriction in the definitions of fill and comp.

Let $\mathbb{I}$ be the cubical set defined by $\mathbb{I}(I) := I \sqcup 2$ representing the interval. The restriction induced by $f : I \to I'$ is defined by $zf = f(z)$ if $z \in I$ and $zf = z$ if $z \in 2$. And let $\mathbb{1}$ be the unit cubical set $(\mathbb{1}(I) = \{\star\})$.

We now define the cubical family $x : \mathbb{I} \vdash A$—representing the type $0 \equiv x$— by:

$$ \text{for all } I \in \square \text{ and } \rho \in \mathbb{I}(I), A\rho := \begin{cases} \{\star\} & \text{if } \rho = 0 \\ \emptyset & \text{otherwise} \end{cases} $$
and $\sigma : 1 \to \mathbb{I}$ the morphism given by $\sigma_I(\star) = 1$. The family $\widehat{A\sigma}$ represents $0 \equiv \widehat{1}$ while $\widehat{A\sigma}$ represents $0 \equiv \widehat{x} \{x := 1\}$. To show that both cubical sets are different, it suffices to remark that:

- For all $I$, $\widehat{A\sigma}(I, \star)$ is empty because the base case $\eta$ of the inductive-recursive type is always empty.

- $\widehat{A\sigma}(\emptyset, \star) = \widehat{A}(\emptyset, 1)$ is not empty because $\eta(\star)$ is in $\widehat{A}(\emptyset, x(x=0))$ and so $\text{comp}_S(\eta(\star))$ belongs to $\widehat{A}(\emptyset, x(x=1))$ for $S = (\{x\}; (x, 1); \emptyset)$. This element is in fact the transport of the term of $0 \equiv \widehat{0}$ along the segment $0 = 1$ of the interval.

Note that this proof can not be replayed with the degenerate fibrant replacement because $\text{comp}_S(\eta(\star))$ can not be formed due to the degeneracy restriction on $x$.