Models of Martin-L\"of type theory from algebraic weak factorisation systems

TL;DR

This paper introduces a new algebraic framework for modeling Martin-Löf type theory using weak factorisation systems, enabling the construction of various homotopy-theoretic models including groupoid and cubical set models.

Contribution

It develops the concept of type-theoretic algebraic weak factorisation systems and demonstrates their application in creating models of type theory, extending existing models and providing new construction methods.

Findings

Established a correspondence between algebraic weak factorisation systems and models of type theory.

Constructed examples including the groupoid and cubical set models.

Provided methods for generating models based on normal fibrations.

Abstract

We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations

Equations

$$\mathbb{E}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$B\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Gamma .A.A.{\mathsf{Id}}_A(x,y)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Gamma .A\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Delta .A[\sigma ]\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Delta .A[\sigma ].A[\sigma ].{\mathsf{Id}}_{A[\sigma ]}(x^{\prime },y^{\prime })\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\mathbb{E}}^R\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\mathsf{Id}}_f(a,b):{\mathsf{Id}}_B(a[\sigma ],b[\sigma ])\to {\mathsf{Id}}_A(a,b)to0.0pt,\text{hss}$$

$$\Delta .B\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Delta .B.B.{\mathsf{Id}}_B(x^{\prime },y^{\prime })\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\Sigma }_{A}B[\sigma ]:={\Sigma }_{A[\sigma ]}B[\sigma ]\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$({\Sigma }_{A}B,{\Sigma }_{A}B[-])[\sigma ]$$

$$=({\Sigma }_{A[\sigma ]}B[\sigma ],({\Sigma }_{A}B)[\sigma ][-])\text{(by def. of ΣAB[−]) to0.0pt.hss}$$

$$\big{(}\mathsf{Id}_{A}(a,b),\mathsf{Id}_{A}(a,b)[-]\big{)}$$

$${\mathsf{Id}}_{{\sigma }^{\ast }}(a,b):{\mathsf{Id}}_{A[\sigma ]}(a[\sigma ],b[\sigma ])\to {\mathsf{Id}}_A(a,b)$$

$${\mathsf{Id}}_{A[\sigma ]}(a[\sigma ],b[\sigma ])={\mathsf{Id}}_A(a,b){\mathsf{Id}}_{{\sigma }^{\ast }}(a,b)=1_{{\mathsf{Id}}_A(a,b)}to0.0pt,\text{hss}$$

$$({\mathsf{Id}}_A(a,b)[\sigma ],{\mathsf{Id}}_A(a,b)[\sigma ][-])=({\mathsf{Id}}_{A[\sigma ]}(a[\sigma ],b[\sigma ]),{\mathsf{Id}}_{A[\sigma ]}(a[\sigma ],b[\sigma ])[-]).$$

$$\Gamma .A.A.{\mathsf{Id}}_A\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Gamma .A\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Delta .B\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\Delta .B.B.{\mathsf{Id}}_B\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 20.58322pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\crcr}}}\ignorespaces{\hbox{\kern-20.58322pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{Id}_{A}(a,b)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 52.41376pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 10.18231pt\raise 0.0pt\hbox{\ignorespaces\ignorespaces\hbox{\kern 0.0pt\raise-10.18231pt\hbox{\hbox{\kern 5.0pt\lower 0.0pt\hbox{\lower 0.0pt\hbox{\line@@}}}\hbox{\kern 0.0pt\lower 0.0pt\hbox{\lower-5.0pt\hbox{\line@@}}}\hbox{}}}}}}{\hbox{\kern 52.41376pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{Id}_{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.125pt\raise-38.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Gamma\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 21.00195pt\raise-44.91666pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{(a,b)}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 44.58322pt\raise-38.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 44.58322pt\raise-38.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Gamma.A.A\hbox to0.0pt{.\hss}}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$$

$${\mathsf{Id}}_{A[\sigma ]}(a[\sigma ],b[\sigma ])\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\mathsf{Id}}_A(x,y)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$X\stackrel{Lf}{\to }Qf\stackrel{Rf}{\to }Y$$

$$\text{L-Map}\to {\mathbb{C}}^{\to }\text{and}\text{R-Map}\to {\mathbb{C}}^{\to }to0.0pt.\text{hss}$$

$$\text{CAT}/{\mathbb{C}}^{\to }\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$R$$

$$\text{R-Map}/X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

Full text

Introduction

Context and motivation The construction of category-theoretic models of Martin-Löf type theory [29] is a complex task that involves two main problems. First, one needs to find a category with sufficient structure, so as to be able to interpret the type-formation rules, e.g. those for dependent sum and dependent product types ($\Sigma$-types and $\Pi$-types, respectively, for short). In particular, in order to have a model with intensional identity types ($\mathsf{Id}$-types for short), the category under consideration needs to possess some homotopy-theoretic structure, as given for example by a weak factorisation system (wfs for short) [1, 13, 27]. Secondly, one has to transform the category under consideration into a genuine model of Martin-Löf type theory, in which certain strictness conditions (needed to model correctly the substitution operation) are required to hold, as in a split comprehension category [21, 22]. As these conditions are rarely satisfied in practice, this second step often involves applying suitable general coherence theorems, analogous to Mac Lane’s theorem relating monoidal categories and strict monoidal categories [25]. To make things more difficult, these two issues are closely related.

There are two main methods to address the strictness issues, to which we refer as the left and right adjoint splitting, [9, 18, 24], since they are based on the left and the right adjoint to the inclusion of split Grothendieck fibrations into Grothendieck fibrations, respectively [16, 34]. The right adjoint splitting was already used in [18] in order to remedy the issues affecting the interpretation of Martin-Löf type theory in locally Cartesian closed categories [33], thus accounting for $\Sigma$-types, $\Pi$-types and extensional $\mathsf{Id}$-types. Subsequently, Warren isolated sufficient conditions to apply the right adjoint splitting and produce models with intensional $\mathsf{Id}$-types [35]. These conditions, however, are not generally satisfied in categories equipped with weak factorisation systems, giving the impression, apparently widespread in the research community, that the right adjoint splitting cannot be used to construct homotopy-theoretic models of Martin-Löf type theories and that the left adjoint splitting should be used instead, applying the results in [24].

Our aim in this paper is to show that this impression is wrong and that the right adjoint splitting can be applied to obtain homotopy-theoretic models of Martin-Löf type theory. The key observation underpinning this work, which was suggested by Garner (see [35, p. 34]), is that the right adjoint splitting can be applied provided that we work with algebraic, rather than ordinary, weak factorisation systems (awfs’s for short) [15, 17] (see also [5, 6, 30]). In an awfs, the lifting properties that are part of the definition of a wfs are replaced by lifting structures, satisfying a naturality condition. As we will see, it is the algebraic character of awfs’s that allows us to apply the right adjoint splitting.

While awfs’s may seem cumbersome, there are situations in which it is actually more natural to consider awfs’s than wfs’s, most notably in the ongoing work aimed at defining homotopy-theoretic models of Martin-Löf’s in a constructive metatheory [7, 12, 14]. Indeed, the left adjoint splitting used in [24] seems to work only under certain exponentiability assumptions, which are not constructively valid in simplicial sets [4]. Issues of constructivity are also the main motivation for our work on normal uniform fibrations, as explained further below.

Main results. This paper makes two main contributions. The first is to introduce type-theoretic awfs’s and show that they give rise to models of Martin-Löf’s type theory with $\Sigma$-types, $\Pi$-types and $\mathsf{Id}$-types. The second is to introduce a general method to obtain examples of type-theoretic awfs’s and to give a homogeneous account of several models in which dependent types are interpreted as uniform fibrations (in the sense of [7, 14]), including the groupoid model [20], in which dependent types are interpreted as split fibrations, and models based on simplicial and cubical sets [7, 14], in which dependent types are interpreted as uniform Kan fibrations.

Our construction of models of Martin-Löf type theory from type-theoretic awfs’s is obtained in two steps. The first is to define a non-split comprehension category from a type-theoretic awfs (Proposition 3.2) and show that this comprehension category is equipped with pseudo-stable $\Sigma$-types, $\Pi$-types and $\mathsf{Id}$-types (Theorem 3.11) in the sense of [24], i.e. commuting with substitution up to isomorphism. The second step is to apply the right adjoint splitting and turn the non-split comprehension category obtained in the first step into a split one equipped with strictly stable $\Sigma$-types, $\Pi$-types and $\mathsf{Id}$-types (Theorem 1.6). It should be noted that the extra algebraic structure of a type-theoretic awfs is crucial to have pseudo-stable $\mathsf{Id}$-types in the non-split comprehension category (cf. [3]) and this, in turn, is essential to apply the right adjoint splitting. As an illustration, we revisit the groupoid model of Martin-Löf type theory [20]. Specifically, we equip the category of groupoids Gpd with an awfs whose right maps correspond to normal isofibrations and then we prove that such awfs is type-theoretical. In this way, we show that the original groupoid model can be obtained as the split comprehension category associated to this type-theoretic awfs. Since the appearance of this paper as a preprint, these results have been extended to internal groupoids [11] and to split isofibrations [36].

Our results on constructing type-theoretic awfs’s build on the theory of uniform fibrations in [14]. Our Theorem 5.10 isolates structure on Grothendieck topos that suffices to produce a type-theoretic awfs of uniform fibrations. We call a Grothendieck topos equipped with such structure a type-theoretic suitable topos (Definition 5.9). We then show that any Grothendieck topos equipped with an interval object with connections is an example of a type-theoretic suitable topos. The main technical machinery used in the proof of Theorem 5.10 is Proposition 5.8, where we show that given a type-theoretic suitable topos, the resulting awfs of uniform fibrations can be equipped with a stable functorial choice of path objects, which is the structure necessary to produce pseudo-stable identity types. This result fills the gap between the theory developed in [14] and its intended application to the construction of models of Martin-Löf type theory.

We also advance the theory of [14] by introducing a stronger version uniform fibrations, which we call normal uniform fibrations, in which the lifts are required to preserve degeneracies. These can be seen as generalisations of normal cloven isofibrations in groupoids, as explained in Remark 6.5. We then show that the ideas in [14] can be adapted so as to accommodate this new normality property. With this, we prove that any suitable topos admits an awfs of normal uniform fibrations (Theorem 6.2).

One of the reasons for our interest in normal uniform fibrations is that they allow us to avoid one of the hypotheses for a type-theoretic suitable topos $\mathbb{E}$ when constructing a type-theoretic awfs (Theorem 7.10). The requirement on $\mathbb{E}$ is that for any object $X\in\mathbb{E}$, the reflexivity map $r_{X}:X\rightarrow X^{I}$, that maps a point of $X$ to the constant path on it, is a member of a distinguished class of monomorphisms $\mathcal{M}$ whose members are to be thought as generating cofibrations. While this assumption holds if we consider $\mathcal{M}$ to be the class of all monomorphisms, it fails in some situations that are of interest for constructive mathematics. For example, if $\mathbb{E}$ is a presheaf topos and we restrict our attention to $\mathcal{M}_{dec}$ the class of decidable monomophisms (i.e. those whose image is level-wise constructively decidable). As noted in [28], it is important to consider decidable monomorphisms when trying to model univalent universes. This issue is also relevant to the question of whether the path types and the identity types coincide in the cubical type theory of [7].

Outline of the paper. Section 1 reviews the interpretation of type dependency using comprehension categories and the right adjoint splitting. Section 2 reviews algebraic weak factorisation systems. In Section 3 we introduce type-theoretic awfs’s and prove that the induced comprehension categories support pseudo-stable $\Pi$-types, $\Sigma$-types and $\mathsf{Id}$-types. We then move on to the construction of examples of type-theoretic awfs. In Section 4 we revisit the groupoid model. In Section 5 we show how to construct a type-theoretic awfs from a type-theoretic suitable topos. In Section 6 we introduce the awfs of normal uniform fibrations and in Section 7 we show that it is type-theoretic.

Acknowledgements. Nicola Gambino gratefully acknowledges the support of EPSRC under grant EP/M01729X/1, of the US Air Force Office for Scientific Research under agreement FA8655-13-1-3038 and the hospitality of the School of Mathematics of the University of Manchester while on study leave from the University of Leeds. Marco Federico Larrea would like to thank the Mexican National Council for Science and Technology (CONACyT) for the financial support during his PhD. We are grateful to Steve Awodey, John Bourke, Thierry Coquand, Peter Lumsdaine, Paige North (who spotted an inaccuracy in an earlier version of Proposition 3.3), Andy Pitts, Christian Sattler, Raffael Stenzel, Andrew Swan and Thomas Streicher for helpful discussions. We are also thankful to the referee for helpful suggestions.

1. Strict stability, pseudostability and coherence

We review basic notions and results on Grothendieck fibrations and comprehension categories, referring to [22, 34] for more information. A comprehension category over a category $\mathbb{C}$ consists of a strictly commutative diagram of the form

[TABLE]

$\text{cod}\colon\mathbb{C}^{\rightarrow}\rightarrow\mathbb{C}$ is the codomain functor, such that $\rho\colon\mathbb{E}\rightarrow\mathbb{C}$ is a Grothendieck fibration, and $\chi\colon\mathbb{E}\rightarrow\mathbb{C}^{\rightarrow}$ maps Cartesian arrows in $\mathbb{E}$ to pullback squares in $\mathbb{C}$. We refer to such a comprehension category by the tuple $(\mathbb{C},\rho,\chi)$ or by the pair $(\rho,\chi)$ if the category $\mathbb{C}$ is easily inferable from the context. A cleavage for $(\mathbb{C},\rho,\chi)$ consists of a choice of lifts for the fibration $\rho$, i.e. for each $u\colon\Delta\rightarrow\Gamma$ in $\mathbb{C}$ and $A$ over $\Gamma$, a Cartesian morphism $u^{*}\colon~{}A[u]~{}\rightarrow~{}A$ over $u$. We will refer to $A[u]$ as the reindexing of $A$ along $u$. A cleavage is normal if it preserves identities and is split if it preserves identities and composition. A split comprehension category is a comprehension category equipped with a split cleavage. Occasionally, we will make use the following notation:

[TABLE]

where the diagram on the left indicates that $f$ is an arrow in $\mathbb{E}$, $\sigma$ is an arrow in $\mathbb{C}$ and $\rho(f)=\sigma$. The pullback notation on the diagram on the right indicates that, in addition to the previous data, $f$ is Cartesian.

A split comprehension category $(\mathbb{C},\rho,\chi)$ provides a natural setting to interpret the basic judgements and the structural rules of a dependent type theory [22]. Type-theoretic contexts are interpreted as objects of $\mathbb{C}$. A judgement $\Gamma\vdash A\colon\mathsf{type}$ is interpreted as an object $A$ in the fibre of $\rho$ over $\Gamma\in\mathbb{C}$. Context extension is modelled via the comprehension functor: for an object $A$ in the fibre over $\Gamma$ there is a morphism $\chi_{A}\colon\Gamma.A\rightarrow\Gamma$ whose domain $\Gamma.A$ is the interpretation of the context extension. A judgement $\Gamma\vdash a\colon A$ is interpreted as a map $a\colon\Gamma\to\Gamma.A$ in $\mathbb{C}$ which is a section of $\chi_{A}\colon\Gamma.A\to\Gamma$.

Substitution of terms into types is interpreted with the use of the split cleavage, while substitution of terms into terms is interpreted by composition. Weakening is modelled by reindexing an object $A$ along a morphism of the form $\chi_{B}:\Gamma.B\rightarrow\Gamma$. For simplicity, the comprehension of $A[\chi_{B}]$ is written $\chi_{B,A}\colon\Gamma.B.A\rightarrow\Gamma.B$.

In order to model type-theoretic constructs, we require a split comprehension category to be equipped with additional, chosen, structure. Furthermore, this structure must cohere strictly with the split cleavage, so as to ensure validity of substitution rules. Definition 1.1 and Definition 1.2 describe the structure necessary to model $\mathsf{Id}$-types. The corresponding structure for $\Sigma$-types and $\Pi$-types is defined in Appendix A.

Definition 1.1**.**

A choice of $\mathsf{Id}$-types on a comprehension category $(\mathbb{C},\rho,\chi)$ consists of the following data.

1. (1)

For each $A$ in the fibre over $\Gamma$ and $a,b\colon\Gamma\to\Gamma.A$ sections of $\chi_{A}$, an object $\mathsf{Id}_{A}(a,b)$ over $\Gamma$. 2. (2)

For each $A$ over $\Gamma$, a section $r_{A}$ over the diagonal morphism $\delta_{A}$, giving a factorisation:

[TABLE]

where $\mathsf{Id}_{A}(x,y)$ is given by $(1)$ applied to the weakened type $A$ over $\Gamma.A.A$ and to the canonical variables $x,y\colon\Gamma.A.A\to\Gamma.A.A.A$. 3. (3)

For any $A$ over $\Gamma$, $C$ over $\Gamma.A.A.\mathsf{Id}_{A}(x,y)$ and $t$ a section of $C$ over $r_{A}$ as shown by the solid arrows in the following diagram:

[TABLE]

a section $j_{A}(C,t)$ of $C$ (shown as the dotted arrow) making both triangles commute.

We refer to a choice of $\mathsf{Id}$-types by $(\mathsf{Id},r,j)$. Similarly, we refer to a choice of $\Sigma$-types as $(\Sigma,pair,sp)$ and to a choice of $\Pi$-types as $(\Pi,\lambda,app)$ (see Appendix A for details).

Definition 1.2**.**

Assume $(\mathbb{C},\rho,\chi)$ is split and is equipped with a choice $(\mathsf{Id},r,j)$ of $\mathsf{Id}$-types. We say that the choice is strictly stable if for every morphism $\sigma\colon\Delta\rightarrow\Gamma$ in the base category, and for every object $A$ in the fibre over $\Gamma$, the following conditions are satisfied:

1. (1)

For any pair of sections $a,b\colon\Gamma\to\Gamma.A$, we have that $\mathsf{Id}_{A[\sigma]}(a[\sigma],b[\sigma])=\mathsf{Id}_{A}(a,b)[\sigma]$. 2. (2)

The following diagram commutes

[TABLE]

where the horizontal arrows are given by split reindexing along $\sigma$ 3. (3)

For any $(C,t)$ as in $(3)$ of Definition 1.1, we can obtain a second pair $(C[\sigma],t[\sigma])$ relative to $\mathsf{Id}_{A[\sigma]}(x^{\prime},y^{\prime})$ by reindexing along $\sigma$. We require following diagram to commute:

[TABLE]

where the horizontal arrows are given by reindexing along $\sigma$.

While split comprehension categories provide a sound interpretation of type theory, non-split comprehension categories arise most naturally in examples. This mismatch can be remedied by applying a well-known construction by Giraud and Bénabou [16] that replaces a comprehension category $(\mathbb{C},\rho,\chi)$ with an equivalent split one $(\mathbb{C},\rho^{R},\chi^{R})$, universally as a right adjoint functor. We review this construction.

Definition 1.3**.**

Let $(\mathbb{C},\rho,\chi)$ be a comprehension category and $A$ an object in the fibre over $\Gamma\in\mathbb{C}$. A local cleavage for $A$ consists of an operation $A[-]$ that assigns to each map $\sigma:\Delta\rightarrow\Gamma$ a Cartesian arrow $\sigma^{*}\colon A[\sigma]\rightarrow A$ over $\sigma$. We say that a local cleavage $A[-]$ is normal if when applied to the identity $1_{\Gamma}\colon\Gamma\rightarrow\Gamma$ it outputs the identity arrow, i.e. $A[1_{\Gamma}]=A$ and $1_{\Gamma}^{*}=1_{A}$.

For a fibration $\rho\colon\mathbb{E}\rightarrow\mathbb{C}$ the category $\mathbb{E}^{R}$ is defined as follows. Its objects are pairs $(A,A[-])$, where $A$ is an object of $\mathbb{E}$ and $A[-]$ is a local normal cleavage for $A$. An arrow $f\colon(B,B[-])\rightarrow(A,A[-])$ is just an arrow $f\colon B\rightarrow A$ in $\mathbb{E}$. Composition and identities are just those of $\mathbb{E}$. Notice that there is a functor $\rho^{R}\colon\mathbb{E}^{R}\rightarrow\mathbb{C}$ given on objects by $\rho^{R}(A,A[-])=\rho(A)$. The next lemma is well-known [9, 16].

Lemma 1.4**.**

The functor $\rho^{R}\colon\mathbb{E}^{R}\rightarrow\mathbb{C}$ is a split Grothendieck fibration. ∎

This construction extends to comprehension categories. Fix a comprehension category $(\mathbb{C},\rho,\chi)$. First, we have a morphism $\epsilon_{\rho}\colon\rho^{R}\rightarrow\rho$ of fibrations (i.e. a functor over $\mathbb{C}$ that preserves Cartesian arrows) that acts on an object $(A,A[-])$ of $\mathbb{E}^{R}$ by forgetting the local normal cleavage. Then, we obtain a split comprehension category $(\mathbb{C},\rho^{R},\chi^{R})$, by letting $\chi^{R}$ be the composite in

[TABLE]

It is natural to ask what structure on a cloven comprehension category gives rise to strictly stable $\Sigma$, $\Pi$, and identity types on its right adjoint splitting. As we discuss below, one needs a choice of $\Sigma$, $\Pi$, and $\mathsf{Id}$-types which are pseudo-stable.

Definition 1.5**.**

A choice $(\mathsf{Id},r,j)$ of $\mathsf{Id}$-types in a comprehension category is said to be pseudo-stable if for any Cartesian arrow $f\colon B\rightarrow A$ over a morphism $\sigma\colon\Delta\rightarrow\Gamma$ in the base, the following conditions are satisfied:

1. (1)

For any pair of sections $a,b\colon\Gamma\to\Gamma.A$, there is a Cartesian arrow

[TABLE]

over $\sigma\colon\Delta\rightarrow\Gamma$. Moreover, the assignment $f\mapsto\mathsf{Id}_{f}(a,b)$ is functorial, that is, $\mathsf{Id}_{1_{A}}(a,b)=1_{\mathsf{Id}_{A}(a,b)}$ and $\mathsf{Id}_{f\circ g}(a,b)=\mathsf{Id}_{f}(a,b)\circ\mathsf{Id}_{g}(a[\sigma],b[\sigma])$. 2. (2)

The following diagram commutes:

[TABLE] 3. (3)

For any pair $(C,t)$ as in $(3)$ of Definition 1.1 and for any Cartesian $h\colon C^{\prime}\rightarrow C$ over $\mathsf{Id}_{f}$, we can construct a pair $(C^{\prime},t^{\prime})$ by pulling back $t$ along $h$ appropriately. We require that the following diagram commutes:

[TABLE]

where the lower horizontal arrow is the (comprehension of the) Cartesian arrow $h\colon C^{\prime}\rightarrow C$.

The definition of pseudo-stability for $\Sigma$-types and $\Pi$-types is given in Appendix A. The following coherence result connects pseudo-stability in a comprehension category and strict stability on its right adjoint splitting. The proof is based on [18, Theorem 2] for $\Sigma$-types and $\Pi$-types and on [35, Theorem 2.48] for $\mathsf{Id}$-types.

Theorem 1.6** (Coherence Theorem).**

Let $(\mathbb{C},\rho,\chi)$ be a comprehension category equipped with pseudo-stable choices of $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types. Then the right adjoint splitting $(\mathbb{C},\rho^{R},\chi^{R})$ is equipped with strictly stable choices of $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types; and the counit $\epsilon_{\rho}\colon(\mathbb{C},\rho^{R},\chi^{R})\rightarrow(\mathbb{C},\rho,\chi)$ preserves each choice of logical structure strictly.

Proof.

For $\Sigma$-types, let us consider a dependent tuple (see Appendix A for definition) $(\Gamma,(A,A[-]),(B,B[-]))$ of $(\rho^{R},\chi^{R})$. The $\Sigma$-type associated to this tuple has the following form: $(\Sigma_{A}B,\Sigma_{A}B[-])$ where $\Sigma_{A}B$ is the $\Sigma$-type given by the pseudo-stable choice of $(\rho,\chi)$ applied to $(\Gamma,A,B)$. The component at $\sigma\colon\Delta\rightarrow\Gamma$ of the local cleavage $\Sigma_{A}B[-]$ is given as follows. First, we use the local cleavages $A[-]$ and $B[-]$ to construct a Cartesian arrow of dependent tuples $(\sigma,f^{*},g^{*})\colon(\Delta,A[\sigma],B[\sigma])\rightarrow(\Gamma,A,B)$ where the arrows $f^{*}$ and $g^{*}$ are given by the local cleavage (see Definition 1.3). Then, we use the action on morphisms of the pseudo-stable choice of $\Sigma$-types to define:

[TABLE]

This local cleavage is normal because the pseudo-stable choice is functorial.

We must show that this choice is strictly stable. By definition, for $\sigma\colon\Delta\rightarrow\Gamma$,

[TABLE]

It only remains to show that the local cleavages $(\Sigma_{A}B)[\sigma][-]$ and $(\Sigma_{A[\sigma]}B[\sigma])[-]$ coincide, but this follows from the functoriality of the pseudo-stable choice of $\Sigma$-types in $(\rho,\chi)$.

The construction for the case of dependent products or $\Pi$-types is completely analogous and hence omitted.

For $\mathsf{Id}$-types, note that the terms of a type $(A,A[-])$ in $(\mathbb{C}^{R},\rho^{R},\chi^{R})$ are the same as the terms of $A$ in $(\mathbb{C},\rho,\chi)$. Let $(A,A[-])$ be an object in the fibre of $\rho^{R}$ over $\Gamma$, and consider sections $a,b\colon\Gamma\to\Gamma.A$. We need an object in $\mathbb{E}^{R}$ over $\Gamma.A.A$, which we denote as

[TABLE]

for brevity. The object $\mathsf{Id}_{A}(a,b)$ is obtained by applying the pseudo-stable choice of $\mathsf{Id}$-types in $(\rho,\chi)$ to $A$ and the sections $a,b\colon\Gamma\to\Gamma.A$.

To define the local normal cleavage $\mathsf{Id}_{A}(a,b)[-]$, consider $\sigma\colon\Delta\rightarrow\Gamma$ in $\mathbb{C}$. The local normal cleavage $A[-]$ gives a Cartesian arrow $\sigma^{*}\colon A[\sigma]\rightarrow A$ over $\sigma$. Using the stable functorial choice of $\mathsf{Id}$-types of $(\rho,\chi)$, we get the Cartesian arrow

[TABLE]

over $\sigma$. We then let $\mathsf{Id}_{A}(a,b)[\sigma]:=\mathsf{Id}_{A[\sigma]}(a[\sigma],b[\sigma])$, so that the Cartesian arrow to $\mathsf{Id}_{A}(a,b)$ can be taken to be $\mathsf{Id}_{\sigma^{*}}(a,b)$. By pseudo-stability, if $\sigma=1_{A}$ then

[TABLE]

as required. It remains to check that this choice is strictly stable. For $\sigma\colon\Delta\rightarrow\Gamma$ and sections $a,b\colon\Gamma\to\Gamma.A$, we must verify that:

[TABLE]

By definition, $\mathsf{Id}_{A}(a,b)[\sigma]$ is given by the local normal cleavage $\mathsf{Id}_{A}[-]$ applied to the arrow $\sigma^{*}$, which is $\mathsf{Id}_{A[\sigma]}(a[\sigma],b[\sigma])$. By the functoriality of the pseudo-stable choice of $\mathsf{Id}$-types, the local cleavages $\mathsf{Id}_{A}(a,b)[\sigma][-]$ and $\mathsf{Id}_{A[\sigma]}(a[\sigma],b[\sigma])[-]$ coincide. ∎

In the next sections we show how to construct comprehension categories with pseudo-stable choices of $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types. For $\mathsf{Id}$-types, the structure that arises more naturally in example corresponds to the so-called variable-based formulation of $\mathsf{Id}$-types [13, Table 3], which is known to be equivalent to the usual formulation. We define this variant in Definition 1.7 and then show that it is equivalent to the notion of Definition 1.1.

Definition 1.7**.**

A choice of variable-based $\mathsf{Id}$-types on a comprehension category $(\mathbb{C},\rho,\chi)$ consists of an operation that assigns a tuple $(\mathsf{Id}_{A},r_{A},j_{A})$, to each object $A$ in the fibre over some $\Gamma\in\mathbb{C}$, where:

1. (1)

$\mathsf{Id}_{A}$ is an object in the fibre over $\Gamma.A.A$, 2. (2)

$r_{A}$ is a section of $\mathsf{Id}_{A}$ over the diagonal morphism $\delta_{A}$, giving a factorisation

[TABLE] 3. (3)

$j_{A}$ is an operation that takes a pair $(C,t)$, where $C$ is an object $C$ in the slice over $\Gamma.A.A.\mathsf{Id}_{A}$ and $t$ is a section of $C$ over $r_{A}$, as in the diagram of solid arrows

[TABLE]

to a section $j_{A}(C,t)$ of $C$ (shown as the dotted arrow) making both triangles commute.

We will refer to a choice of variable-based $\mathsf{Id}$-types by $(\mathsf{Id}_{v.b.},r,j)$.

Definition 1.8**.**

A choice of variable-based $\mathsf{Id}$-types $(\mathsf{Id}_{v.b.},r,j)$ in a comprehension category is said to be pseudo-stable if for any Cartesian arrow $f\colon B\rightarrow A$ over a morphism $\sigma\colon\Delta\rightarrow\Gamma$ in the base, the following conditions are satisfied.

1. (1)

There is a Cartesian arrow $\mathsf{Id}_{f}\colon\mathsf{Id}_{B}\rightarrow\mathsf{Id}_{A}$ over the canonical morphism $\delta_{f}\colon\Delta.B.B\rightarrow\Gamma.A.A$, and the assignment $f\mapsto\mathsf{Id}_{f}$ is functorial, i.e. $\mathsf{Id}_{1_{A}}=1_{\mathsf{Id}_{A}}$ and $\mathsf{Id}_{f\circ g}=\mathsf{Id}_{f}\circ\mathsf{Id}_{g}$. 2. (2)

The following diagram commutes:

[TABLE] 3. (3)

For any pair $(C,t)$ as in $(3)$ of Definition 1.7 and for any Cartesian $h\colon C^{\prime}\rightarrow C$ over $\mathsf{Id}_{f}$, we can construct a pair $(C^{\prime},t^{\prime})$ by pulling back $t$ along $h$ appropriately. We require that the following diagram commutes:

[TABLE]

where the lower horizontal arrow is the (comprehension of the) Cartesian arrow $h\colon C^{\prime}\rightarrow C$.

Proposition 1.9**.**

A cloven comprehension category $(\mathbb{C},\rho,\chi)$ is equipped with a pseudo-stable choice of $\mathsf{Id}$-types if and only if it is equipped with a pseudo-stable choice of variable-based $\mathsf{Id}$-types.

Proof.

Suppose we have a pseudo-stable choice of $\mathsf{Id}$-types. To construct a pseudo-stable choice of variable-based $\mathsf{Id}$-types, consider an object $A$ over $\Gamma$, we define $\mathsf{Id}_{A}:=\mathsf{Id}_{A}(x,y)$ over $\Gamma.A.A$ using the canonical variables $x,y\colon\Gamma.A.A\to\Gamma.A.A.A$. The operations $r$ and $j$ are given just as in Definition 1.5.

For the converse, assume a pseudo-stable choice of variable-based $\mathsf{Id}$-types. Consider an object $A$ over $\Gamma$ and sections $a,b\colon\Gamma\to\Gamma.A$. We have $\mathsf{Id}_{A}$ over $\Gamma.A.A$, and thus, we can define $\mathsf{Id}_{A}(a,b)$ to be the reindexing of $Id_{A}$ along $(a,b)\colon\Gamma\to\Gamma.A.A$, as in

[TABLE]

We can extend this definition to provide the rest of the data in part $(1)$ of Definition 1.5. Consider $f\colon B\to A$ Cartesian over $\sigma\colon\Delta\to\Gamma$, then we have

[TABLE]

where $\mathsf{Id}_{f}(a,b)\colon\mathsf{Id}_{B}(a[\sigma],b[\sigma])\rightarrow\mathsf{Id}_{A}(a,b)$ is given uniquely by the universal property of the square in (1.1). If $f$ (and $\sigma$) are identities, then by pseudo-stability of $\mathsf{Id}$-types, $Id_{f}\colon Id_{A}\to Id_{A}$ is also the identity, and thus $\mathsf{Id}_{f}(a,b)$ must be the identity by the uniqueness property that characterises it. Similarly, the pseudo-stability of the variable-based $\mathsf{Id}$-types and the uniqueness property of $\mathsf{Id}_{f}(a,b)$ can be used to show that this operation preserves composition.

For the operations $r$ and $j$, we first consider the diagram

[TABLE]

where the square on the right is obtained by the functoriality of the pseudo-stable choices of variable-based $\mathsf{Id}$-types to $\chi_{A,A}\colon\Gamma.A.A\to\Gamma$. The square on the left is obtained by definition of $\mathsf{Id}_{A}(x,y)$ applied to the object $A$ weakened to $\Gamma.A.A$ and to the variables $x,y\colon\Gamma.A.A\to\Gamma.A.A.A$. Both top horizontal arrows are Cartesian and the composition of the bottom two arrows equals the identity. Thus $\mathsf{Id}_{A}(x,y)\cong\mathsf{Id}_{A}$ as objects over $\Gamma.A.A$. We can then transport the operations $r$ and $j$ along this isomorphism. ∎

Remark 1.10**.**

The reason for introducing two versions of identity types is that examples give rise more natually to the variable-based $\mathsf{Id}$-types of Definition 1.7, while the coherence theorem Theorem 1.6 is easier to prove constructively with the identity types of Definition 1.1. Indeed, if one works with variable-based $\mathsf{Id}$-types and tries to follow the argument used for $\Sigma$- and $\Pi$-types, the construction of the local cleavage seems to require a case distiction on whether the argument is an identity or not to ensure functoriality.

Our goal in the reminder of the paper is to construct and study comprehension categories equipped with pseudo-stable choices of $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types. By Theorem 1.6, these will give rise to genuine models of Martin-Löf type theory with $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types.

2. Algebraic weak factorisation systems

We review some of the basic theory on algebraic weak factorisation systems and on orthogonal categories of arrows [5, 6, 15, 17]. These will be the basis for our definition of a type-theoretic algebraic weak factorisation system in Section 3.

First of all, recall that a functorial factorisation $(Q,L,R)$ on a category $\mathbb{C}$ consists of an operation that assigns to each arrow $f\colon X\rightarrow Y$ a factorisation

[TABLE]

functorially in $f$. The induced endofunctors $L,R\colon\mathbb{C}^{\rightarrow}\rightarrow\mathbb{C}^{\rightarrow}$ are canonically copointed and pointed respectively; that is, there are a counit $\epsilon\colon L\rightarrow 1$ and a unit $\eta\colon 1\rightarrow R$. We denote the category of $(R,\eta)$-algebras as $R$-Map and the category of $(L,\epsilon)$-coalgebras by $L$-Map, and refer to their objects also as $R$-maps and $L$-maps, respectively. There are faithful, but not full, forgetful functors to the arrow category,

[TABLE]

Let $(g,\lambda)\colon A\rightarrow B$ be an $L$-map, $(f,s)\colon X\rightarrow Y$ an $R$-map and $(h,k)\colon g\rightarrow f$ a morphism in the arrow category. Then we can construct a filler for the square $(h,k)$, which is given by $j\colon=s\cdot Q(h,k)\cdot\lambda$, where $Q(h,k)\colon Qg\rightarrow Qf$ is the map obtained by applying the functorial factorisation to $(h,k)$. These fillers satisfy naturality conditions with respect to morphism of $L$-maps and $R$-maps.

Definition 2.1**.**

An algebraic weak factorisation system (awfs for short) on a category $\mathbb{C}$ consists of the following data:

1. (1)

a functorial factorisation $(Q,L,R)$ on $\mathbb{C}$, 2. (2)

an extension of the pointed endofunctor $(R,\eta)$ to a monad $(R,\eta,\mu)$, 3. (3)

an extension of the copointed endofuctor $(L,\epsilon)$ to a comonad $(L,\epsilon,\delta)$, 4. (4)

the canonical map $\Delta\colon LR\rightarrow RL$ defined using the monad and comonad structure is a distributive law.

We refer to an awfs as in Definition 2.1 just as $(L,R)$. Item (4) of Definition 2.1 is a technical requirement which plays no role in this work. Given an awfs as Definition 2.1, we have also the category of algebras for the monad $(R,\eta,\mu)$, which we denote $R$-Alg, and the category of coalgebras for the comonad $(L,\epsilon,\delta)$, which we denote $L$-Coalg. We refer to the objects of $R$-Alg and $L$-Coalg as $R$-algebras and $L$-coalgebras, respectively. There are full and faithful functors \text{{R-Alg}}\hookrightarrow\text{{R-Map}} and \text{{L-Coalg}}\hookrightarrow\text{{L-Map}}.

Remark 2.2**.**

The category $R$-Alg (and also $R$-Map) is closed under ‘vertical’ composition; that is if $(f,s)\colon X\rightarrow Y$ and $(f^{\prime},s^{\prime})\colon Y\rightarrow Z$ are $R$-algebras then there is a canonical $R$-algebra structure $s^{\prime}\cdot s$ on the composite $f^{\prime}\cdot f$. In fact, finding such a vertical composition operation provides a complete characterisations of the awfs [2, Theorem 4.15].

Also, for an $R$-algebra $(f,s)$ and a pullback square $(h,k)\colon f^{\prime}\rightarrow f$ then, there exists a unique $R$-algebra structure $s^{\prime}$ on $f^{\prime}$ making $(h,k)$ a morphism of $R$-algebras. The same result holds for $R$-maps.

We recall some notions regarding categories of arrows and of orthogonality in the setting of awfs’s. By a category of arrows over $\mathbb{C}$ we mean a functor $u\colon\mathcal{J}\rightarrow\mathbb{C}^{\rightarrow}$ where $\mathcal{J}$ is a category. A right $\mathcal{J}$-map consists of a pair $(f,\theta)$ where $f\colon X\rightarrow Y$ is an arrow of $\mathbb{C}$ and $\theta$ is a right lifting operation against $\mathcal{J}$, i.e. $\theta$ assigns a filler $\theta(i)$ to each commutative square of the form $(l,m)\colon u_{i}\rightarrow f$, with $i\in\mathcal{J}$. These fillers, in addition, are compatible with the arrows in $\mathcal{J}$ in the evident way.

Given a pair of right $\mathcal{J}$-maps $(f,\theta)$ and $(f^{\prime},\theta^{\prime})$, a right $\mathcal{J}$-map morphism consists of a square $(\alpha,\beta)\colon f\rightarrow f^{\prime}$ such that for every $i\in\mathcal{J}$, the triangle created by the corresponding choices of diagonal fillers commute. Given a category of arrows $u\colon\mathcal{J}\rightarrow\mathbb{C}^{\rightarrow}$, we define the category $\mathcal{J}^{\boxslash}$ consisting of right $\mathcal{J}$-maps $(f,\theta)$ together with the corresponding morphisms. There is a functor $u^{\boxslash}\colon\mathcal{J}^{\boxslash}\rightarrow\mathbb{C}^{\rightarrow}$ forgetting the lifting structure. It can be shown that this operation defines a contravariant functor denoted by $(-)^{\boxslash}$. In a completely analogous manner, we can define the concepts of left $\mathcal{J}$-map and left $\mathcal{J}$-map morphism, and obtain a dual functor ${}^{\boxslash}\!(-)$. This data constitutes the orthogonality adjunction, which generalises the classical Galois connection between orthogonal classes of maps:

[TABLE]

The next proposition [5, Lemma 1] relates awfs and orthogonal categories of arrows.

Proposition 2.3**.**

Let $(L,R)$ be an awfs on $\mathbb{C}$. Then, there are lifting functors over $\mathbb{C}^{\rightarrow}$ as shown in the following commutative diagram:

[TABLE]

All functors are full and faithful and the diagonal one is an isomorphism. There is also a functor (\text{{L-Map}})^{\boxslash}\rightarrow\text{{R-Map}}, which is not an equivalence in general. ∎

We say that an awfs $(L,R)$ is algebraically-free on a category of arrows $\mathcal{J}$ if there is a functor \eta\colon\mathcal{J}\rightarrow\text{{L-Coalg}} over $\mathbb{C}^{\rightarrow}$, such that the composition

[TABLE]

is an isomorphism of categories, cf. [15, Theorem 4.4]. The following result regarding algebraically-free awfs is implicit in the literature (cf. [14, Theorem 6.9] for example).

Proposition 2.4**.**

If $(L,R)$ is algebraically-free on some category of arrows $\mathcal{J}$, then there are functors back-and-forth \text{{R-Map}}\leftrightarrow\text{{R-Alg}} over $\mathbb{C}^{\rightarrow}$. ∎

This proposition shows that when working with an algebraically-free awfs $(L,R)$ (as will be the case in Section 5), any construction made using $R$-maps can be functorially transported to a construction using $R$-algebras, and viceversa.

3. Type-theoretic awfs’s

In this section we introduce the notion of a type-theoretic awfs. We then show how a type-theoretic awfs induces a comprehension category structure equipped with pseudo-stable choices of $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types. We begin by making the connection between awfs and comprehension categories.

Lemma 3.1**.**

Let $(L,R)$ be an awfs over $\mathbb{C}$. The functor \text{{R-Map}}\rightarrow\mathbb{C} mapping an $R$-map $(f,s)$ to $cod(f)$ is a Grothendieck fibration. Moreover, the Cartesian arrows are the morphisms of $R$-maps whose underlying square is a pullback square. ∎

Proposition 3.2**.**

Let $(L,R)$ be an awfs on a category $\mathbb{C}$. Then there is a comprehension category

[TABLE]

where $U$ is the evident forgetful functor. ∎

Results analogous to Lemma 3.1 and Proposition 3.2 hold for also for $R$-Alg. Next, we study additional logical structure on the comprehension category induced by an awfs.

Proposition 3.3**.**

Let $(L,R)$ be an awfs on $\mathbb{C}$. Then the comprehension category induced by $(L,R)$ is equipped with a pseudo-stable choice of $\Sigma$-types.

Proof.

Let $(f,s)\colon X\to\Gamma$ and $(g,t)\colon Y\to X$ be in $R$-Map. The pullback functor along $f\colon X\to\Gamma$ has a left adjoint $\Sigma_{f}\colon\mathbb{C}/X\rightarrow\mathbb{C}/\Gamma$, which is given by composition. By Remark 2.2, this functor lifts to slices of $R$-Map, as follows

[TABLE]

For the formation rule, we define $\Sigma_{f}g\colon=\Sigma_{f}(g)=f\circ g\colon Y\to\Gamma$. For the introduction rule, we define $pair_{f,g}\colon Y\rightarrow Y$ over $f$,

[TABLE]

by letting $pair_{f,g}\colon=1_{Y}$. Finally, for the elimination rule, let $C$ be over $\Sigma_{f}g$ and let $t$ be a section of $C$ over $pair_{f,g}$, we define $sp_{f,g}(C,t)\colon=t$. The computation rule holds trivally, thus giving rise to a choice of $\Sigma$-types. Stable functoriality and coherence of elimination terms also follow easily, the crucial observation is that vertical composition of $R$-maps plays nicely with the horizontal categorical structure (see [5, Section 2.8]). ∎

The case of $\Pi$-types requires the following property.

Definition 3.4**.**

An awfs $(L,R)$ on $\mathbb{C}$ satisfies the exponentiability property if for any $g\colon Z\rightarrow Y$, $f\colon Y\rightarrow X$ in the image of \text{{R-Map}}\rightarrow\mathbb{C}^{\rightarrow}, the exponential $\Pi_{f}g\in\mathbb{C}/X$ exists.

Clearly, any awfs in a locally Cartesian closed category satisfies the exponentiability property. We need something more than mere exponentiability, namely a way to coherently lift an exponential from $\mathbb{C}/X$ to \text{{R-Map}}/X. For this reason we recall the following notion from [14].

Definition 3.5**.**

Let $(L,R)$ be an awfs on a category $\mathbb{C}$. A functorial Frobenius structure is given by a lift of the pullback functor as shown:

[TABLE]

where $PB(f,g)$ denotes the pullback of $g$ along $f$.

Proposition 3.6**.**

Consider an awfs $(L,R)$ on $\mathbb{C}$ satisfying the exponentiability property and equipped with a functorial Frobenius structure. Then the comprehension category induced by $(L,R)$ has a pseudo-stable choice of $\Pi$-types.

Proof.

Consider $(f,s)\colon X\rightarrow\Gamma$ in $R$-Map. By the exponentiability property, we have a pushforward functor $\Pi_{f}\colon\underline{\smash[b]{\text{\rm{R}}}}/X\to\mathbb{C}/\Gamma$ (here $\underline{\smash[b]{\text{\rm{R}}}}/X$ denotes the slice category whose objects are arrows $g\colon Y\to X$ that can be equipped with an $R$-map structure) and, by [14, Proposition 6.5 and Proposition 6.7] this lifts to a functor

[TABLE]

Using the functors \text{{R-Map}}\leftrightarrow\text{{L-Map}}^{\boxslash} of Proposition 2.3 we can find a lift of $\Pi_{A}$ as follows:

[TABLE]

Consider an $R$-map $(g,t)\colon Y\to X$. For the formation rule, we apply $\Pi_{f}$ to obtain an $R$-map $\Pi_{f}g\colon Y\rightarrow\Gamma$. For the introduction rule, we define the operation $\lambda$; consider a section $t$ of $g$, this is an arrow $t\colon 1_{X}\rightarrow g$ in $\mathbb{C}/X$ and since $f^{*}(1_{\Gamma})\cong 1_{X}$ this is the same thing as an arrow $t\colon f^{*}(1_{\Gamma})\rightarrow g$. Taking the transpose yields a map $\lambda(t)\colon 1_{\Gamma}\rightarrow\Pi_{f}g$, as required. For the elimination rule we need to provide an arrow $app_{f,g}\colon f^{*}(\Pi_{f}g)\rightarrow g$. We can take $app_{f,g}$ to be the counit of the adjunction, $app_{f,g}\colon=\epsilon_{g}\colon f^{*}(\Pi_{f}g)\rightarrow g$. The computation rule follows easily from the bijection $\lambda\colon\mathbb{C}/X[1_{X},g]\to\mathbb{C}/\Gamma[1_{\Gamma},\Pi_{f}g]$.

It only remains to show the assignment $(\Gamma,f,g)\mapsto(\Pi_{f}g,\lambda,app)$ is pseudo-stable. This is a diagram-chasing argument, which relies on the fact that, for a Cartesian square of the form

[TABLE]

the Beck-Chevalley isomorphism $BC\colon\Delta_{\sigma}\Pi_{f}\rightarrow\Pi_{f^{\prime}}\Delta_{\tau}$ (where we write $\Delta_{\sigma}$ and $\Delta_{\tau}$ for the pullback functors along $\sigma$ and $\tau$, respectively) lifts to an isomorphism of $R$-maps by [14, Proposition 6.7]. We leave the details to the readers. ∎

Remark 3.7**.**

As shown above, an awfs equipped with a functorial Frobenius structure implies the existence of lifts \Sigma_{f}\colon\text{{R-Map}}/X\rightarrow\text{{R-Map}}/\Gamma and \Pi_{f}\colon\text{{R-Map}}/X\rightarrow\text{{R-Map}}/\Gamma of the composition and pushforward functor, respectively, for each $R$-map $(f,s)$. However, the underlying adjunctions need not lift to $R$-Map. Fortunately, this is not necessary for the construction of pseudo-stable choices of $\Sigma$- and $\Pi$-types since we only need the universal property at the level of the underlying category.

The case for intensional identity types is more complicated. Here the extra algebraic structure is essential, it will allow us to keep track of the necessary information needed to coherently produce the ‘elimination terms’ (i.e. the fillers $j$ of Item 3 from Definition 1.7) for the choice of $\mathsf{Id}$-types. To address this issue, recall that a functorial factorisation of the diagonal is a functor $\mathcal{P}\colon\mathbb{C}^{\rightarrow}\rightarrow\mathbb{C}^{\rightarrow}\times_{\mathbb{C}}\mathbb{C}^{\rightarrow}$ that acts on a map $f\colon X\rightarrow Y$ as

[TABLE]

such that the composition $\rho_{f}\cdot r_{f}$ equals the diagonal morphism $\delta_{f}\colon X\rightarrow X\times_{Y}X$. We say that a functorial factorisation of the diagonal is stable if the square $\rho_{(h,k)}\colon\rho_{f^{\prime}}\rightarrow\rho_{f}$ is Cartesian when $(h,k)\colon f^{\prime}\rightarrow f$ is so. We denote a (stable) functorial factorisation of the diagonal by $\mathcal{P}=\langle r,\rho\rangle$, where $r,\rho\colon\mathbb{C}^{\rightarrow}\rightarrow\mathbb{C}^{\rightarrow}$ are the induced functors from the two legs of the factorisation respectively. The following notion was first described in [3, Definition 3.3.3].

Definition 3.8**.**

Let $(L,R)$ be an awfs on $\mathbb{C}$. A stable functorial choice of path objects (or sfpo for conciseness) consists of a lift of a stable functorial factorisation of the diagonal $\mathcal{P}$ as shown in the following diagram:

[TABLE]

Proposition 3.9**.**

Let $(L,R)$ be an awfs equipped with a sfpo of the form $\mathcal{P}=\langle r,\rho\rangle$. Then $(L,R)$ is equipped with the structure of a pseudo-stable choice of $\mathsf{Id}$-types.

Proof.

We first construct a pseudo-stable choice $(\mathsf{Id}_{v.b.},r,j)$ of variable-based $\mathsf{Id}$-types (see Definition 1.7) and then apply Proposition 1.9 in order to obtain a pseudo-stable choice of $\mathsf{Id}$-types (see Definition 1.5).

The choices for $\mathsf{Id}$ and $r$ are canonically given by the stable functorial choice of path objects. These satisfy the coherence properties of Definition 1.8. Since the maps $r_{f}$ are equipped with an $L$-map structure, we have lifts against $R$-maps. Using this, we obtain a choice of canonical elimination terms (i.e. $j$-terms).

We are left to verify that this choice is coherent. For this, it is sufficient to show that given a Cartesian morphism of $R$-maps $(h,k)\colon f^{\prime}\rightarrow f$, a $R$-map $q\colon C\rightarrow PX$, if the diagram on the left of (3.1) commutes, then so does the one on the right.

[TABLE]

where $q^{*}\colon C^{*}\rightarrow PX^{\prime}$ is defined as the pullback of $q$ along $P(h,k)$. The arrows denoted by $j$ are the canonical choices of lifts. The arrow $d^{*}$ is the pullback of $d$ along $P(h,k)$, i.e. it is defined to be the unique arrow $d^{*}\colon X^{\prime}\rightarrow C^{*}$ such that:

[TABLE]

We split the problem into two. First, consider the following diagram equipped with the corresponding canonical lifts:

[TABLE]

Note that $j=P(h,k)^{*}\circ j(d^{*})$ since the Cartesian square $q^{*}\rightarrow q$ is a morphism of $R$-maps. Now consider the following lifting problem

[TABLE]

Once more, $j^{\prime}=j(d)\circ P(h,k)$ since the square $r_{f^{\prime}}\rightarrow r_{f}$ is morphism of $L$-maps. Finally, (3.2) tells us that the outer squares of the two previous diagrams are equal, implying that they have the same lift $j=j^{\prime}$. Thus, $P(h,k)^{*}\circ j(d^{*})=j(d)\circ P(h,k)$ as needed. ∎

Type-theoretic awfs’s, defined below, collect the structure that we discussed so far.

Definition 3.10**.**

Let $\mathbb{C}$ be a category. A type-theoretic awfs on $\mathbb{C}$ consists of the following data:

1. (1)

an awfs $(L,R)$ on $\mathbb{C}$ satisfying the exponentiability property, 2. (2)

a functorial Frobenius structure on $(L,R)$, 3. (3)

a stable functorial choice of path objects on $(L,R)$,

The following theorem summarises our results obtained so far in this section.

Theorem 3.11**.**

Let $(L,R)$ be an awfs on a category $\mathbb{C}$ with the structure of a type-theoretic awfs. Then the comprehension category induced by $(L,R)$ is equipped with pseudo-stable choices of $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types.

Proof.

Apply Proposition 3.3, Proposition 3.6 and Proposition 3.9. ∎

We conclude the section describing how type-theoretic awfs’s give rise to models of type theory.

Theorem 3.12**.**

Let $(L,R)$ be an awfs on a category $\mathbb{C}$ with the structure of a type-theoretic awfs. Then the right adjoint splitting of the comprehension category associated to $(L,R)$ is equipped with strictly stable choices of $\Sigma$-, $\Pi$- and $\mathsf{Id}$-types.

Proof.

Combine Theorem 1.6 and Theorem 3.11. ∎

4. Revisiting the groupoid model

The aim of this section is to provide a first example of a type-theoretic awfs by revisiting the original Hofmann-Streicher model [20] on the category of groupoids. Explicitly, we construct a type-theoretic awfs $(C_{f},F)$ on the category $\underline{\smash[b]{\text{\rm{Gpd}}}}$ of groupoids and functors.

Consider $f\colon X\rightarrow Y$ a functor between groupoids. The comma category of $f$, denoted by ${\bf\downarrow f}$, has as objects tuples $(a,b,p)$ with $a\in X$, $b\in Y$ and $p\colon b\rightarrow fa$. We have that ${\bf\downarrow f}$ is again a groupoid, and moreover the construction is functorial: ${\bf\downarrow(-)}\colon\underline{\smash[b]{\text{\rm{Gpd}}}}^{\rightarrow}\rightarrow\underline{\smash[b]{\text{\rm{Gpd}}}}$. This forms the middle part of a functorial factorisation assigning

[TABLE]

to $f\colon X\rightarrow Y$, where $C_{t}f(a)=(a,fa,1_{fa})$ and $Ff(a,b,p)=b$.

Proposition 4.1**.**

The functorial factorisation $({\bf\downarrow(-)},C_{t},F)$ is an algebraic weak factorisation system on $\underline{\smash[b]{\text{\rm{Gpd}}}}$. The $C_{t}$-maps are the strong deformation retractions, while the $F$-maps are the normal isofibrations.

Proof.

We start by examining the structures of the $C_{t}$-maps and the $F$-maps. We know that an $F$-map structure on a map $f\colon X\rightarrow Y$ corresponds to a lift $s$ as shown on the diagram on the left below:

[TABLE]

A closer analysis will show that $s$ equips $f\colon X\rightarrow Y$ with the structure of a normal isofibration. An $L$-map structure on $g\colon A\rightarrow B$, is given by a lift $\lambda$ as shown on the diagram on the right of the previous figure. The structure obtained from such a lift $\lambda$ can be decomposed as $\lambda(b)=(\lambda_{1}(b),b,\lambda_{2}(b))$ where $\lambda_{1}\colon B\rightarrow A$ corresponds to a retraction of $g$ and $\lambda_{2}\colon 1_{B}\rightarrow g\circ\lambda_{1}$ corresponds to a natural transformation constant on the image of $f$. This information corresponds to the structure of a strong deformation retraction.

We construct the corresponding structures of a comonad and a monad for $C_{t}$ and $F$ respectively. We provide a brief description and leave the details to the reader. The comultiplication $\delta_{f}\colon{\bf\downarrow f}\rightarrow{\bf\downarrow C_{t}f}$ for $C_{t}$ is defined by letting

[TABLE]

Similarly, the endofunctor $F$ has a multiplication $\mu_{f}\colon{\bf\downarrow Ff}\rightarrow{\bf\downarrow f}$ given by

[TABLE]

Remark 4.2**.**

The identification of the $F$-maps with normal isofibrations implies that the category $\underline{\smash[b]{\text{\rm{Gpd}}}}$ satisfies the exponentiability condition (see Definition 3.4) with respect to the awfs $(C_{t},F)$ since isofibrations can be exponentiated [8], even if $\underline{\smash[b]{\text{\rm{Gpd}}}}$ is not locally Cartesian closed. The $F$-algebras can be identified with split isofibrations. An extension of the theory considered here to $F$-algebras has been considered in [36].

Proposition 4.3**.**

The awfs $(C_{t},F)$ is equipped with a functorial Frobenius structure.

Proof.

We show that pulling back a $C_{t}$-map along an $F$-map is uniformly a $C_{t}$-map. Consider $(g,\lambda)\colon A\rightarrow Y$ a $C_{t}$-map and $(f,s)\colon X\rightarrow Y$ an $F$-map. Let $g^{\prime}\colon A\times_{Y}X\rightarrow X$ be the pullback of $g$ along $f$. We define a $C_{t}$-map structure $\lambda^{\prime}$ on $g^{\prime}$ which, by Proposition 4.1, corresponds to a strong deformation retraction $(g^{\prime},\lambda_{1}^{\prime},\lambda_{2}^{\prime})$. Using that $f$ corresponds to a normal isofibration, we can find for each point $x\in X$, a point $x^{\prime}\in X$ and a lift $\lambda_{2}^{\prime}(x)$ of $\lambda_{2}(fx)$, as in

[TABLE]

We define $\lambda_{1}^{\prime}(x)=(\lambda_{1}(fx),x^{\prime})$, the homotopy $\lambda_{2}^{\prime}\colon 1\rightarrow g^{\prime}\circ\lambda_{1}^{\prime}$ is defined using the top arrow in the previous diagram. ∎

We turn our attention to identity types. The category $\underline{\smash[b]{\text{\rm{Gpd}}}}$ has a stable and functorial factorisation of the diagonal given on a map $f\colon X\rightarrow Y$ by:

[TABLE]

where the objects of $Pf$ are tuples $(a,a^{\prime},p)$ such that $p\colon a\rightarrow a^{\prime}$ is a morphism in $X$ over the identity, i.e. $fa=fa^{\prime}$ and $fp=1_{fa}$. The map $r_{f}$ is given by $a\mapsto(a,a,1_{a})$ and the map $\rho_{f}$ is given by $(a,b,p)\mapsto(a,b)$.

Proposition 4.4**.**

The awfs $(C_{t},F)$ is equipped with a stable and functorial choice of path objects.

Proof.

For an $F$-map $(f,s)\colon X\rightarrow Y$, we need to uniformly provide a $C_{t}$-map structure to $r_{f}$ and an $F$-map structure to $\rho_{f}$. Let us define $\lambda_{1}:=t_{f}\colon Pf\rightarrow X$ the canonical target map. We define the natural transformation $\lambda_{2}\colon 1_{Pf}\rightarrow r_{f}\circ t_{f}$ by

[TABLE]

This corresponds to a strong deformation retraction structure on $r_{f}$. An $F$-map structure on $\rho_{f}$ corresponds to a normal isofibration. Consider $(\alpha,\beta)\colon(b,b^{\prime})\rightarrow(a,a^{\prime})$ in $X\times_{Y}X$ and an object $(a,a^{\prime},p)\in Pf$ over $(a,a^{\prime})$. We find the lift $(\alpha,\beta)\colon(b,b^{\prime},q)\rightarrow(a,a^{\prime},p)$ by setting $q:=\beta\circ p\circ\alpha^{-1}\colon b\rightarrow b^{\prime}$. ∎

Theorem 4.5**.**

The awfs $(C_{t},F)$ on the category $\underline{\smash[b]{\text{\rm{Gpd}}}}$ is equipped with the structure of a type-theoretic awfs.

Proof.

Apply Proposition 4.1, Proposition 4.3 and Proposition 4.4. ∎

By Theorem 3.12 and Theorem 4.5 we obtain a version of the groupoid model of [20], using normal isofibrations instead of split fibrations and presented in terms of a split comprehension category rather than of a category with families [10]. In our presentation, the connection to the homotopy theory of groupoids is made explicit thanks to the notion of a type-theoretic awfs.

5. Type-theoretic awfs from uniform fibrations

In this section we investigate how to obtain type-theoretic awfs using the theory of uniform fibrations of [14]. This provides a major source of examples of categories equipped with type-theoretic awfs, including some on simplicial and cubical sets.

We begin by recalling the pushout-product construction [31]. Let us consider a Grothendieck topos $\mathbb{E}$, the pushout-product bifunctor $-\hat{\times}-\colon\mathbb{E}^{\rightarrow}\times\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ is defined on a pair of arrows $f\colon X\rightarrow Y$ and $g\colon A\rightarrow B$ as the dotted arrow in

[TABLE]

An interval object in $\mathbb{E}$ consists a object $I$ together with two morphisms $\delta^{0},\delta^{1}\colon\bot\rightarrow I$ (where we write $\bot$ for the terminal object of $\mathbb{E}$), respectively called the left and right endpoint inclusions; these morphisms are required to be disjoint, i.e. the pullback of one along the other matches the initial object. We require the following additional structure. The connection operations on $I$ are given by $c^{k}\colon I\times I\rightarrow I$ for $k\in\{0,1\}$, making the following diagrams commute:

[TABLE]

Connections correspond to special type of degeneracy maps that can be pictured as the two possible deformations of the square $I\times I$ into its diagonal by fixing one of the two endpoints. With this in place, we proceed to describe the construction of uniform fibrations. Our starting point is the following definition.

Definition 5.1**.**

A suitable topos consists of a tuple $(\mathbb{E},I,\mathcal{M})$ where $\mathbb{E}$ is a Grothendieck topos equipped with an interval object $I$ with connections and a class $\mathcal{M}$ of arrows in $\mathbb{E}$ satisfying the following conditions:

• (M1)

the objects of $\mathcal{M}$ are monomorphisms,

• (M2)

the inital map $\emptyset\rightarrow X$ is in $\mathcal{M}$ for every $X\in\mathbb{E}$,

• (M3)

the objects of $\mathcal{M}$ are closed under pullback along any arrow in $\mathbb{E}$,

• (M4)

the elements of $\mathcal{M}$ are closed under pushout-product with the endpoint inclusions, i.e. for each $j\in\mathcal{M}$, we have that $\delta^{k}\hat{\times}j\in\mathcal{M}$.

The elements of $\mathcal{M}$ are called generating monomorphisms.

Given a suitable topos $(\mathbb{E},I,\mathcal{M})$, we can consider $\mathcal{M}$ as a category by taking Cartesian squares as arrows. Now, let us denote by $\mathcal{M}_{\hat{\times}}$ the category that has as objects maps of the form $\delta^{k}\hat{\times}j$ with $j\in\mathcal{M}$ and $k\in\{0,1\}$ and whose morphisms are given by squares of the form $\delta^{k}\hat{\times}\sigma\colon(\delta^{k}\hat{\times}j^{\prime})\rightarrow(\delta^{k}\hat{\times}j)$ induced by functoriality of the pushout-product applied to Cartesian squares $\sigma\colon j^{\prime}\rightarrow j$ between generating monomorphisms. We consider $\mathcal{M}_{\hat{\times}}$ to be a category of arrows by taking the inclusion into $\mathbb{E}^{\rightarrow}$.

Construction 5.2**.**

Let us consider a suitable topos $(\mathbb{E},I,\mathcal{M})$. The category of arrows of trivial uniform fibrations, denoted by

[TABLE]

is defined as the right orthogonal category of arrow to $\mathcal{M}$, that is, $\underline{\smash[b]{\text{\rm{TrivUniFib}}}}\colon=\mathcal{M}^{\boxslash}$. Analogously, the category of arrows of uniform fibrations, denoted by

[TABLE]

is defined as the right orthogonal category of arrow to $\mathcal{M}_{\hat{\times}}$, i.e. $\underline{\smash[b]{\text{\rm{UniFib}}}}\colon=\mathcal{M}_{\hat{\times}}^{\boxslash}$.

We construct awfs’s of trivial uniform fibrations and uniform fibrations, even if we cannot apply Garner’s small object argument directly because $\mathcal{M}$ need not be small.

Lemma 5.3**.**

Consider a suitable topos $(\mathbb{E},I,\mathcal{M})$ with a fixed dense small subcategory $\mathbb{A}$. Let us denote by $\mathcal{I}$ the full subcategory of $\mathcal{M}$ spanned by those arrows in $\mathcal{M}$ whose codomain lie in $\mathbb{A}$. Similarly, denote by $\mathcal{I}_{\hat{\times}}$ the full subcategory of $\mathcal{M}_{\hat{\times}}$ whose objects are pushout-product maps $\delta^{k}\hat{\times}j$ with $j\in\mathcal{I}$. Then the following are satisfied:

1. (1)

The right orthogonal functor of the inclusion $\mathsf{inc}\colon\mathcal{I}\hookrightarrow\mathcal{M}$ is an isomorphism i.e. $\mathsf{inc}^{\boxslash}\colon\mathcal{M}^{\boxslash}\cong\mathcal{I}^{\boxslash}$. 2. (2)

The right orthogonal functor of the inclusion $\mathsf{inc}_{\hat{\times}}\colon\mathcal{I}_{\hat{\times}}\hookrightarrow\mathcal{M}_{\hat{\times}}$ is an isomorphism i.e. $\mathsf{inc}_{\hat{\times}}^{\boxslash}\colon\mathcal{M}_{\hat{\times}}^{\boxslash}\cong\mathcal{I}_{\hat{\times}}^{\boxslash}$.

Proof.

We start with $(1)$. In order to define an inverse $\mathcal{I}^{\boxslash}\to\mathcal{M}^{\boxslash}$, consider an object $(f,\theta)\in\mathcal{I}^{\boxslash}$, where $\theta$ is a lifting operation for squares $(a,b)\colon i\to f$ with $i\in\mathcal{I}$. We need a way to canonically extend $\theta$ to all arrows in $\mathcal{M}$. In order to do this, let us consider $j\colon A\to B$ in $\mathcal{M}$. Since $\mathbb{A}$ is dense, we can express $B$ canonically as a colimit $B\cong\mathsf{colim}_{k\colon\mathscr{A}\to B}\mathscr{A}$ with $\mathscr{A}\in\mathbb{A}$. Moreover, in a topos, pullbacks commute with colimits, and thus we obtain

[TABLE]

where $\Delta_{k}j$ is the pullback of $j\colon A\to B$ along $k\colon\mathscr{A}\to B$. Since $\mathcal{M}$ is closed under base change, $\Delta_{k}j\in\mathcal{M}$ and by definition, we get $\Delta_{k}j\in\mathcal{I}$. A filler for a square $(a,b)\colon j\to f$ is canonically obtained from the universal property of the colimit, applied to the collections of fillers given by $\theta$ relative to $\Delta_{k}j$ for each $k\colon\mathscr{A}\to B$.

For $(2)$, we proceed in a similar manner. Consider $(f,\theta)\in\mathcal{I}_{\hat{\times}}^{\boxslash}$, we need to canonically extend $\theta$ to all arrows in $\mathcal{M}_{\hat{\times}}$. For this, consider $\delta^{k}\hat{\times}j\in\mathcal{M}_{\hat{\times}}$. By definition, $j\in\mathcal{M}$ and thus $j\cong\mathsf{colim}_{k\colon\mathscr{A}\to B}(k^{*}j)$ by the previous argument. Since $\delta^{k}\hat{\times}-$ is cocontinuous, we obtain:

[TABLE]

and by definition $\delta^{k}\hat{\times}(\Delta_{k})\in\mathcal{I}_{\hat{\times}}$. Once more, any square $(a,b)\colon\delta^{k}\hat{\times}j\to f$ can be filled canonically by the universal property of the colimit applied to the collections of fillers given by $\theta$ relative to $\delta^{k}\hat{\times}(\Delta_{k}j)$. ∎

Proposition 5.4**.**

Consider a suitable topos $(\mathbb{E},I,\mathcal{M})$. There exists two awfs $(C,F_{t})$ and $(C_{t},F)$ on $\mathbb{E}$ which are algebraically-free on $\mathcal{M}$ and on $\mathcal{M}_{\hat{\times}}$ respectively.

Proof.

Apply Garner’s small object argument to $\mathcal{I}$ and $\mathcal{I}_{\hat{\times}}$ respectively. Since $\mathbb{E}$ is a Grothendieck topos, there exists a small dense subcategory $\mathbb{A}$ of $\mathbb{E}$ (for example, the full subcategory of compact objects for a large enough cardinal). By Lemma 5.3, the resulting awfs’s are algebraically-free on $\mathcal{M}$ and $\mathcal{M}_{\hat{\times}}$ respectively. ∎

Remark 5.5**.**

By definition of algebraically-free awfs we have the following isomorfisms \text{{F_{t}-Alg}}\cong\underline{\smash[b]{\text{\rm{TrivUniFib}}}} and \text{{F-Alg}}\cong\underline{\smash[b]{\text{\rm{UniFib}}}}. And, by Proposition 2.4 we have back-and-forth functors \text{{F_{t}-Map}}\leftrightarrow\underline{\smash[b]{\text{\rm{TrivUniFib}}}} and \text{{F-Map}}\leftrightarrow\underline{\smash[b]{\text{\rm{UniFib}}}}.

We proceed to show that, under some extra hypothesis, the awfs $(C,F_{t})$ of uniform fibrations is type-theoretic. We know that it has a functorial Frobenius structure by [14, Theorem 8.8] and so we only need to construct a stable functorial choice of path objects on $(C_{t},F)$. For this, we require the following construction. Given a topos $\mathbb{E}$ equipped with an interval object $I$, there is a natural way to construct a stable and functorial factorisation of the diagonal: for a morphism $f\colon B\rightarrow A$, consider

[TABLE]

where the object $Pf$ and the map $r_{f}$ arise from the pullback diagram:

[TABLE]

Here, we use the abbreviation of $(-)^{I}$ for the exponential object $\hom(I,-)$ and denote by $\epsilon\colon I\rightarrow\bot$ the unique map to the terminal object. The second leg of the factorisation $\rho_{f}\colon Pf\rightarrow B\times_{A}B$ is given by the universal property of $B\times_{A}B$ applied to the canonical source and target maps $s_{f},t_{f}\colon Pf\rightarrow B$ given by the composition of the arrow $Pf\rightarrow B^{I}$ from the pullback square, and $B^{\delta^{0}},B^{\delta^{1}}\colon B^{I}\rightarrow B$ respectively. We denote the factorisation by $\mathcal{P}_{I}$, so as to indicate that it was constructed from the interval $I$.

Let us provide an alternative construction of this factorisation which makes evident some intermediate steps and uses the adjunction $-\hat{\times}i\vdash\hat{\hom}(i,-)$ given by the pushout-product and pullback-exponential. Denote by $i\colon\partial I\rightarrow I$ the boundary inclusion of the interval object and by $\iota^{k}\colon\bot\rightarrow\partial I$ the composition of the boundary with the $k$-th endpoint inclusion. The following diagram expands the previous one, i.e. the exterior part is exactly the one in (5.1).

[TABLE]

The intermediate horizontal arrows $\lambda_{f}$, $\alpha_{f}$ and $\beta_{f}$ are given intuitively as follows. The map $\lambda_{f}$ sends a pair of points in $B\times_{A}B$ to the same pair of points but now in $B^{\partial I}$, $\alpha_{f}$ sends a similar pair of points $(b_{1},b_{2})$ to the reflexivity (constant) path on $f(b_{1})=f(b_{2})$, and map $\beta_{f}$ also sends a point $b$ to the reflexivity path on $f(b)$.

The next essential ingredient needed to prove that the factorisation $\mathcal{P}_{I}=\langle r,\rho\rangle$ lifts to a stable functorial choice of path objects, is that of the categories of strong homotopy equivalences and of strong deformation retracts. We recall from [14, Definition 4.1] the definition of $k$-oriented strong homotopy equivalence (for $k\in\{0,1\}$) and from [14, Lemma 8.1] that they assemble into a category of arrows which we will call $\underline{\smash[b]{\text{\rm{SE}}}}_{k}$, we denote $\underline{\smash[b]{\text{\rm{SE}}}}\colon=\underline{\smash[b]{\text{\rm{SE}}}}_{0}+\underline{\smash[b]{\text{\rm{SE}}}}_{1}$. The definition of k-oriented strong deformation retracts is analogous; briefly, a k-oriented strong deformation retraction structure corresponds to a tuple $(g\colon A\rightarrow B,r\colon B\rightarrow A,h\colon I\times B\rightarrow B)$ such that $rg=1_{A}$, $h$ is an homotopy from $gr$ to $1_{B}$ or from $1_{B}$ to $gr$ respectively if $k$ is [math] or $1$ and such that $h$ is degenerate in the image of $g$ (hence the strength). Strong deformation retracts assemble into categories of arrows $\underline{\smash[b]{\text{\rm{SDR}}}}_{k}$ depending on the orientation $k\in\{0,1\}$, and so we obtain $\underline{\smash[b]{\text{\rm{SDR}}}}\colon=\underline{\smash[b]{\text{\rm{SDR}}}}_{0}+\underline{\smash[b]{\text{\rm{SDR}}}}_{1}$ by taking their coproduct. Notice that any strong deformation retract is also a strong homotopy equivalence, i.e. there is a functor of category of arrows $\underline{\smash[b]{\text{\rm{SDR}}}}\rightarrow\underline{\smash[b]{\text{\rm{SE}}}}$ over the identity of the underlying category.

The following two lemmas constitute the first key results regarding the connection between the factorisation $\mathcal{P}_{I}=\langle r,\rho\rangle$ and the awfs of uniform fibrations.

Lemma 5.6**.**

Consider a suitable topos $(\mathbb{E},I,\mathcal{M})$ and let $(C_{t},F)$ be a corresponding awfs of uniform fibrations on $\mathbb{E}$. Suppose that the following additional hypothesis holds:

1. (M5)

Maps in $\mathcal{M}$ are closed under pushout-product against the boundary inclusion $i\colon\partial I\rightarrow I$, i.e. for any $j\in\mathcal{M}$, we have that $i\hat{\times}j\in\mathcal{M}$.

Then, the second component of the factorisation $\mathcal{P}_{I}$, i.e $\rho\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$, lifts to a functor \rho\colon\text{{F-Map}}\rightarrow\text{{F-Map}}.

Proof.

Since the awfs of trivial uniform fibrations $(C,F_{t})$ is suitable (see [14, Definition 7.1]), the functor $\delta^{k}\hat{\times}-$ lifts to the category $C$-Map and $\delta^{k}\hat{\times}-$ also factors though the category SE of strong homotopy equivalences by [14, Lemma 8.4]. Combining these two facts, we obtain a lift

[TABLE]

By [14, Proposition 8.5], we have a functor \text{{C-Map}}\times_{\mathbb{E}^{\rightarrow}}\underline{\smash[b]{\text{\rm{SE}}}}\rightarrow\text{{C_{t}-Map}} over $\mathbb{E}^{\rightarrow}$, composing with the one above, we obtain a lift of $\delta^{k}\hat{\times}-$

[TABLE]

By functorial orthogonality arguments with respect to the pushout-product and pullback-exponential constructions (see [14, Proposition 5.11] and [14, Remark 5.12]) together with the hypothesis (M5), the functor $i\hat{\times}-\colon\mathcal{M}\rightarrow\mathcal{M}$ lifts to the category $C$-Map,

[TABLE]

Applying the lifts in (5.3) and (5.4), together with the fact that $(C,F_{t})$ is algebraically-free on the category of arrows $\mathcal{M}\rightarrow\mathbb{E}^{\rightarrow}$, as witnessed by the functor \eta\colon\mathcal{M}\rightarrow\text{{C-Coalg}}, we obtain the diagram

[TABLE]

where $\tilde{\eta}$ is the composite of $\eta$ and the forgetful functor from $C$-algebras to $C$-maps.

By symmetry of the pushout-product functor, we obtain a natural isomorphism between $i\hat{\times}\delta^{k}\hat{\times}-$ and $\delta^{k}\hat{\times}i\hat{\times}-$. We can transfer the algebraic structure along this natural isomorphism in order to obtain the following lift:

[TABLE]

Taking the coproduct of these lifts for $k=0,1$ we obtain a lift of $i\hat{\times}-$, .

[TABLE]

Using that \text{{C_{t}-Map}}\cong{{}^{\boxslash}}\text{{F-Alg}} (cf. Proposition 2.3) and that $(C_{t},F)$ is algebraically-free on $\mathcal{M}_{\hat{\times}}$, we can apply [14, Proposition 5.9] to (5.5) and obtain

[TABLE]

By the top pullback square in (5.2), the morphism $\rho_{f}\colon Pf\rightarrow B\times_{A}B$ is obtained in the following two steps:

[TABLE]

i.e. by first applying $\hat{\hom}(i,-)$ and then pulling back along $\langle\alpha_{f},\lambda_{f}\rangle$. Since we have lifts of $\hat{\hom}(i,-)$ and of the pullback functor to the category of $F$-algebras, we obtain a lift of $\rho$,

[TABLE]

Finally, as we are working with an algebraically-free awfs, we have lifts back-and-forth between $R$-Alg and $R$-Map over $\mathbb{E}^{\rightarrow}$ (cf. Proposition 2.4), and thus we can transfer the lift of $\rho$ from the category of $R$-algebras to that of $R$-maps. ∎

Lemma 5.7**.**

Consider a suitable topos $(\mathbb{E},I,\mathcal{M})$ and let $(C_{t},F)$ be a corresponding awfs of uniform fibrations on $\mathbb{E}$. Then the first component $r\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ of the factorisation $\mathcal{P}_{I}$ lifts to the category of strong deformation retracts,

[TABLE]

Proof.

We first show that the target map functor (that takes a map $f\colon B\rightarrow A$ to a map $t_{f}\colon Pf\rightarrow B$) lifts to a functor from $F$-Map to $F_{t}$-Map. Using that we have a lift \delta^{1}\hat{\times}-\colon\text{{C-Map}}\rightarrow\text{{C_{t}-Map}} as shown in the proof of Lemma 5.6, we can transpose using [14, Proposition 5.9] to obtain a lift of $\hat{\hom}(\delta^{1},-)$:

[TABLE]

Looking at (5.2), note that $t_{f}\colon Pf\rightarrow B$ is obtained by applying $\hat{\hom}(\delta^{1},-)$ to $f$ and then pulling back along $\langle\beta_{f},1_{B}\rangle$. Thus, the functor mapping $f\mapsto t_{f}$ lifts as

[TABLE]

Since both awfs in question are algebraically-free, we can apply Proposition 2.4 to obtain the desired lift.

Let us return to the task of finding a lift of the functor $r\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ to a functor r\colon\text{{F-Map}}\rightarrow\underline{\smash[b]{\text{\rm{SDR}}}}. For this, we show that for each uniform fibration $(f,s)\colon B\rightarrow A$ the target map $t_{f}\colon Pf\rightarrow B$ is a strong homotopy retraction of $r_{f}\colon B\rightarrow Pf$.

Looking again at (5.2) it is clear that $t_{f}\circ r_{f}=1_{B}$. Thus, we are left with the task of constructing an homotopy $H\colon r_{f}\circ t_{f}\sim 1_{Pf}$, for this consider the commutative diagram

[TABLE]

where the top horizontal arrow is given by the universal property of $Pf^{\partial I}\cong Pf\times Pf$. This gives us an arrow into the pullback

[TABLE]

We already have a lift of the target map t_{(-)}\colon\text{{F-Map}}\rightarrow\text{{F_{t}-Map}}. Combining this with the fact that $\hat{\hom}(i,-)$ lifts to $F_{t}$-Map (which follows by similar arguments to those used in the proof of Lemma 5.6), $\hat{\hom}(i,t_{(-)})$ lifts to a functor

[TABLE]

which we can apply to $f$ to obtain a uniform trivial fibration $\hat{\hom}(i,t_{f})$.

By part (M2) of Definition 5.1, for every object $X\in\mathbb{E}$, the map $\emptyset\rightarrow X$ is in $\mathcal{M}$. Using this, we obtain a morphism $H$ as the canonical filler in

[TABLE]

It is straightforward to verify that this $H$ is actually an homotopy from $r_{f}\circ t_{f}$ to $1_{Pf}$. This shows that $t_{f}$ is a strong deformation retract of $r_{f}$.

We have given the action of the desired lift r\colon\text{{F-Map}}\rightarrow\underline{\smash[b]{\text{\rm{SDR}}}} on objects . To show that this construction is functorial on $f$, consider a morphism of $F$-Map $(h,k)\colon f^{\prime}\rightarrow f$. Since the factorisation of the diagonal is functorial, we obtain the diagram

[TABLE]

The bottom square is a morphism of $F_{t}$-Map since it is the result of applying the lift of $t_{(-)}$ of (5.6) to the square $(h,k)$. Let us prove that $(h,P(h,k))\colon r_{f^{\prime}}\rightarrow r_{f}$ is a morphism of strong deformation retracts. Looking at the definition of a morphism of homotopy equivalences (in the paragraph before [14, Lemma 8.1]), we observe that the only thing we need to show is that the following diagram commutes:

[TABLE]

where the left and right horizontal arrows are the homotopies witnessing that $r_{f^{\prime}}$ and $r_{f}$ respectively are strong deformation retracts. For this, we make use of the naturality of the filling operations. Consider the diagrams:

[TABLE]

[TABLE]

The left square in (5.7) is a morphism in $\mathcal{M}$ since it is Cartesian. The right square of (5.8) is a morphism of $F_{t}$-maps since it is the result of applying the lift \hat{\hom}(i,t_{(-)})\colon\text{{F-Map}}\rightarrow\text{{F_{t}-Map}} to the square $(h,k)$ which is, by hypothesis, a morphism of $F$-maps. Hence, the corresponding lifts cohere.

Since the construction of the maps $\tilde{H}$ and $\tilde{H}^{\prime}$ is given by a universal property, it is functorial and so the diagram

[TABLE]

commutes. Thus, the composition of the bottom horizontal arrows in (5.7) and (5.8) coincide. This makes the filler $L^{\prime}$ and $L$ in diagrams 5.7 and 5.8 respectively, the same morphism and thus $H\circ P(h,k)=L^{\prime}=L=P(h,k)^{I}\circ H^{\prime}$, as required. ∎

Using Lemma 5.6 and Lemma 5.7, we can prove the following proposition.

Proposition 5.8**.**

Consider a suitable topos $(\mathbb{E},I,\mathcal{M})$ and let $(C_{t},F)$ be a corresponding awfs of uniform fibrations on $\mathbb{E}$. Suppose that the following additional hypotheses hold:

1. (M5)

Maps in $\mathcal{M}$ are closed under pushout-product against the boundary inclusion $i\colon\partial I\rightarrow I$, i.e. for any $j\in\mathcal{M}$, we have that $i\hat{\times}j\in\mathcal{M}$. 2. (M6)

For any $f\colon B\rightarrow A$ in $\mathbb{E}$, the first leg map $r_{f}\colon B\rightarrow Pf$ from the factorisation of the diagonal $\mathcal{P}_{I}$ belongs to $\mathcal{M}$:

Then, the factorisation of diagonal $\mathcal{P}_{I}=\langle r,\rho\rangle$ induced from the interval object, lifts to a stable functorial choice of path objects for $(C_{t},F)$:

[TABLE]

Proof.

Recall that the factorisation of the diagonal $\mathcal{P}_{I}=\langle r,\rho\rangle$ is divided into two functors $r,\rho\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$. By Lemma 5.6, $\rho$ lifts to the category $F$-Map, so it remains to show that $r\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ lifts to a functor r\colon\text{{F-Map}}\rightarrow\text{{C_{t}-Map}}. This follows from two observations. First, since the factorisation of the diagonal is stable, $r$ preserves Cartesian squares and thus, by item (M6) in the hypothesis of the theorem, $r$ lifts to $\mathcal{M}$ (considered as a category of arrows), $r\colon\mathbb{E}^{\rightarrow}\to\mathcal{M}$. Secondly, consider the unit $\eta_{\mathcal{M}}\colon\mathcal{M}\rightarrow{{}^{\boxslash}}(\mathcal{M}^{\boxslash})$ of the orthogonality adjunction of 2.1 and note that since $(C,F_{t})$ is algebraically-free on $\mathcal{M}$, we obtain a morphism in the slice over $\mathbb{E}^{\rightarrow}$,

[TABLE]

We can compose these last two lifts to obtain r\colon\mathbb{E}^{\rightarrow}\rightarrow\text{{C-Map}}.

Finally, we can combine the lifts r\colon\text{{F-Map}}\rightarrow\underline{\smash[b]{\text{\rm{SDR}}}} from Lemma 5.7 with r\colon\mathbb{E}^{\rightarrow}\rightarrow\text{{C-Map}} and apply [14, Proposition 8.5] in order to obtain the desired lift of $r$,

[TABLE]

We introduce the following definition to summarise our results.

Definition 5.9**.**

A type-theoretic suitable topos consists of a suitable topos $(\mathbb{E},I,\mathcal{M})$ (see Definition 5.1) which moreover satisfy the conditions (M5) and (M6) in the hypothesis of Proposition 5.8.

Theorem 5.10**.**

Let $(\mathbb{E},I,\mathcal{M})$ be a type-theoretic suitable topos, and let $(C_{t},F)$ be the awfs of uniform fibrations on $\mathbb{E}$. Then $(C_{t},F)$ is equipped with the structure of a type-theoretic awfs.

Proof.

The result follows from [14, Theorem 8.8] and Proposition 5.8. ∎

The next result allows us to construct examples of type-theoretic suitable topos.

Proposition 5.11**.**

Consider $\mathbb{E}$ be a Grothendieck topos equipped with an interval object $I$ with connections. Let $\mathcal{M}_{all}$ be the class that consists of all monomophisms of $\mathbb{E}$. Then the tuple $(\mathbb{E},I,\mathcal{M}_{all})$ is a type-theoretic suitable topos.

Proof.

We need to verify conditions (M1)-(M6) from the definition of type-theoretic suitable topos. By elementary properties of monomorphisms, it is clear that (M1)-(M3) hold. Condition (M4) follows because in the topos $\mathbb{E}$ the pushout-product construction $\delta^{k}\hat{\times}j$ for a given monomorphism $j\colon A\rightarrow B$, computes the join (or union) of the subobjects $\delta^{k}\times B\colon B\rightarrow I\times B$ and $I\times j\colon I\times A\rightarrow I\times B$, which is again a subobject of $I\times B$ and in particular a monomorphism. The same arguments applies for condition (M5). Finally condition (M6) follows since for any map $f\colon X\rightarrow Y$, the morphism $r_{f}\colon X\rightarrow Pf$ is the section of the target map $t_{f}\colon Pf\rightarrow X$ and in particular, it is a monomorphism. ∎

Example 5.12**.**

We can instantiate Proposition 5.11 on the presheaf toposes of simplicial sets $\underline{\smash[b]{\text{\rm{sSet}}}}$ and of cubical sets $\underline{\smash[b]{\text{\rm{cSet}}}}$ equipped with the obvious choices of interval objects given by the representable $1$-simplex and $1$-cube respectively. We thus obtain type-theoretic awfs on $\underline{\smash[b]{\text{\rm{sSet}}}}$ and $\underline{\smash[b]{\text{\rm{cSet}}}}$. In $\underline{\smash[b]{\text{\rm{sSet}}}}$, assuming classical logic, a morphism admits the structure of a uniform fibration if and only if it is a Kan fibration by [14, Theorem 9.9].

Remark 5.13**.**

Although the proof of Theorem 5.10 is constructive, in order to construct a univalent universe à la Hofmann-Streicher [19] in a constructive setting, it is necessary to restrict the category $\mathcal{M}_{all}$ of generating monomorphisms to that of decidable ones; i.e. those mononomorphism that have level-wise decidable image[28]. The arguments in this section do not apply if we take $\mathcal{M}_{dec}$ as the category of generating monomorphisms, where $\mathcal{M}_{dec}$ is the subclass of $\mathcal{M}_{all}$ of decidable monomorphisms (for either $\underline{\smash[b]{\text{\rm{sSet}}}}$ or $\underline{\smash[b]{\text{\rm{cSet}}}}$). The issue lies in condition (M6), i.e. that the first leg $r_{f}\colon X\rightarrow Pf$ of the factorisation of the diagonal of a morphism $f\colon X\rightarrow Y$ is in $\mathcal{M}_{dec}$. Intuitively, the morphism $r_{f}$ maps an object of $x$ of $X$ to the degenerate path on $x$, this morphism is not decidable because, in general, it is not possible to decide degeneracies [4]. Because of this, in the next section we turn our attention to normal uniform fibrations (see Remark 7.2). An alternative approach would be to restrict attention to cofibrant objects, as in [12].

6. Normal uniform fibrations

In this section, we develop the notion of a normal uniform fibration in the context of a suitable topos $(\mathbb{E},I,\mathcal{M})$ (Definition 5.1). Recall from the discussion before Proposition 5.4 that the category of arrows of uniform fibrations was constructed by right orthogonality form the category of arrows $\mathcal{M}_{\hat{\times}}$ over $\mathbb{E}$, whose objects are maps of the form $\delta^{k}\hat{\times}j$ with $j\in\mathcal{M}$ and $k\in\{0,1\}$. Moreover, recall from Proposition 5.4 that we cannot use Garner’s small object argument directly with $\mathcal{M}_{\hat{\times}}$ to construct the awfs of uniform fibrations $(C_{t},F)$ as $\mathcal{M}_{\hat{\times}}$ is not small; instead, we need to restrict to the small category of arrows $\mathcal{I}_{\hat{\times}}$ that consists of arrows $\delta^{k}\hat{\times}j$ with $j\in\mathcal{I}$, where $\mathcal{I}$ consists of the arrows in $\mathcal{M}$ whose codomain lie in a fixed small dense subcategory of $\mathbb{E}$.

We define a new category of arrows $\mathcal{I}^{\bf n}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$ such that a right $\mathcal{I}^{\bf n}_{\hat{\times}}$-map will consist of a uniform fibration with an extra normality property. The idea is that $\mathcal{I}^{\bf n}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$ is obtained form $\mathcal{I}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$ by adding, for each generating monomorphism $i:A\rightarrowtail B$ and for $k\in\{0,1\}$, the coherence square on the left in

[TABLE]

where $\textbf{sq}_{k}(i)\colon B+_{A}(I\times A)\rightarrow B$ is the universal map out of the pushout as described on the right of the previous diagram. The arrows $\epsilon\times B$ and $\epsilon\times A$ are the projections from the second component of the product. We refer to the square on the left of (6.1) as the $k$-squash square of $i\colon A\rightarrowtail B$ and we denote it by

[TABLE]

The name follows the intuition of squashing the mapping cylinder in the direction of the interval (i.e. the filling direction). The following technical result about squash squares will be needed in what follows.

Lemma 6.1**.**

Let $k\in\{0,1\}$ and consider monomophisms $i\colon A\rightarrowtail B$ and $j\colon C\rightarrowtail D$. Then applying the pushout-product functor $(j\hat{\times}-)\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ to the k-squash square of $i\colon A\rightarrowtail B$, produces the k-squash square of $j\hat{\times}i$; that is:

[TABLE]

Proof.

If we apply $(j\hat{\times}-)\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ to the k-squash square of $i\colon A\rightarrowtail B$, using that the pushout-product is symmetric and associative, we get the following square:

[TABLE]

where we only need to verify that the top horizontal arrow $\Theta$ is the squash morphism, that is, we need to verify that $\Theta=\textbf{sq}_{k}(j\hat{\times}i)\colon\text{dom}(\delta^{k}\hat{\times}(j\hat{\times}i))\rightarrow D\times B$, but this follows since the diagram commutes. ∎

We now proceed to construct the arrow category $\mathcal{I}^{\bf n}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$ that will generate the category of normal uniform fibrations. We do this a follows. First let us denote by $\mathbb{I}$ the ‘walking arrow’, that is the poset with two objects $0<1$ considered as a category, this has the structure of an interval object in $\underline{\smash[b]{\text{\rm{Cat}}}}$ and we denote the inclusions by:

[TABLE]

We define $\mathcal{I}^{\bf n}_{\hat{\times}}:=\mathbb{I}\times\mathcal{I}_{\hat{\times}}$, where $\mathcal{I}_{\hat{\times}}$ is the generating category of uniform fibrations. The functor down to $\mathbb{E}^{\rightarrow}$ is determined by the following two properties.

1. (1)

The following diagram commutes:

[TABLE]

where the map $\epsilon_{cod}\colon\mathcal{I}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$ sends an object $i\in\mathcal{I}_{\hat{\times}}$ to the identity arrow on the codomain of $i$. 2. (2)

For $k\in\{0,1\}$ and for each $i\colon A\rightarrowtail\mathscr{A}$ in $\mathcal{I}$, the functor $u^{\bf n}_{\otimes}$ takes the arrow in $\mathbb{I}\times\mathcal{I}_{\hat{\times}}$ of the form $\mathbb{I}\times i\colon\{0\}\times i\rightarrow\{1\}\times i$, to the $k$-squash square of $i$; i.e. $\textbf{squash}_{k}(i)\colon\delta^{k}\hat{\times}i\rightarrow 1_{\mathscr{A}}$.

In other words, $\mathcal{I}^{\bf n}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$ is a natural transformation: $u_{\otimes}\rightarrow\epsilon_{cod}\colon\mathcal{I}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$ whose components are the $k$-squash squares.

We define $\underline{\smash[b]{\text{\rm{NrmUniFib}}}}\rightarrow\mathbb{E}^{\rightarrow}$ to be the category of arrows of right $\mathcal{I}^{\bf n}_{\hat{\times}}$-maps in $\mathbb{E}$, and we call its objects normal uniform fibrations. Using Garner’s small object argument [15, Theorem 4.4] along the lines of Lemma 5.3 and Proposition 5.4, we obtain the following result.

Theorem 6.2**.**

There is an algebraically-free awfs on the category of arrows $\mathcal{I}^{\bf n}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$, denoted by $(NC_{t},NF)$, whose category of $NF$-algebras is that of normal uniform fibrations. ∎

Let us observe that the forgetful functor into $\mathbb{E}^{\rightarrow}$ factors through the category of uniform fibrations, i.e. we have a commutative diagram:

[TABLE]

Moreover, we can prove the following lemma.

Lemma 6.3**.**

The forgetful functor $U\colon\underline{\smash[b]{\text{\rm{NrmUniFib}}}}\rightarrow\underline{\smash[b]{\text{\rm{UniFib}}}}$ is fully faithful.

Proof.

This follows intuitively by noticing that the structure of a normal uniform fibration does not add any new lifting problems to that of a uniform fibrations; this is because the only new vertical arrows we are adding are identities and every morphism has a unique lift against them. Concretely, if $(f,\phi)\in\underline{\smash[b]{\text{\rm{NrmUniFib}}}}$ and if $(f,\theta)\in\underline{\smash[b]{\text{\rm{UniFib}}}}$, then both lifting structures $\phi$ and $\theta$ produce lifts against the exactly the same squares, the difference is that $\phi$ may have additional coherence properties. ∎

In the following proposition we characterise those uniform fibration structures that are normal. We use the following terminology: we say that a morphism $\theta\colon I\times B\rightarrow X$ is degenerate in the lifting direction if it factors through the projection $\rho_{1}\colon I\times B\rightarrow B$ via some arrow $\theta^{*}\colon B\rightarrow X$; we call $\theta^{*}$ the lifting degeneracy of $b$.

Proposition 6.4**.**

Let $(f,\theta)\in\underline{\smash[b]{\text{\rm{UniFib}}}}$ then the following are equivalent:

1. (1)

$(f,\theta)$* is a normal uniform fibration.* 2. (2)

For any generating monomorphism $i\colon A\rightarrowtail\mathscr{A}$ in $\mathcal{I}$ and for any square:

[TABLE]

*if the square factors through the squash square of $i$ as * \textstyle{\delta^{k}\hat{\times}i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\textbf{squash}_{k}(i)}$$\textstyle{1_{\mathscr{A}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(a^{*},b^{*})}$$\textstyle{f} , then the lift $\theta_{i}(a,b)$ is degenerate in the lifting direction with $a^{*}$ as lifting degeneracy. 3. (3)

For any generating monomorphism $i\colon A\rightarrowtail B$ in $\mathcal{M}$ and for any square:

[TABLE]

*if the square factors through the squash square of $i$ as * \textstyle{\delta^{k}\hat{\times}i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\textbf{squash}_{k}(i)}$$\textstyle{1_{B}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(a^{*},b^{*})}$$\textstyle{f} , then the lift $\theta_{i}(a,b)$ is degenerate in the lifting direction with $a^{*}$ as lifting degeneracy.

Proof.

Let us first assume that $(f,\theta)$ is a normal uniform fibration. It is easy to see that item (2) holds, for this consider the diagram:

[TABLE]

it is clear that the lifts cohere because the left square is by definition a morphism in (the image of) $\mathcal{I}^{\bf n}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$.

It is also easy to see that (2) implies (1), this follows since the uniform fibration structure $\theta$ already provides lifts against all lifting problems coming form $\mathcal{I}^{\bf n}_{\hat{\times}}$, moreover, the lifts will also cohere with all the squares coming from $u_{\otimes}\colon\mathcal{I}_{\hat{\times}}\rightarrow\mathbb{E}^{\rightarrow}$. So we only need to verify that it coheres with the squash squares, but these squares are precisely those as in the hypothesis of item (2).

It is clear that (3) implies (2). For the converse let us first observe, using that colimits in $\mathbb{E}$ are universal, that any monomorphism $i\colon A\rightarrowtail B$, is the colimit over the generalised elements with domain on the dense subcategory $\mathbb{A}$ used to define the category of arrows $\mathcal{I}$ (see Proposition 5.4); that is,

[TABLE]

where for each $x\colon\mathscr{A}\rightarrow B$ we denote by $x^{*}(i)$ the pullback of $i$ along $x$. Now, since $\delta^{k}\hat{\times}-\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ is cocontinuous, we have that:

[TABLE]

Let us suppose that (2) holds, and that we have a diagram as in item (3). Then for each generalised element $x\colon\mathscr{A}\rightarrow B$ with $\mathscr{A}\in\mathbb{A}$, we have a square:

[TABLE]

where the left square is the colimit inclusion corresponding to $x\colon\mathscr{A}\rightarrow B$. The commutation of the respective triangle is obtained by the universal property of the colimit.

Finally, if the square on the right factors through a squash square

[TABLE]

then (by naturality) the outer square also factor through a squash square and thus the lift $\theta_{x^{*}(i)}$ is degenerate with $a^{*}\iota_{x}$ as lifting degeneracy. This implies by the uniqueness of the universal property, that also $\theta_{i}$ is degenerate with $a^{*}$ as lifting degeneracy. ∎

Remark 6.5**.**

To guide our intuition towards normal uniform fibrations, we can compare the notions of normality for cloven isofibrations in groupoids and for uniform fibrations in simplicial sets. For this, we consider the awfs of (normal) uniform fibrations on simplicial sets constructed from the suitable topos structure consisting of the $1$-simplex as the interval object and the class $\mathcal{M}_{all}$ of all monomorphisms as the class of generating monomorphisms. It is not hard to show that the following are pullback squares:

[TABLE]

Here, the categories $\underline{\smash[b]{\text{\rm{ClFib}}}}$ and $\underline{\smash[b]{\text{\rm{NrmFib}}}}$ are those of cloven isofibrations and normal cloven isofibrations in groupoids while the horizontal arrows are given by the nerve functor and its respective lifts. This shows how the notion of uniform fibration (respectively normal uniform fibration) is a generalisation to higher dimensions of the notion of cloven isofibration (respectively normal cloven isofirations).

The category of arrows of normal trivial cofibrations is defined to be the category of $NC_{t}$-maps with respect to the awfs of normal uniform fibrations Theorem 6.2. Alternatively, it is the left orthogonal category of arrows of $\underline{\smash[b]{\text{\rm{NrmUniFib}}}}$. We will denote it by $\underline{\smash[b]{\text{\rm{NrmTrivCof}}}}$. Even if we do not know a complete characterisation of normal trivial cofibrations, we have is a general method for constructing normal trivial cofibrations from a structure that is easier to handle. For this, let us recall the categories $\underline{\smash[b]{\text{\rm{SDR}}}}$ of strong deformation retractions and $\underline{\smash[b]{\text{\rm{SE}}}}$ of strong homotopy equivalences from Section 5 defined immediately before Lemma 5.6. In the next proposition, we observe that every strong deformation retract has (uniformly) the structure of a normal trivial cofibration. Normality is an essential ingredient in the proof, in particular, a similar result would not hold for uniform fibrations.

Proposition 6.6**.**

There is a functor from the category strong deformation retracts $\underline{\smash[b]{\text{\rm{SDR}}}}$ to that of normal trivial cofibrations NrmTrivCof,

[TABLE]

Proof.

Let $(g,r,h)\in\underline{\smash[b]{\text{\rm{SDR}}}}$ which we assume to be [math]-oriented (the other case being analogous). We have to define $\Psi(g,r,h):=(g,\Psi h)$ with $\Psi h$ a left $\underline{\smash[b]{\text{\rm{NrmTrivCof}}}}$-map structure for $g$. To do this, let us consider a normal uniform fibration $(f,\phi)$ and a square $(a,b)\colon g\rightarrow f$ for which we will construct a lift $\Psi h_{f}\colon B\rightarrow X$ as shown:

[TABLE]

We first consider the lift $H\colon I\times B\rightarrow X$, in the following square (which commutes because the deformation retraction is [math]-oriented), produced by the normal uniform fibration structure of $f$:

[TABLE]

We define $\Psi h_{f}\colon=H\cdot(\delta^{1}\times B)$. That is, the lift $\Psi h_{f}$ is defined to be $H$ on restricted to the top of the cylinder $I\times B$. The verification that $f\circ\Psi h_{f}=b$ is straightforward.

We now need to check that $\Psi h_{f}\cdot g=a$, for this we first observe the following diagram:

[TABLE]

here, the lift $H_{0}$ is also defined by the uniform fibration structure of $f$, and moreover the triangle created by the lifts commute, since the square on the left is a morphism of left $\underline{\smash[b]{\text{\rm{UniFib}}}}$-maps.

We use that $rg=1_{a}$ and the strength of the homotopy retraction tuple $(g,r,h)$, to replace the horizontal arrows in the previous diagram in order to obtain the following one:

[TABLE]

where the lifts cohere by Proposition 6.4 using the squash square of $\bot_{A}\colon\emptyset\rightarrow A$. With this in place,

[TABLE]

as required. ∎

7. Type-theoretic awfs from normal uniform fibrations

In order to equip the awfs $(NC_{t},NF)$ of normal uniform fibrations with the structure of a type-theoretic awfs we require a functorial Frobenius structure and a stable functorial choice of path objects. In this section, we show how to construct these. We focus first with the construction of a stable functorial choice of path objects (sfpo for short), cf. Definition 3.8. We work in the context of a suitable topos $(\mathbb{E},I,\mathcal{M})$ that in addition satisfies hypothesis (M5) from Proposition 5.8. Recall from the discussion preceding Proposition 5.8 that a suitable topos has a canonical stable and functorial factorisation of the diagonal, called $\mathcal{P}_{I}$, which is constructed via exponentiation by the interval. Our objective is to lift this factorisation to a sfpo. That is, we need to exhibit a lift of $\mathcal{P}_{I}$ as in

[TABLE]

We can split the problem in two. If we denote by $r,\rho\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ the two legs of the sfpo (i.e. by composing $\mathcal{P}_{I}$ with the two projections from the pullback), then it is sufficient to show that there are lifts of these functors as in the following diagram.

[TABLE]

The lift of $r\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ can easily obtained by collecting some of the results established so far.

Lemma 7.1**.**

There is a lift of the functor $r\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ as shown:

[TABLE]

Proof.

We construct the desired lift as the following composite:

[TABLE]

where the lift in the leftmost square is the forgetful functor, that on the middle square comes from Lemma 5.7 and the lift in the rightmost square is the one from Proposition 6.6. ∎

Remark 7.2**.**

The proof of Proposition 5.8, which shows that the functor $r\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ lifts to the category of left maps of the awfs of uniform fibrations, relied crucially on the hypothesis (M6). This says that the image of $r$ lands on the class $\mathcal{M}$ of generating monomorphisms of the suitable topos. As noted in Remark 5.13, hypothesis (M6) does not hold if we consider $\mathcal{M}_{dec}$, the class of decidable monos in the context of a presheaf topos. However notice that the proof of Lemma 7.1 does not require hypothesis (M6). In other words, the extra ‘normality’ condition on the category of uniform fibrations allows us to get rid of this requirement.

The construction of the lift for the other functor $\rho\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ is not quite as direct; we need to briefly recall the construction of the uniform fibration structure produced by Lemma 5.6. Let us consider a map $f\colon X\rightarrow Y$ in $\mathbb{E}$; recall (from the discussion before Proposition 5.8) that the second leg of the factorisation of the diagonal, $\rho_{f}\colon Pf\rightarrow X\times_{Y}X$ can also be obtained as a pullback of the map $\hat{\hom}(i,f)$ where $i\colon\partial I\rightarrow I$ stands for the inclusion of the boundary of the interval. Let us assume for now that $(f,\theta)$ is a uniform fibration. We know that right orthogonal categories of arrows are closed under pullbacks, thus to give a uniform fibration structure to $\rho_{f}$ it is sufficient to give one to $\hat{\hom}(i,f)$. Now, in order to construct a uniform fibration structure for $\hat{\hom}(i,f)$, let us consider a lifting problem with respect to a morphism of the generating category of arrows $\mathcal{I}_{\hat{\times}}$ of uniform fibrations; i.e. a square of the form $(U,b)\colon\delta^{k}\hat{\times}j\rightarrow\hat{\hom}(i,f)$ where $j\colon A\rightarrowtail B$ is in $\mathcal{I}$, for which we show how to construct a lift. This is shown in the left side of the following diagram:

[TABLE]

Transposing along the adjunction $(i\hat{\times}-)\dashv\hat{\hom}(i,-)$ we obtain a square as on the right of the previous diagram. We use that the pushout-product construction is symmetric and associative, and in particular we obtain that $i\hat{\times}(\delta^{k}\hat{\times}j)\cong\delta^{k}\hat{\times}(i\hat{\times}j)$. By hypotheis (M5) of the category of generating cofibrations $\mathcal{M}$ we know that $i\hat{\times}j$ is a generating monomorphism, thus we find a lift for the square on the right of the previous diagram, denoted by $\rho\theta_{i}$. By transposing everything back we obtain the desired lift for the original square. This construction produces a uniform fibration structure for $\hat{\hom}(i,f)$ which we denote by $\rho\theta$.

Lemma 7.3**.**

There is a lift of the functor from Lemma 5.6 as shown:

[TABLE]

Proof.

Since the forgetful functor $\underline{\smash[b]{\text{\rm{NrmUniFib}}}}\rightarrow\underline{\smash[b]{\text{\rm{UniFib}}}}$ is fully faithful (Lemma 6.3), and using that right ortogonal categories are closed under pullbacks; it is sufficient to prove that given $(f,\psi)$ a normal uniform fibration, the uniform fibration structure $\rho\psi$ of $\hat{\hom}(i,f)$, described in the foregoing discussion, is also normal.

By Proposition 6.4, we need to show that, for a generating monomorphism $j\colon A\rightarrowtail B$, the lifts in the diagram on the left of the following figure cohere:

[TABLE]

by transposing the whole diagram along $(i\hat{\times}-)\dashv\hat{\hom}(i,-)$ and using the symmetry and associativity of the pushout-product, we obtain the lifting problem as on the right of the previous diagram, for which we need to show that the lifts cohere. The lift $\rho\theta_{j}$ on the left (on either diagram) is, by construction, the lift obtained from the uniform fibration structure $\rho\theta$ on $\hat{\hom}(i,f)$. The result follows by applying Lemma 6.1. ∎

Proposition 7.4**.**

Consider a suitable topos $(\mathbb{E},I,\mathcal{M})$ satisfying condition (M5). Then the stable functorial factorisation of the diagonal $\mathcal{P}_{I}$ lifts to a stable functorial choice of path objects for the awfs of normal uniform fibrations; as shown in the following diagram:

[TABLE]

Proof.

This follows by applying Lemma 7.1 to lift the functor $r\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$ and by applying Lemma 5.6 and Lemma 7.3 to lift the functor $\rho\colon\mathbb{E}^{\rightarrow}\rightarrow\mathbb{E}^{\rightarrow}$. ∎

We turn our attention to the proof that the category of arrows of normal uniform fibrations has a functorial Frobenius structure. The structure is given by adapting the functorial Frobenius structure on uniform fibrations constructed in [14, Theorem 8.8]. Throughout this section, we will work on an arbitrary suitable topos $(\mathbb{E},I,\mathcal{M})$.

Lemma 7.5**.**

Let $i\colon A\rightarrowtail B$ be a monomorphism, and let $f\colon X\rightarrow B$ be any map. Then the following holds:

1. (1)

There is an isomorphism

[TABLE] 2. (2)

Pulling back the $k$-squash square of $i$ along the square $(I\times f,f)$ produces the $k$-squash square of $f^{*}i$; concretely, for $k\in\{0,1\}$, there is an isomorphism:

[TABLE]

Proof.

To show item $(1)$, let us first consider the following cube:

[TABLE]

Here, the square on the top is the pullback of $i$ along $f$. It is straightforward to verify that all squares pointing from left to right are Cartesian, and note that the squares on the left and right are the outer squares used for defining the pushout-products $\delta^{k}\hat{\times}(f^{*}i)$ and $\delta^{k}\hat{\times}i$ respectively. All of this implies that there is a comparison map $\delta^{k}\hat{\times}(f^{*}i)\rightarrow(I\times f)^{*}(\delta^{k}\hat{\times}i)$, which is an isomorphism because colimits in $\mathbb{E}$ are universal. Item $(2)$ follows directly form item $(1)$. ∎

We recall a result about the squares $\theta^{k}\hat{\times}i\colon i\rightarrow\delta^{k}\hat{\times}i$ from [14, Lemma 4.3].

Lemma 7.6**.**

For every $i\colon A\rightarrow B$, the square $\theta^{k}\hat{\times}i\colon i\rightarrow\delta^{k}\hat{\times}i$ below is Cartesian.

[TABLE]

Proof.

The proof uses once again the fact that colimits in $\mathbb{E}$ are universal. Let us compute the pullback of $\delta^{k}\hat{\times}i$ along $\delta^{1-k}\times B$. By universality of colimits, this is the same as pulling back the diagram defining $B+_{A}(I\times A)$ and then calculating the colimit.

We can observe in the following picture, the result of first pulling back the defining diagram of $B+_{A}(I\times A)$ which appears as the upper span of the right-most square on the following cube:

[TABLE]

Let us notice that the pullback of $\delta^{k}\times B$ (respectively $\delta^{k}\times A$) along $\delta^{1-k}\times B$ (respectively $\delta^{1-k}\times A$) is empty since the interval has disjoint endpoints. We conclude that the colimit of the upper span of the left-most square on the cube must be equal to $A$ and moreover, the universal arrow down to $B$ has to be $i\colon A\rightarrow B$. ∎

Consider a generating monomorphism $i\colon A\rightarrowtail B$ and a uniform fibration $f\colon X\rightarrow B$, then there are two possible trivial uniform cofibration structures on the map $\delta^{k}\hat{\times}(f^{*}i)$: the first one is the canonical one, i.e. the one given by the fact that $f^{*}i$ is also a generating monomorphism. The second one is the one provided by the functorial Frobenius structure on uniform fibrations using the isomorphism $\delta^{k}\hat{\times}(f^{*}i)\cong(I\times f)^{*}(\delta^{k}\hat{\times}i)$ of Lemma 7.5. These two are actually the same structure as we show in the following lemma.

Lemma 7.7**.**

Consider $i\colon A\rightarrowtail B$ be a generating monomorphism and $f\colon X\rightarrow B$ a uniform fibration. Then the two possible trivial uniform cofibration structures on $\delta^{k}\hat{\times}(f^{*}i)$ coincide.

Proof.

Let us denote by $\lambda^{1}$ and $\lambda^{2}$, respectively, the canonical trivial uniform cofibration structure on $\delta^{k}\hat{\times}(f^{*}i)$ and the one obtained by applying the functorial Frobenius structure. In order to prove they are the same, let us consider $g\colon Z\rightarrow Y$ a uniform fibration and a square $(a,b)\colon\delta^{k}\hat{\times}(f^{*}i)\rightarrow g$. Without loss of generality, let us denote by $\lambda^{1}$ and $\lambda^{2}$ the two fillers of this square given by the uniform trivial cofibration structure with the same name. We have to show that $\lambda^{1}=\lambda^{2}$. If we go over the proof of [14, Proposition 8.8], just before the conclusion, a retract diagram is used to transfer the structure of a trivial cofibration to the desired morphism (since trivial cofibrations are closed under retracts). In our situation, this retract diagram is given by the two left-most squares shown below:

[TABLE]

where the left-most square is $\theta^{k}\hat{\times}\delta^{k}\hat{\times}(f^{*}i)$. Notice that $\delta^{k}\hat{\times}\delta^{k}\hat{\times}(f^{*}i)$ has a canonical trivial cofibration structure and thus, the square $\delta^{k}\hat{\times}\delta^{k}\hat{\times}(f^{*}i)\rightarrow f$ has a lift which we denote by $\lambda$. By definition, the lift $\lambda^{2}$ is equal to $\lambda\cdot t$ where $t$ is the horizontal arrow on the lower left part of the diagram.

On the other hand, the lift of the outer square of the previous diagram is $\lambda^{1}$. Thus if we want to show that $\lambda^{1}=\lambda^{2}$ it is sufficient to show that the square $\theta^{k}\hat{\times}\delta^{k}\hat{\times}(f^{*}i)$ is a morphism of trivial uniform cofibrations. To show this, we use that the pushout-product is symmetric and associative, and thus $\theta^{k}\hat{\times}\delta^{k}\hat{\times}(f^{*}i)\cong\delta^{k}\hat{\times}\theta^{k}\hat{\times}(f^{*}i)$. From this, we see that the square is a morphism of trivial uniform cofibrations provided the square $\theta^{k}\hat{\times}(f^{*}i)$ is a morphism of generating monomorphisms, i.e. if it is Cartesian. But this is precisely the statement of Lemma 7.6. ∎

We wish to show that the functorial Frobenius structure on uniform fibrations of [14, Theorem 8.8] can be extended to normal uniform fibrations. We start with a proposition.

Proposition 7.8**.**

There is a lift of the pullback functor as shown:

[TABLE]

Proof.

Object-wise, this follows directly from [14, Theorem 8.8]. To see this, we notice that there are no more objects in the image of the category of arrows $\mathcal{I}^{\bf n}_{\hat{\times}}$ than in the image of $\mathcal{I}_{\hat{\times}}$ thus we can apply the functorial Frobenius structure for uniform fibrations. Then we use the functor $\underline{\smash[b]{\text{\rm{TrivCof}}}}\rightarrow\underline{\smash[b]{\text{\rm{NrmTrivCof}}}}$, obtain by functoriality of the left orthogonal functor ${}^{\boxslash}{(-)}$ applied to the forgetful functor $\underline{\smash[b]{\text{\rm{NrmUniFib}}}}\rightarrow\underline{\smash[b]{\text{\rm{UniFib}}}}$.

For the morphism case, we first notice that the only morphisms in $\mathcal{I}^{\bf n}_{\hat{\times}}$ that we need to consider are the squash squares. Thus let us consider a cospan of squares as in the following diagram:

[TABLE]

such that the vertical square is the squash square of a generating monomorphism $i\colon A\rightarrowtail B$ and the horizontal square is a morphism of uniform fibrations $(m,\epsilon\times B)\colon f^{\prime}\rightarrow f$. We need to verify that pulling back the squash square along the morphism of uniform fibrations is a morphism of normal trivial cofibrations.

The first thing we do is to split this cospan of squares into two, by factoring through the pullback square of $f$ along $\epsilon\times B$. That is we obtain the following diagrams:

[TABLE]

where the dotted arrow $m^{*}\colon X^{\prime}\rightarrow(I\times X)$ is obtain by universal property. Notice that composing the two cospans of squares along their common face, produces the original one. Notice also that the two horizontal squares are morphisms of uniform fibrations.

Let us focus first on the cospan of the right. The identity morphism $1\colon(\delta^{k}\hat{\times}i)\rightarrow(\delta^{k}\hat{\times}i)$ is a morphism of trivial uniform cofibrations, thus if we pull-back this along the morphism of uniform fibrations $(f^{\prime},I\times f)\colon m^{*}\rightarrow 1_{\delta^{k}\hat{\times}i}$ we obtain a morphism of trivial uniform cofibrations by [14, Theorem 8.8] to which we can apply the functor $\underline{\smash[b]{\text{\rm{TrivCof}}}}\rightarrow\underline{\smash[b]{\text{\rm{NrmTrivCof}}}}$ to obtain a morphism of normal trivial cofibrations.

With this we have reduced the situation to the cospan of squares on the left of the previous diagram. Using item $(2)$ of Lemma 7.5 we see that the pullback of the squash square of $i\colon A\rightarrowtail B$ along the square $(I\times f,f)\colon\epsilon\times X\rightarrow\epsilon\times B$ is the squash square of $f^{*}i\colon f^{*}A\rightarrowtail X$. This square is a morphism in $\mathcal{I}^{\bf n}_{\hat{\times}}$ provided that the canonical trivial normal cofibration structure of $\delta^{k}\hat{\times}(f^{*}i)$ is the same as that obtained from the functorial Frobenius structure; but this follows from Lemma 7.7. ∎

Proposition 7.9**.**

Let $(\mathbb{E},I,\mathcal{M})$ be a suitable topos. Then the awfs $(NC_{t},NF)$ of normal uniform fibrations has a functorial Frobenius structure.

Proof.

Using the lift of Proposition 7.8 and the forgetful functor $\underline{\smash[b]{\text{\rm{NrmUniFib}}}}\rightarrow\underline{\smash[b]{\text{\rm{UniFib}}}}$, we find a lift of the pullback functor as one shown:

[TABLE]

The fact that we can extend this structure from $\mathcal{I}^{\bf n}_{\hat{\times}}$ to the whole category $\underline{\smash[b]{\text{\rm{NrmTrivCofi}}}}$ follows from [14, Proposition 6.8]. ∎

Theorem 7.10**.**

Consider a suitable topos $(\mathbb{E},I,\mathcal{M})$ satisfying condition (M5). Then the awfs $(NC_{t},NF)$ of normal uniform fibrations has the structure of a type-theoretic awfs.

Proof.

The claim follows from Proposition 7.4 and Proposition 7.9. ∎

Appendix A Some technical definitions

Let $(\mathbb{C},\rho,\chi)$ be a comprehension category. For $n\in\mathbb{N}$, the category $DT_{n}(\rho,\chi)$ of dependent $n$-tuples over $(\mathbb{C},\rho,\chi)$ is defined as follows. Objects are tuples $(\Gamma,A_{1},\dots,A_{n})$ where $\Gamma$ is an element in the base category, $A_{1}$ is in the fibre of $\rho$ over $\Gamma$ and, for $i>1$, $A_{i}$ is in the fiber over $\Gamma.A_{1}.\cdots.A_{i-1}$. An arrow $(\Delta,B_{1},\dots,B_{n})\rightarrow(\Gamma,A_{1},\dots,A_{n})$ consists of a tuple of the form $(u,f_{1},\dots,f_{n})$ where $f_{1}:B_{1}\rightarrow A_{1}$ is over $u:\Delta\rightarrow\Gamma$ and for $i>1$ we have

[TABLE]

Composition and identities are given component-wise by the structure of the fibration $\rho$. We say that an arrow of dependent tuples is Cartesian if every composing arrow (except the one of the base category) is Cartesian with respect to $\rho$.

$\Sigma$-types and $\Pi$-types

A choice of $\Sigma$-types for $(\mathbb{C},\rho,\chi)$ consists of an operation that assigns to each dependent tuple $(\Gamma,A,B)\in DT_{2}(\rho,\chi)$ a tuple $(\Sigma_{A}B,pair_{A,B},sp_{A,B})$ consisting of the following data:

1. (1)

$\Sigma_{A}B$ is an object of $\mathbb{E}$ over $\Gamma$. 2. (2)

$pair_{A,B}$ is an arrow over $\chi_{A}$ as shown:

[TABLE] 3. (3)

$sp_{A,B}$ is an operation that takes a dependent tuple $(\Gamma,\Sigma_{A}B,C)\in DT_{2}(\chi,\rho)$ and a section $t$ of $C$ over $pair_{A,B}$, as in the following solid arrowed diagram:

[TABLE]

to a section $sp_{A,B}(C,t)$ of $C$, shown in the above diagram as the dotted arrow. 4. (4)

The above data is subject to the condition that, for any section $t$ of $C$ over $pair_{A,B}$, $sp_{A,B}(C,t)\circ pair_{A,B}=t$. Thus says that the triangle in the diagram of item $(3)$ involving the dotted arrow commutes.

A choice of $\Pi$-types for $(\mathbb{C},\rho,\chi)$ consists of an operation that assigns to each dependent tuple $(\Gamma,A,B)\in DT_{2}(\rho,\chi)$ a tuple $(\Pi_{A}B,\lambda_{A,B},app_{A,B})$ consisting of the following data:

1. (1)

$\Pi_{A}B$ is an object of $\mathbb{E}$ over $\Gamma$. 2. (2)

$\lambda_{A,B}$ is an operation that takes a section $t:\Gamma.A\rightarrow\Gamma.A.B$ of $\chi_{B}$ to a section $\lambda_{A,B}(t):\Gamma\rightarrow\Pi_{A}B$ of $\chi_{\Pi_{A}B}$, as shown in the following diagram:

[TABLE] 3. (3)

$app_{A,B}$ is an arrow in the slice over $\Gamma.A$, as shown:

[TABLE]

where $\Gamma.A.\Pi_{A}B$ is (the comprehension of) any reindexing of $\Pi_{A}B$ along $\chi_{A}$. Notice that the choice of $app_{A,B}$ determines uniquely any other choice with respect to a different Cartesian reindexing of $\Pi_{A}B$, this follow by the universal property of Cartesian arrows. 4. (4)

This data must be subject to the condition that, for any section $t\colon\Gamma.A\rightarrow\Gamma.A.B$ of $\chi_{B}$, $app_{A,B}\circ(\lambda(t)[\chi_{A}])=t$. where $\lambda(t)[\chi_{A}]$ is the result of reindexing $\lambda(t)$ along $\chi_{A}$.

Strict stability

Let $(\mathbb{C},\rho,\chi)$ be a split comprehension category.

A choice of $\Sigma$-types $(\Sigma,pair,sp)$ for $(\mathbb{C},\rho,\chi)$ is said to be strictly stable if for every morphism $\sigma:\Delta\rightarrow\Gamma$ in the base category and for any dependent tuple $(\Gamma,A,B)\in DT_{2}(\rho,\chi)$, the following conditions are satisfied:

1. (1)

$\Sigma_{A[\sigma]}B[\sigma]=(\Sigma_{A}B)[\sigma]$ 2. (2)

The following diagram commutes:

[TABLE]

where the horizontal arrows are obtained by the split reindexing along $\sigma$. 3. (3)

For any dependent tuple $(\Gamma,\Sigma_{A}B,C)$ in $DT_{2}(\rho,\chi)$, and any section $t$ of $C$ over $pair_{A,B}$ there is a corresponding dependent tuple $(\Delta,\Sigma_{A[\sigma]}B[\sigma],C[\sigma])$ and a section $t[\sigma]$ of $C$ over $pair_{A[\sigma],B[\sigma]}$ obtained by reindexing. The following diagram is required to commute:

[TABLE]

where the horizontal arrows are obtained by the split reindexing along $\sigma$.

A choice of $\Pi$-types $(\Pi,\lambda,app)$ for $(\mathbb{C},\rho,\chi)$ is said to be strictly stable if for every morphism $\sigma:\Delta\rightarrow\Gamma$ in the base category and for any dependent tuple $(\Gamma,A,B)\in DT_{2}(\rho,\chi)$, the following conditions are satisfied:

1. (1)

$\Pi_{A[\sigma]}B[\sigma]=(\Pi_{A}B)[\sigma]$ 2. (2)

For any section $t$ of $\chi_{B}$ there is a corresponding section $t[\sigma]$ of $\chi_{B[\sigma]}$ obtained by reindexing. This two sections must be related by the following commutative diagram:

[TABLE]

where the lower horizontal arrow is obtained by the split reindexing along $\sigma$. 3. (3)

The following diagram commutes:

[TABLE]

where the horizontal arrows are obtained by split reindexing along $\sigma$.

Pseudostability

Let $(\mathbb{C},\rho,\chi)$ be a comprehension category.

A choice of $\Sigma$-types $(\Sigma,pair,sp)$ for $(\mathbb{C},\rho,\chi)$ is said to be pseudo-stable if for every Cartesian arrow $(\sigma,f,g):(\Delta,A^{\prime},B^{\prime})\rightarrow(\Gamma,A,B)$ of dependent tuples, the following conditions are satisfied:

1. (1)

There is a Cartesian arrow $\Sigma_{f}g:\Sigma_{A^{\prime}}B^{\prime}\rightarrow\Sigma_{A}B$ over $\sigma$ and the assignment:

[TABLE]

is functorial, i.e. $\Sigma_{1_{A}}1_{B}=1_{\Sigma_{A}B}$ and $\Sigma_{(f^{\prime}\circ f)}(g^{\prime}\circ g)=\Sigma_{f^{\prime}}g^{\prime}\circ\Sigma_{f}g$. 2. (2)

The following diagram commutes:

[TABLE] 3. (3)

For any Cartesian arrow $h:C^{\prime}\rightarrow C$ above $\Sigma_{f}g:\Sigma_{A^{\prime}}B^{\prime}\rightarrow\Sigma_{A}B$ and for any section $t$ of $C$ over $pair_{A,B}$ there is a corresponding section $t^{\prime}$ of $C^{\prime}$ over $pair_{A^{\prime},B^{\prime}}$ obtained by reindexing. The following diagram is required to commute:

[TABLE]

A choice of $\Pi$-types $(\Pi,\lambda,app)$ for $(\mathbb{C},\rho,\chi)$ is said to be pseudo-stable if for every Cartesian arrow $(\sigma,f,g):(\Delta,A^{\prime},B^{\prime})\rightarrow(\Gamma,A,B)$ of dependent tuples, the following conditions are satisfied:

1. (1)

There is a Cartesian arrow $\Pi_{f}g:\Pi_{A^{\prime}}B^{\prime}\rightarrow\Pi_{A}B$ over $\sigma$ and the assignment:

[TABLE]

is functorial, i.e. $\Pi_{1_{A}}1_{B}=1_{\Pi_{A}B}$ and $\Pi_{(f^{\prime}\circ f)}(g^{\prime}\circ g)=\Pi_{f^{\prime}}g^{\prime}\circ\Pi_{f}g$. 2. (2)

For any section $t:\Gamma.A\rightarrow\Gamma.A.B$ of $B$ there is a corresponding section $t^{\prime}:\Delta.A^{\prime}\rightarrow\Delta.A^{\prime}.B^{\prime}$ of $B^{\prime}$ obtained by reindexing along $f:\Delta.A^{\prime}\rightarrow\Gamma.A$. Then, the following diagram commutes:

[TABLE] 3. (3)

The following diagram commutes:

[TABLE]