Univalent polymorphism

TL;DR

This paper constructs models of Homotopy Type Theory within the effective topos using path categories, demonstrating univalent representations for propositions and sets, thus connecting to the Calculus of Constructions.

Contribution

It introduces a path category model of the effective topos with univalent representations for propositions and sets, advancing the understanding of homotopy-theoretic models in type theory.

Findings

Effective topos as homotopy category of a path category

Existence of a univalent universe of propositions

Construction of a univalent universe of sets

Abstract

We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category $\mathbb{EFF}$. Path categories are categories of fibrant objects in the sense of Brown satisfying two additional properties and as such provide a context in which one can interpret many notions from homotopy theory and Homotopy Type Theory. Within the path category $\mathbb{EFF}$ one can identify a class of discrete fibrations which is closed under push forward along arbitrary fibrations (in other words, this class is polymorphic or closed under impredicative quantification) and satisfies propositional resizing. This class does not have a univalent representation, but if one restricts to those discrete fibrations whose fibres are propositions in the sense of Homotopy Type Theory, then it does. This means that, modulo the usual coherence problems, it can be seen as a model of the Calculus of Constructions with a univalent type of propositions. We will also build a more complicated path category in which the class of discrete fibrations whose fibres are sets in the sense of Homotopy Type Theory has a univalent representation, which means that this will be a model of the Calculus of Constructions with a univalent type of sets.

Equations

$$f^{\ast }:\mathcal{C}(X)\to \mathcal{C}(Y),$$

$$\Gamma :Y{\times }_{X}PX\to Y$$

$$\Gamma :Y{\times }_{X}PX\to Y.$$

$$\Gamma (s{p}_1,p_2),\Gamma (t{p}_1,p_2):P_X(Y){\times }_{X}PX\to Y$$

$$\Gamma (p_1,s{p}_2),\Gamma (p_1,t{p}_2):Y{\times }_X{P}_{X\times X}(PX)\to Y$$

$$\Gamma (p_1,\mu (p_3,p_2)),\Gamma (\Gamma (p_1,p_2),p_3):Y{\times }_{X}PX{\times }_{X}PX\to Y$$

$${\Pi }_f(P_Y(Z)))\to {\Pi }_f(Z){\times }_X{\Pi }_f(Z)$$

$$D$$

$$\delta (c,b)$$

$$\mathcal{D}((c,b),(c^{\prime },b^{\prime }))$$

$$P$$

$$\pi (a,a^{\prime },\rho )$$

$$\mathcal{P}((a,a^{\prime },\rho ),(b,b^{\prime },\sigma ))$$

$$P:\mathbb{EFF}\to \mathcal{E}ff$$

$$a{=}_A{a}^{\prime }=\{<n,\pi ,n^{\prime }>:n=\alpha (a),n^{\prime }=\alpha (a^{\prime }),\pi \in \mathcal{A}(a,a^{\prime })\}$$

$$F(b,a)=\{<m,\pi ,n>:m=\beta (b),n=\alpha (a),\pi \in \mathcal{A}(fb,a).\}$$

$$A$$

$$\alpha (<x,n>)$$

$$\mathcal{A}(<x,n>,<x^{\prime },n^{\prime }>)$$

$${\Pi }_f(g):(D,\delta ,\mathcal{D})\to (A,\alpha ,\mathcal{A})$$

$$N$$

$$\nu (n)$$

$$\mathcal{N}(n,n)$$

$$\mathcal{N}(n,m)$$

$$J$$

$$j(i)$$

$$\mathcal{J}(i,i)$$

$$\mathcal{J}(i,k)$$

$$d:B\to \{(b_0,b_1):f(b_0)=f(b_1),\beta (b_0)=\beta (b_1)\}$$

$$b_0\sim b_1\text{mbox}ifandonlyiff(b_0)=f(b_1)\text{mbox}and\beta (b_0)=\beta (b_1),$$

$$I$$

$$\iota (i)$$

$$\mathcal{I}(i,j)$$

$$f:(B,\beta ,\mathcal{B})\to (A,\alpha ,\mathcal{A})$$

$$P$$

$$\pi (b,b^{\prime },\pi )$$

$$\mathcal{P}((b_0,b_0^{\prime },{\pi }_0),(b_1,b_1^{\prime },{\pi }_1))$$

$$C=\{(a,n):(\exists b)f(b)=a,\beta (b)=n\},$$

Full text

1. Introduction

There has been a continuing interest in obtaining models of impredicative type theories, like the Calculus of Constructions (CoC). One reason is the use of CoC as the basis of proof assistants such as Coq and Lean; on a more theoretical level, these models shed light on issues surrounding impredicativity. Recently, the quest for models has received a new impetus due to the influence of Homotopy Type Theory (HoTT). Some natural questions which have arisen are whether it is possible to have universes which are both impredicative and univalent, how the type Prop of propositions in CoC relates to the notion of proposition in HoTT and whether one can obtain models of Voevodsky’s resizing axioms.

So what is needed to model CoC? Roughly, what one needs is a category equipped with two classes of maps, one (“the small fibrations”) contained in the other (“the fibrations”), and where both classes are pullback stable, closed under composition and contain all isomorphisms. One needs a particular small fibration (a “representation”) such that any other small fibration can be obtained as a pullback of that one; in addition, one needs to be able to push forward fibrations along other fibrations (where push forward is the right adjoint to pullback), and, crucially, one needs that small fibrations are closed under being pushed forward along arbitrary fibrations (this is what is meant by impredicativity in this context).

There is an old idea (see [13]) that models of CoC can be obtained by looking at Hyland’s effective topos ${\mathcal{E}\!f\!f}$ [11]: the idea is that in this case every map is fibration and the small fibrations are the discrete maps, with a map in the effective topos being discrete if all its fibres are subcountable. It turns out that this does not quite work, due to a certain ambiguity in the notion of a discrete map, as explained in [13]. There is a global notion of a discrete map, where one says that a map $f:Y\to X$ in ${\mathcal{E}\!f\!f}$ is discrete if $f$ can be covered by a subobject of the natural numbers object $\pi_{X}:\mathbb{N}\times X\to X$ in ${\mathcal{E}\!f\!f}/X$ (this is how discrete maps are defined in [16, Definition 3.4.2(i)]). In this case the discrete maps have a representation, but are not stable under push forward along arbitrary maps (see [13, Proposition 7.5]). Alternatively, there is the local notion of a discrete map, where one says that a map $f:Y\to X$ is discrete if there is an epi $q:X^{\prime}\to X$ such that $q^{*}f$ is covered by a subobject of the natural numbers object $\pi_{X^{\prime}}:\mathbb{N}\times X^{\prime}\to X^{\prime}$ in ${\mathcal{E}\!f\!f}/X^{\prime}$ (this is equivalent to saying that, internally, $f$ has the right lifting property with respect to $\Omega\to 1$ or $\nabla(2)\to 1$). In this case the discrete maps are stable under push forward along arbitrary maps, but it is still an open question whether the discrete maps defined in this local manner have a representation in ${\mathcal{E}\!f\!f}$.

The standard way of solving this problem is to restrict to the $\lnot\lnot$-separated objects in the effective topos (the assemblies; see also [6, 12]). Within these assemblies the distinction between the two notions of a discrete map disappears (see [13, Proposition 6.7]) and the discrete maps have a representation and are closed under push forward along arbitrary maps. This means that within the assemblies one can obtain a model of CoC, and to this day this remains the “standard” model for CoC.

This paper suggests an alternative solution. The first step in this direction is the observation that the the effective topos arises as the homotopy category of a certain path category, which we will denote $\mathbb{EFF}$.

The notion of a path category, short for a category with path objects, was first introduced in [3] and provides an abstract categorical setting for doing homotopy theory, in a manner similar to Quillen’s model categories. Path categories are categories equipped with two classes of maps, fibrations and equivalences, satisfying a number of axioms which strengthen Ken Brown’s axioms for a category of fibrant objects [5] (in that sense the notion of a path category is similar to Joyal’s notion of a tribe [14], with the notion of a tribe being the stronger of the two). From a type-theoretic perspective, path categories provide models of “propositional identity types” (models of Martin-Löf’s identity types but with the computation rule formulated as a propositional equality; see [1]). The key notions from Homotopy Type Theory such as transport, univalence and hlevel, make sense in any path category, and therefore these notions make sense in $\mathbb{EFF}$ as well.

It turns out that in $\mathbb{EFF}$ one can define a notion of discrete fibration which is stable under push forward along arbitrary fibrations. It is still unclear if the class of discrete fibrations has a representation in $\mathbb{EFF}$; however, if we restrict the hlevel of its fibres to propositions in the sense of HoTT, the discrete fibrations will have a representation and will still be be closed under push forward along arbitrary fibrations. In fact, its representation is essentially the subobject classifier in the effective topos and this representation will be univalent in $\mathbb{EFF}$. That means that with the class of propositional discrete fibrations as the small fibrations, $\mathbb{EFF}$ is a model of CoC with a univalent Prop. Given that the homotopy category of $\mathbb{EFF}$ is the effective topos, this may not be so surprising. However, the author of this paper thinks it is quite satisfying to see the notion of proposition from CoC, HoTT and the effective topos match up nicely like this. In addition, it is interesting to note that $\mathbb{EFF}$ is a model of propositional resizing. (This should be compared with the negative result due to Taichi Uemura [23], showing that it fails in cubical assemblies.)

One way in which the model in $\mathbb{EFF}$ is somewhat poor is that its universe only contains propositions (in the sense of HoTT) and therefore excludes many data types like $\mathbb{N}$ or $\mathbb{N}\to\mathbb{N}$ (in that it differs from the standard model in assemblies). The difficulty is that these objects are not propositions, but actually live one hlevel higher: that is, they are sets in the sense of HoTT. For that reason I will also construct a more complicated path category $\mathbb{EFF}_{1}$ in which the class of fibrations of discrete sets is an impredicative class of small fibrations with a univalent representation. This univalent universe will also contain such objects as $\mathbb{N}$ or $\mathbb{N}\to\mathbb{N}$.

There is a clear sense in which the construction of $\mathbb{EFF}_{1}$ is the natural next step after the construction of $\mathbb{EFF}$. The natural next step after that would be the construction of a path category $\mathbb{EFF}_{2}$ in which the class of discrete fibrations of groupoids would be closed under push forward along arbitrary fibrations and would have a univalent representation. In the limit one would expect to be able to construct a path category $\mathbb{EFF}_{\infty}$ in which the class of discrete fibrations (without any restriction on its hlevel) would be closed under push forward along arbitrary fibrations and have a univalent representation. This would provide an alternative way of salvaging the original idea of obtaining models of CoC using discrete fibrations.

At this point I should make two important disclaimers. Firstly, when I say that $\mathbb{EFF}$ and $\mathbb{EFF}_{1}$ are models of CoC, I am ignoring the usual coherence problems related to substitution. I suspect it would be relatively straightforward to solve this by some careful rephrasing in terms of categories with families [7, 10], but I am leaving this to future work. Secondly, and this may be the more essential point, $\mathbb{EFF}$ and $\mathbb{EFF}_{1}$ will be models of a version of CoC in which many definitional equalities have been replaced by propositional ones: this applies not just to the computation rule for the identity type, but to many computation rules. In fact, I am imagining a version of CoC in which the notion of definitional equality has been completely eliminated in favour of the notion of propositional equality. I am currently working on writing down a precise syntax for such a system, but this is still work in progress. I suspect that a reader familiar with the categorical semantics of type theory can guess what it would look like on the basis of the categorical definitions in Section 2 below.

Throughout this paper we will rely on categorical language: familiarity with the language of type theory will not be assumed.

Finally, unless explicitly noted otherwise, the results obtained here are all constructive. However, since we will be interested in building models of impredicative type theories, our metatheory will be impredicative as well, which means that our metatheory will be something like intuitionistic Zermelo-Fraenkel set theory (IZF) or the internal logic of an elementary topos with a natural numbers object (both can be seen as subsystems of ZF). Results which rely on the axiom of choice will be marked with the label (ZFC).

2. Path categories

We will start this paper by discussing the notion of a path category, as introduced in [3], and by showing how many of the concepts in Homotopy Type Theory make sense in the context of a path category. The reader who wishes to see more details should consult Section 2 of [3].

2.1. Definition

Let me first give the definition.

Definition 2.1**.**

A path category (short for a category with path objects) is a category $\mathcal{C}$ equipped with two classes of maps, called fibrations and equivalences, respectively. A fibration which is also an equivalence will be called trivial. If $X\to PX\to X\times X$ is a factorisation of the diagonal on $X$ as an equivalence followed by a fibration, then $PX$ is a path object for $X$. In this case, we will often denote the equivalence $X\to PX$ by $r$ and the fibration $PX\to X\times X$ by $(s,t)$. In a path category the following axioms should be satisfied:

1. (1)

Isomorphisms are fibrations and fibrations are closed under composition. 2. (2)

$\mathcal{C}$ has a terminal object 1 and $X\to 1$ is always a fibration. 3. (3)

The pullback of a fibration along any other map exists and is again a fibration. 4. (4)

Isomorphisms are equivalences and equivalences satisfy 6-for-2: that is, if $f,g,h$ are maps for which the composition $hgf$ is defined and for which $hg$ and $gf$ are equivalences, then $f,g,h$ and $hgf$ are equivalences as well. 5. (5)

Every object $X$ has at least one path object. 6. (6)

Trivial fibrations are stable under pullback along arbitrary maps. 7. (7)

Trivial fibrations have sections.

Remark 2.2**.**

In [1, 3] the equivalences were called weak equivalences. Since every object in a path category is both fibrant and cofibrant (to use the language of model categories) and we have Theorem 2.7 below, there does not really seem to be much need for the adjective “weak”, so we have decided to drop it. Indeed, the HoTT book [19] simply calls this class of maps equivalences, without the adjective.

A basic fact about path categories is that they are stable under slicing.

Definition 2.3**.**

Let $\mathcal{C}$ be a path category and $X$ be an object in $\mathcal{C}$. Write ${\mathcal{C}}(X)$ for the full subcategory of ${\mathcal{C}}/X$ whose objects are fibrations. With the equivalences and fibrations as in $\mathcal{C}$, this is again a path category.

Proposition 2.4**.**

If $f:Y\to X$ is a morphism in a path category, then the functor

[TABLE]

obtained by pulling back fibrations along $f$, preserves all the structure of a path category: that is, it preserves fibrations, equivalences, the terminal object and pullbacks of fibrations along arbitrary maps.

Proof.

See [3, Proposition 2.6]. ∎

2.2. Homotopy in path categories

On parallel morphisms in a path category one can define a homotopy relation, as follows.

Definition 2.5**.**

If $f,g:Y\to X$ are two parallel maps in a path category, then we say that $f$ and $g$ are homotopic if there is a map $H:Y\to PX$ to a path object on $X$ making

{PX}$${Y}$${X\times X}$$\scriptstyle{(s,t)}$$\scriptstyle{(f,g)}$$\scriptstyle{H}

commute. (One can show that this is independent of the choice of path object $PX$.) In this case we write $f\simeq g$, or $H:f\simeq g$ if we wish to stress the homotopy $H$. More generally, suppose $p:X\to I$ is a fibration and $P_{I}(X)$ is the path object of $X$ in the slice category $\mathcal{C}(I)$. If $f,g:Y\to X$ are two parallel maps with $pf=pg$, then we say that $f$ and $g$ are fibrewise homotopic if there is a map $H:Y\to P_{I}(X)$ making

{P_{I}X}$${Y}$${X\times_{I}X}$$\scriptstyle{(s,t)}$$\scriptstyle{(f,g)}$$\scriptstyle{H}

commute. (This is again independent of the choice of path object $P_{I}(X)$.) In this case we write $f\simeq_{I}g$, or $H:f\simeq_{I}g$ if we wish to stress the fibrewise homotopy $H$.

Theorem 2.6**.**

The homotopy relation $\simeq$ is a congruence on $\mathcal{C}$.

Proof.

This is Theorem 2.14 in [3]. ∎

The quotient is the homotopy category of $\mathcal{C}$. A map which becomes an isomorphism in the homotopy category is called a homotopy equivalence.

Theorem 2.7**.**

The equivalences and homotopy equivalences coincide in a path category.

Proof.

This is Theorem 2.16 in [3]. ∎

Using the notion of homotopy we can strengthen Theorem 2.6.

Proposition 2.8**.**

Every object in a path category carries a groupoid structure up to homotopy. More precisely, if $A$ is an object in a path category and $PA$ is a path object for $A$ with equivalence $r:A\to PA$ and fibration $(s,t):PA\to A\times A$, while $PA\times_{A}PA$ is the pullback

{PA\times_{A}PA}$${PA}$${PA}$${A,}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{2}}$$\scriptstyle{t}$$\scriptstyle{s}

then there are maps $\mu:PA\times_{A}PA\to PA$ and $\sigma:PA\to PA$ with $(s,t)\mu=(sp_{2},tp_{1})$ and $(s,t)\sigma=(t,s)$ such that:

1. (1)

$\mu(p_{1},\mu(p_{2},p_{3}))\simeq_{A\times A}\mu(\mu(p_{1},p_{2}),p_{3}):PA\times_{A}PA\times_{A}PA\to PA$. 2. (2)

$\mu(1,rs)\simeq_{A\times A}1:PA\to PA$. 3. (3)

$\mu(rt,1)\simeq_{A\times A}1:PA\to PA$. 4. (4)

$\mu(1,\sigma)\simeq_{A\times A}rt:PA\to PA$. 5. (5)

$\mu(\sigma,1)\simeq_{A\times A}rs:PA\to PA$.

Proof.

See [1, Proposition A.6]. ∎

Remark 2.9**.**

In fact, the arguments in [2, 4] can be modified to show that every object in a path category carries the structure of a Grothendieck $\infty$-groupoid.

2.3. Transport and univalence

A crucial concept in homotopy type theory is transport.

Definition 2.10**.**

Let $f:Y\to X$ be a fibration, and $Y\times_{X}PX$ be the following pullback

{Y\times_{X}PX}$${PX}$${Y}$${X}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{2}}$$\scriptstyle{s}$$\scriptstyle{f}

A transport structure $\Gamma$ on $f$ is a map

[TABLE]

such that $f\Gamma=tp_{2}$ and $\Gamma(1_{Y},rf)\simeq_{X}1_{Y}$.

The intuition behind transport is the following: given a fibration $f:Y\to X$, an element $y_{0}\in Y$ and a path $\alpha:x_{0}\to x_{1}$ in $X$ with $f(y_{0})=x_{0}$, transport finds an element $y_{1}$ in $Y$ with $f(y_{1})=x_{1}$. In addition, we require that if $\alpha$ would the reflexivity path at $x_{0}$, then $y_{1}$ should be connected to $y_{0}$ by a path lying in the fibre over $x_{0}$.

Theorem 2.11**.**

Every fibration $f:Y\to X$ carries a transport structure and transport structures are unique up to fibrewise homotopy over $X$.

Proof.

This is Theorem 2.26 in [3]. ∎

In the sequel we will frequently rely on the following properties of transport.

Proposition 2.12**.**

Let $f:Y\to X$ be a fibration with transport structure

[TABLE]

Then:

1. (1)

$\Gamma$* preserves fibrewise homotopy. More precisely, the maps*

[TABLE]

are fibrewise homotopic. 2. (2)

If you have two paths in $X$ which have the same end points and which are homotopic relative those end points, then the transports of $y\in Y$ along both paths are fibrewise homotopic. More precisely, the maps

[TABLE]

are fibrewise homotopic. 3. (3)

The transport of an element in $Y$ along the composition of two paths and the result of first transporting it along one path and then along the other are fibrewise homotopic. More precisely, the maps

[TABLE]

are fibrewise homotopic.

Proof.

See [1, Lemma A.10-12]. ∎

Proposition 2.13**.**

Suppose $p:Y\to X$ is a fibration and $f,g:Z\to X$ are two parallel maps which are homotopic via a homotopy $H:Z\to PX$. The morphism $f^{*}p\to g^{*}p$ over $Z$ induced by $H$ and the transport structure on $p$ is an equivalence.

Proof.

To be clear, if $H:Z\to PX$ is the homotopy and $\Gamma:Y\times_{X}PX\to Y$ is a transport structure, the induced map $f^{*}p\to g^{*}p$ is:

{Z{}_{f}\kern-0.5pt{\times}_{p}Y}$${Z\times_{X}Y\times_{X}PX}$${Z{}_{g}\kern-0.5pt{\times}_{p}Y.}$$\scriptstyle{1\times_{X}H\pi_{Z}}$$\scriptstyle{Z\times_{X}\Gamma}

Since every path in $PX$ has an inverse up to homotopy, there is also an operation $g^{*}p\to f^{*}p$ induced by the inverse of the homotopy $H$. Using the properties of transport from the previous proposition one can show that this operation is homotopy inverse to the one induced by $H$. ∎

A fibration is univalent if we can also go in the other direction, as follows.

Definition 2.14**.**

The fibration $p:Y\to X$ is univalent if the following holds: whenever $f,g:Z\to X$ are two morphisms and $w:f^{*}p\to g^{*}p$ is an equivalence in the slice over $Z$, then there is a homotopy $H:Z\to PX$ between $f$ and $g$ such that $w$ is, up to fibrewise homotopy over $Z$, the equivalence induced by $H$, as in the previous proposition.

Remark 2.15**.**

In other words, if $p:Y\to X$ is a fibration, then any path $\pi:x\to x^{\prime}$ in $X$ induces an equivalence between the fibres $Y_{x}\simeq Y_{x^{\prime}}$; a fibration is univalent if, up to fibrewise homotopy, every equivalence between the fibres is obtained in this way. This may look a bit different from the way univalence is usually stated, but it is equivalent to the standard formulation, as discussed on the HoTT mailing list. See also [18, Theorem 3.5] for more details.

2.4. Function spaces

No type theory is complete without function types. We will work with function types in the following form, that is, they will be exponentials in the homotopy category.

Definition 2.16**.**

If $X$ and $Y$ are objects in a path category, then we will call an object $X^{Y}$ the homotopy exponential of $X$ and $Y$ if it comes equipped with a map ${\rm ev}:X^{Y}\times Y\to X$ such that for any map $h:A\times Y\to X$ there is a map $H:A\to X^{Y}$ such that ${\rm ev}(H\times 1_{Y})\simeq h$, with $H$ being unique up to homotopy with this property.

Remark 2.17**.**

Perhaps two remarks are in order about this definition of a homotopy exponential from a type-theoretic perspective. First of all, we only demand that ${\rm ev}(H\times 1_{Y})$ and $h$ are homotopic, rather than equal. This basically states $\beta$-equality in a propositional, rather than a definitional form: this reflects the fact that we are thinking of a version of type theory in which all the computational rules have been stated propositionally. Secondly, the fact that $H$ is unique up to homotopy amounts to the validity of function extensionality. (See also [3, Remark 5.8].) Similar remarks apply to the following definition of homotopy $\Pi$-types.

Definition 2.18**.**

If $g:Z\to Y$ and $f:Y\to X$ are fibration, then the homotopy $\Pi$-type of $f$ along $g$ is a fibration $\Pi_{f}(g):E\to X$ equipped with a map $\varepsilon:f^{*}\Pi_{f}(g)\to g$ over $Y$ such that for any $h:A\to X$ and $m:f^{*}h\to g$ over $Y$ there exists a map $M:h\to\Pi_{f}(g)$ such that $\varepsilon\circ f^{*}M\simeq_{Y}m$, with $M$ being unique up to fibrewise homotopy over $X$ with this property. We will say that a path category $\mathcal{C}$ has homotopy $\Pi$-types if all such homotopy $\Pi$-types exist for fibrations $f$ and $g$.

One can phrase this in terms of right adjoints but one has to be a bit careful. If $\mathcal{C}$ is a path category with homotopy $\Pi$-types and $f:Y\to X$ is a fibration in $\mathcal{C}$, then the pullback functor $f^{*}:{\mathcal{C}}(X)\to{\mathcal{C}}(Y)$ has a right adjoint if we pass to the homotopy category. That is, there is an operation $\Pi_{f}:{\mathcal{C}}(Y)\to{\mathcal{C}}(X)$ which goes in the other direction, but it is only a functor up to fibrewise homotopy over $X$.

Also, we cannot really say that the operation $\Pi_{f}:{\mathcal{C}}(Y)\to{\mathcal{C}}(X)$ preserves fibrations. We do have the following statement, however, which is a good substitute.

Proposition 2.19**.**

Let $\mathcal{C}$ be a path category with homotopy $\Pi$-types. Assume $f:Y\to X$ is a fibration in ${\mathcal{C}}$, while $p:B\to A$ is a fibration in ${\mathcal{C}}(Y)$ and $\Pi_{f}(A)$ is a homotopy $\Pi$-type in ${\mathcal{C}}(X)$. Then there exists a homotopy $\Pi$-type $\Pi_{f}(B)$ in ${\mathcal{C}}(X)$ together with a fibration $\Pi_{f}(p):\Pi_{f}(B)\to\Pi_{f}(A)$ in ${\mathcal{C}}(X)$ such that:

1. (1)

The diagram

{f^{*}\Pi_{f}(B)}$${B}$${f^{*}\Pi_{f}(A)}$${A}$$\scriptstyle{f^{*}\Pi_{f}(p)}$$\scriptstyle{\varepsilon}$$\scriptstyle{p}$$\scriptstyle{\varepsilon}

in ${\mathcal{C}}(Y)$ commutes. 2. (2)

For each object $C$ in ${\mathcal{C}}(X)$ the diagram

{{\rm Ho}({\mathcal{C}}(X))(C,\Pi_{f}(B))}$${{\rm Ho}({\mathcal{C}}(Y))(f^{*}C,B)}$${{\rm Ho}({\mathcal{C}}(X))(C,\Pi_{f}(A))}$${{\rm Ho}({\mathcal{C}}(Y))(f^{*}C,A)}

is a pullback in ${\mathcal{S}ets}$.

Proof.

(Compare [3, Proposition 5.5].) We construct $\Pi_{f}(p)$ as follows. First, we take the pullback

{P}$${B}$${f^{*}\Pi_{f}(A)}$${A}$$\scriptstyle{q}$$\scriptstyle{p}$$\scriptstyle{\varepsilon}

and then we define $\Pi_{f}(p)$ to be $\Pi_{\pi}(q)$, where $\pi:f^{*}\Pi_{f}(A)\to\Pi_{f}(A)$ is the projection. ∎

2.5. Homotopy $n$-types

One can also makes sense of Voevodsky’s homotopy levels in the context of path categories.

Definition 2.20**.**

The fibrations of $n$-types ($n\geq-2$) are defined inductively as follows:

• •

A fibration $f:Y\to X$ is a fibration of $(-2)$-types if $f$ is trivial.

• •

A fibration $f:Y\to X$ is a fibration of $(n+1)$-types if $P_{X}(Y)\to Y\times_{X}Y$ is a fibration of $n$-types for some path object $P_{X}(Y)$ for $f$ in ${\mathcal{C}}(X)$.

An object $X$ in a path category is called an $n$-type if the map $X\to 1$ is a fibration of $n$-types.

Definition 2.21**.**

For small $n$ we will often use the following terminology for $n$-types, as is customary in the context of HoTT.

[TABLE]

In the definition of a fibration of $(n+1)$-types the dependence on the choice of path object $P_{X}(Y)$ is only apparent. The reason for this is that path objects are unique up to equivalence (see [3, Corollary 2.39]) and we have the following proposition.

Proposition 2.22**.**

Let $f$ be a fibration of $n$-types.

1. (1)

If $g$ is a fibration which can be obtained by pulling back $f$ along some map, then $g$ is also a fibration of $n$-types. 2. (2)

If $w$ is an equivalence and $g$ is a fibration such that $f\simeq gw$ or $fw\simeq g$, then $g$ is also a fibration of $n$-types. 3. (3)

If $w$ is an equivalence and $g$ is a fibration such that $f\simeq wg$ or $wf\simeq g$, then $g$ is also a fibration of $n$-types.

Proof.

(1) is easily proved by induction on $n\geq-2$ using Proposition 2.4.

(2) It suffices to prove that if $g=fw$ and $w$ is an equivalence, then $g$ is a fibration of $n$-types. To see this, note, first of all, that if $g\simeq fw$, then there is a map $w^{\prime}$ homotopic to $w$ such that $g=fw^{\prime}$ (see [3, Proposition 2.31]); such a map $w^{\prime}$ is an equivalence as well, because it is homotopic to $w$. Furthermore, if $gw\simeq f$, then $g\simeq fw^{-1}$ for a homotopy inverse $w^{-1}$ of $w$; and such a homotopy inverse is an equivalence as well.

So we prove that if $g=fw$ and $w:Z\to Y$ is an equivalence and $f:Y\to X$ and $g:Z\to X$ are fibrations, with $f$ being a fibration of $n$-types, then $g$ is a fibration of $n$-types as well. This statement is proved by induction on $n$, with the case $n=0$ following from 6-for-2 for equivalences.

So assume the statement is true for $n$ and $f$ is a fibration of $(n+1)$-types. We have a commuting diagram of the form

{Z}$${P_{X}(Z)}$${Z\times_{X}Z}$${Y}$${P_{X}(Y)}$${Y\times_{X}Y.}$$\scriptstyle{w}$$\scriptstyle{w\times_{X}w}

In this diagram we have a dotted arrow down the middle which make the diagram on the left commute up to homotopy, while the diagram of the right commutes on the nose (see [3, Theorem 2.38]). The dotted arrow is an equivalence because all the other arrows in the left hand square are. In addition, because equivalences are stable under pullback along fibrations (see [3, Proposition 2.7]), we have that $w\times_{X}w$ and the inscribed map $P_{X}(Z)\to(w\times_{X}w)^{*}P_{X}(Y)$ are equivalences as well. By assumption, the map $P_{X}(Y)\to Y\times_{X}Y$ is a fibration of $n$-types, so by (1) the same is true for its pullback along $w\times_{X}w$, and hence the same is true for $P_{X}(Z)\to Z\times_{X}Z$ by induction hypothesis. Hence $g$ is a fibration of $(n+1)$-types.

(3) Again, it suffices to prove only one of the two statements and we will show that $f\simeq wg$ implies that $g$ is a fibration of $n$-types. So assume $f\simeq wg$ and construct the following pullback

{D}$${B}$${C}$${A.}$$\scriptstyle{v}$$\scriptstyle{h}$$\scriptstyle{f}$$\scriptstyle{w}

We have $wgv\simeq fv=wh$ and since $w$ is an equivalence, it follows that $h\simeq gv$. Since $v$ is an equivalence by [3, Proposition 2.7] and $h$ is a fibration of $n$-types by (1), this implies that $g$ is a fibration of $n$-types by (2). ∎

Theorem 2.23**.**

If $\mathcal{C}$ is a path category with homotopy $\Pi$-types, then $\Pi_{f}:{\mathcal{C}}(Y)\to{\mathcal{C}}(X)$ preserves fibrations of $n$-types for any fibration $f:Y\to X$.

Proof.

This is Theorem 7.1.9 in the HoTT book [19]. The proof is by induction on $n\geq-2$.

We have seen that $\Pi_{f}$ is not really a functor, but it is one up to homotopy. For that reason it preserves equivalences and therefore the statement is true for $n=-2$.

For the induction step, suppose that $p:Z\to Y$ is a fibration on $(n+1)$-types in ${\mathcal{C}}(Y)$; so $P_{Y}(Z)\to Z\times_{Y}Z$ is a fibration of $n$-types. Since $\Pi_{f}(Z)\times_{X}\Pi_{f}(Z)$ is a homotopy $\Pi$-type of $Z\times_{Y}Z$ along $f$, we can compute $\Pi_{f}(P_{Y}(Z))$ as in the proof of Proposition 2.19, which, by induction hypothesis and the previous proposition, ensures that

[TABLE]

will be a fibration of $n$-types. Since $\Pi_{f}$ preserves equivalences, $\Pi_{f}(P_{Y}(Z))$ is a path object for $\Pi_{f}(Z)$ in ${\mathcal{C}}(X)$ and therefore $\Pi_{f}(Z)\to X$ is a fibration of $(n+1)$-types, as desired. ∎

Definition 2.24**.**

The $n$-truncation of a fibration $f:B\to A$ is a factorisation of $f$ as a map $g:B\to C$ followed by a fibration on $n$-types $h:C\to A$, in such a way that if $g^{\prime}:B\to C^{\prime}$ and $h^{\prime}:C^{\prime}\to A$ is another such factorisation, then there exists a map $d:C\to C^{\prime}$ over $A$ with $dh\simeq_{A}g^{\prime}$; if, moreover, $d^{\prime}:C\to C^{\prime}$ would be another such map then $d\simeq_{A}d^{\prime}$.

2.6. Small fibrations

Let us suppose ${\mathcal{S}}$ is a subclass of the class of fibrations which is closed under composition, contains all isomorphisms and is stable under homotopy pullback. (Recall that a commutative square

{D}$${B}$${C}$${A}$$\scriptstyle{g}$$\scriptstyle{f}

in which both $f$ and $g$ are fibrations is a homotopy pullback if the induced map $D\to C\times_{A}B$ is an equivalence. By saying that ${\mathcal{S}}$ is stable under homotopy pullback, we mean that whenever there is such a square and $f$ belongs to ${\mathcal{S}}$, then $g$ belongs to ${\mathcal{S}}$ as well.) Let us refer to the elements of ${\mathcal{S}}$ as the “small fibrations”.

Definition 2.25**.**

Let ${\mathcal{S}}$ be a class of small fibrations, as above. A representation for such a class ${\mathcal{S}}$ is a small fibration $\pi:E\to U$ such that any other small fibration $f:B\to A$ can be obtained as a homotopy pullback of that one via some map $A\to U$.

We will be especially interested in classes of small fibrations with a univalent representation. Note that for a univalent representation $\pi:E\to U$ the classifying map $A\to U$ is unique up to homotopy.

For obtaining models of CoC, we need to assume in addition that the class of small fibrations is impredicative.

Definition 2.26**.**

Let ${\mathcal{S}}$ be a class of small fibrations in a path category with homotopy $\Pi$-types. Then ${\mathcal{S}}$ is called impredicative (or polymorphic) if it is closed under $\Pi_{f}$ for any fibration $f$.

Finally, we can also formulate Voevodsky’s resizing axiom.

Definition 2.27**.**

A class of small fibrations ${\mathcal{S}}$ satisfies (propositional) resizing if every propositional fibration belongs to ${\mathcal{S}}$.

3. The path category $\mathbb{EFF}$

In this section we will see that Martin Hyland’s effective topos [11] is the homotopy category of an interesting path category. This path category will be called $\mathbb{EFF}$ and is constructed as follows.

Objects of the category $\mathbb{EFF}$ consist of:

1. (1)

A set $A$. 2. (2)

A function $\alpha:A\to\mathbb{N}$ (sending an element $a\in A$ to its realizer). 3. (3)

For each pair of elements $a,a^{\prime}\in A$ a subset $\mathcal{A}(a,a^{\prime})$ of $\mathbb{N}$. 4. (4)

A function which computes for a realizer of $a\in A$ an element in $1_{a}\in\mathcal{A}(a,a)$. 5. (5)

A function which given realizers for $a,a^{\prime}$ and $\pi\in\mathcal{A}(a,a^{\prime})$ computes an element $\pi^{-1}\in\mathcal{A}(a^{\prime},a)$. 6. (6)

A function which given realizers for $a,a^{\prime},a^{\prime\prime}$ and $\pi\in\mathcal{A}(a,a^{\prime}),\pi^{\prime}\in\mathcal{A}(a^{\prime},a^{\prime\prime})$ computes an element $\pi^{\prime}\circ\pi\in\mathcal{A}(a,a^{\prime\prime})$.

Objects in this category will typically be denoted by $(A,\alpha,\mathcal{A})$, suppressing the data in (4-6).

Remark 3.1**.**

Just to be clear, condition (4) has to be read in the following way: there is a partial computable function, which given any element $a\in A$ computes an element in $\mathcal{A}(a,a)$ from the realizer of $a$. Conditions (5) and (6) have to be read in the same way. In fact, from a certain point onwards we will simply state a condition like (4) as: an element in $\mathcal{A}(a,a)$ can be computed from $a\in A$, where it has to be understood that the partial computable function gets the realizer of $a$ as input.

A morphism $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ in $\mathbb{EFF}$ consists of:

1. (1)

A function $f:B\to A$ such that the realizer of $f(b)$ can be computed from a realizer of $b$. 2. (2)

For each $b,b^{\prime}\in B$ a function $f_{(b,b^{\prime})}:\mathcal{B}(b,b^{\prime})\to\mathcal{A}(fb,fb^{\prime})$ such that $f_{(b,b^{\prime})}(\pi)$ can be computed from realizers for $b,b^{\prime}$ and $\pi$.

If $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is such a morphism, we will refer to Gödel numbers for the partial computable functions whose existence is demanded in (1) and (2) as trackings for the 0- and 1-cells, respectively.

Remark 3.2**.**

The right way to think about the objects and morphisms in $\mathbb{EFF}$ is as locally codiscrete bigroupoids and (non-strict) homomorphisms between them, with elements in $A$ as the 0-cells and the elements in $\mathcal{A}(a,a^{\prime})$ as the 1-cells. The definitions do not mention 2-cells, but one should really think of any two elements in $\mathcal{A}(a,a^{\prime})$ as being connected by a unique 2-cell. So one could add certain (weak) groupoid laws and demand that the morphisms preserve them, but with this intuition in mind it becomes clear that such conditions would be superfluous.

Definition 3.3**.**

Two parallel maps $f,g:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ are homotopic if there is a function computing for every realizer for $b\in B$ an element in $\mathcal{A}(fb,gb)$ (such a function is called a homotopy). A Gödel number for such a function will be called a coded homotopy. A map $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a (homotopy) equivalence if there is a morphism $g$ in the other direction (the homotopy inverse) such that both composites $fg$ and $gf$ are homotopic to the identity.

Note that the homotopy relation does not take into account the action of morphisms on 1-cells.

Definition 3.4**.**

A map $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ in $\mathbb{EFF}$ is a fibration if:

1. (1)

for any $b,a$ and $\pi:f(b)\to a$ one can effectively find $b^{\prime},\rho:b\to b^{\prime}$ such that $f(b^{\prime})=a$ and $f(\rho)=\pi$ (meaning: there are partial computable functions $\varphi$ and $\psi$ such that for any $b,a$ and $\pi:f(b)\to a$ there are $b^{\prime},\rho:b\to b^{\prime}$ with $f(b^{\prime})=a$ and $f(\rho)=\pi$ and with $\varphi$ computing the realizer of $b^{\prime}$ from $\pi$ and realizers for $a$ and $b$ and with $\psi$ computing $\rho$ from $\pi$ and realizers for $a$ and $b$). 2. (2)

for any $b,b^{\prime}\in B$, $\rho\in\mathcal{B}(b,b^{\prime})$ and $\pi\in\mathcal{A}(fb,fb^{\prime})$ one can compute $\rho^{\prime}\in\mathcal{B}(b,b^{\prime})$ with $f(\rho^{\prime})=\pi$.

Remark 3.5**.**

The second (somewhat remarkable) condition here is easy to miss, but with a bigroupoidal intuition it is clear that it should be there: it states a lifting condition for the invisible 2-cells.

Theorem 3.6**.**

With the equivalences and fibrations as defined above, $\mathbb{EFF}$ is a path category.

Proof.

We verify the axioms. It is easy to see that axioms 1 and 2 for a path category are satisfied, and because the homotopy relation is a congruence, axiom 4 follows as well.

Let us first construct pullbacks of fibrations. If $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a fibration and $g:(C,\gamma,\mathcal{C})\to(A,\alpha,\mathcal{A})$ is any map, then its pullback is:

[TABLE]

Note that one has to use the second condition in the definition of a fibration to define the bigroupoid structure on $(D,\delta,\mathcal{D})$: for instance, if $d=(c,b)\in D$, then there are 1-cells $1_{b}\in\mathcal{B}(b,b)$ and $1_{c}\in\mathcal{C}(c,c)$. We have $g(1_{c})\in\mathcal{A}(fb,fb)$, so by the second condition there is a 1-cell $\pi\in\mathcal{B}(b,b)$ with $f(\pi)=g(1_{c})$ and hence $1_{d}:=(1_{c},\pi)\in\mathcal{D}(d,d)$. For the inverses and composition there are similar arguments. In addition, the obvious projection $(D,\delta,\mathcal{D})\to(C,\gamma,\mathcal{C})$ is again a fibration (this takes care of axiom 3).

Let us now construct path objects (axiom 5). If $(A,\alpha,\mathcal{A})$ is any object, then its path object $(P,\pi,\mathcal{P})$ is:

[TABLE]

Note that the notion of homotopy determined by these path objects is precisely the homotopy relation we defined earlier.

Finally, we make the following claim: a fibration $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is trivial precisely when it has a section $s$ such that $sf$ is homotopic to the identity. Then it is easy to see that trivial fibrations have sections and are stable under pullback (axioms 6 and 7). So suppose that $g:A\to B$ is a morphism such that $H:fg\simeq 1$. Then for every $a\in A$ there is a morphism $H_{a}:fga\to a$, and the first property of a fibration allows us to find an element $sa\in B$ and a morphism $K_{a}:ga\to sa$ such that $f(K_{a})=H_{a}$. If $\pi:a\to a^{\prime}$ is a 1-cell in $A$, then we can use the fact that $g$ is a morphism to find a 1-cell $sa\to sa^{\prime}$. Using the second condition for a fibration we can choose $s(\pi):sa\to sa^{\prime}$ such that $fs(\pi)=\pi$. This constructs a section $s$ of $f$, which is homotopic to $g$. This shows that the claim about trivial fibrations is correct. ∎

Proposition 3.7**.**

The homotopy category of $\mathbb{EFF}$ is equivalent to the effective topos.

Proof.

We will assume familiarity with the effective topos ${\mathcal{E}\!f\!f}$ (see, for instance, [16]). Consider the functor

[TABLE]

sending $(A,\alpha,\mathcal{A})$ to $(A,=_{A})$ with

[TABLE]

and $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ to $F:A\times B\to{\rm Pow}(\mathbb{N})$ with

[TABLE]

This functor $P$ is full and for two parallel arrows $f,g$ in $\mathbb{EFF}$ we have $Pf=Pg$ precisely when $f$ and $g$ are homotopic. So it remains to verify that $P$ is essentially surjective.

So let $(X,=_{X})$ be an object in the effective topos. If $(A,\alpha,\mathcal{A})$ is the object in $\mathbb{EFF}$ with

[TABLE]

then $P(A,\alpha,\mathcal{A})\cong(X,=_{X})$ in ${\mathcal{E}\!f\!f}$. ∎

Remark 3.8**.**

In a metatheory without the axiom of choice, the effective topos can be defined in different ways. To prove that the functor $P$ from the previous proof is full, we need a version where functionality of a morphism $F:(B,=_{B})\to(A,=_{A})$ in ${\mathcal{E}\!f\!f}$ means that we have a function $f$ picking for every $b\in B$ and $n\in b=_{B}b$ an element $a=f(b,n)\in A$ such that from $n$ one can compute an element in $F(b,a)$.

Remark 3.9**.**

The contents from this section are very close to an earlier argument by Rosolini in [21], where he also constructs the effective topos as a homotopy quotient. The main difference is that here we obtain the effective topos as the homotopy category of a path category, which also involves finding a suitable class of fibrations; in addition, we think of the objects in the path category as degenerate bigroupoids, rather than as 2-groupoids.

Remark 3.10**.**

It also follows from [3] that the effective topos arises as a homotopy category: since the effective topos is the exact completion of the category of partitioned assemblies (see [20]), the effective topos is the homotopy category of ${\rm Ex}({\bf PAsm})$, where ${\rm Ex}$ is the homotopy exact completion from [3] and ${\bf PAsm}$ is the category of partitioned assemblies regarded as a path category by declaring every map to be a fibration and the isomorphisms to be the equivalences. The construction in this section is similar, but different: indeed, in ${\rm Ex}({\bf PAsm})$ not every fibration would be a fibration of sets, as happens for $\mathbb{EFF}$ (see Proposition 6.3 below).

4. Function spaces in $\mathbb{EFF}$

The purpose of this section is to show that $\mathbb{EFF}$ has homotopy $\Pi$-types. We will only give the constructions here, as the verifications are both straightforward and tedious.

Proposition 4.1**.**

The path category $\mathbb{EFF}$ has homotopy exponentials.

Proof.

If $B=(B,\beta,\mathcal{B})$ and $A=(A,\alpha,\mathcal{A})$ are two objects in $\mathbb{EFF}$, then the homotopy exponential $A^{B}$ can be constructed as follows:

• •

The elements of the underlying set are triples consisting of a morphism $f:B\to A$ and trackings for both its 0- and 1-cells.

• •

Realized by a code for the pair consisting of the tracking for the 0- and 1-cells.

• •

And the 1-cells between $f$ and $g$ are coded homotopies between $f$ and $g$.

This completes the construction. ∎

Remark 4.2**.**

The construction in the previous proposition does not yield a genuine exponential in $\mathbb{EFF}$, for more than one reason. First of all, there is some arbitrariness in how the evaluation morphism $A^{B}\times B\to A$ is defined on 1-cells. In addition, since trackings are not unique, there is no canonical choice for the exponential transpose.

Proposition 4.3**.**

The path category $\mathbb{EFF}$ has homotopy $\Pi$-types.

Proof.

If $(A,\alpha,\mathcal{A})$ is an object in $\mathbb{EFF}$ and $a\in A$, then this induces an arrow $a:1\to A$ sending the unique 0-cell in 1 to $a$ and the unique 1-cell in 1 to $1_{a}$. In addition, if $\pi\in\mathcal{A}(a,a^{\prime})$, then this induces a homotopy between the parallel arrows $a,a^{\prime}:1\to A$, which we will also denote by $\pi$. So it follows from Proposition 2.13 that if $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a fibration and $\pi\in\mathcal{A}(a,a^{\prime})$, then $\pi$ induces an equivalence $\Gamma^{B}_{\pi}:B_{a}\to B_{a^{\prime}}$, where $B_{a}$ and $B_{a^{\prime}}$ are the pullbacks of $f$ along $a:1\to A$ and $a^{\prime}:1\to A$, respectively.

If $g:(C,\gamma,\mathcal{C})\to(B,\beta,\mathcal{B})$ is another fibration, then the fibration

[TABLE]

is constructed as follows. We define $(D,\delta,\mathcal{D})$ by:

• •

Elements of $D$ consist of an element $a\in A$, a section $s:B_{a}\to C$ of $g$ and trackings for the 0- and 1-cells of $s$.

• •

A realizer of such an element is a coded triple consisting of the realizer of $a\in A$ and the trackings for the 0- and 1-cells of $s$.

• •

A 1-cell between $(a,s)$ and $(a^{\prime},s^{\prime})$ consists of a code for a pair containing an element $\pi:a\to a^{\prime}$ and a coded homotopy between $s^{\prime}\circ\Gamma^{B}_{\pi}$ and $\Gamma^{C}_{\pi}\circ s$.

In addition, the map $\Pi_{f}(g)$ is obtained by projecting on $a$ and $\pi$. Lengthy verifications are now in order. ∎

5. Discrete fibrations in $\mathbb{EFF}$

Within the path category $\mathbb{EFF}$ one can define an impredicative class of small fibrations given by the discrete fibrations.

Definition 5.1**.**

A fibration $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a standard discrete fibration if for elements $b,b^{\prime}\in B$ we have:

if $f(b)=f(b^{\prime})$ and $\beta(b)=\beta(b^{\prime})$, then $b=b^{\prime}$.

A fibration $f$ is discrete if $f$ can be written as $gw$ with $w$ being an equivalence and $g$ a standard discrete fibration.

Remark 5.2**.**

We could also have said that a fibration $f$ is discrete if there a standard discrete fibration $g$ and an equivalence $w$ such that $f\simeq gw$, or $fw\simeq g$, or $fw=g$. By arguments as in Proposition 2.22 one can show that all these definitions are equivalent.

Proposition 5.3**.**

The discrete fibrations form an impredicative class of small fibrations in that:

1. (1)

every isomorphism is a discrete fibration, 2. (2)

discrete fibrations are stable under homotopy pullback, 3. (3)

discrete fibrations are closed under composition, and 4. (4)

discrete fibrations are closed under $\Pi_{f}$ with $f$ a (not necessarily discrete) fibration.

Proof.

It is easy to see that every isomorphism is a standard discrete fibration, that standard discrete fibrations are stable under pullback, closed under composition and that $\Pi_{f}(g)$ as constructed in Proposition 4.3 is a standard discrete fibration whenever $f$ and $g$ are fibrations and $g$ is standard discrete. From this the statement follows. ∎

Remark 5.4**.**

1. (1)

It also follows from the construction of path objects in $\mathbb{EFF}$ as in Theorem 3.6 that $(s,t):PX\to X\times X$ is discrete for any object $X$. (In fact, we have that $P_{I}(X)\to X\times_{I}X$ is discrete for any fibration $X\to I$.) 2. (2)

One also easily verifies that $\mathbb{EFF}$ has homotopy sums (as in [3]) and that for any two discrete fibrations $f:B\to A$ and $g:D\to C$, the map $f+g:B+D\to A+C$ is again discrete, and that for any two discrete fibrations $f:B\to A$ and $g:C\to A$ the map $[f,g]:B+C\to A$ is again discrete. 3. (3)

We can call an object $A$ discrete if the map $A\to 1$ is a discrete fibration. So, basically, an object $(A,\alpha,\mathcal{A})$ is discrete if $\alpha$ is injective, or if it is homotopic to such an object (see also the definition of the category $\mathbb{DISC}$ in Section 11 below). Examples of such discrete objects are the terminal object, its finite coproducts (0,1,2), as well as the homotopy natural numbers object $(N,\nu,\mathcal{N})$ with:

[TABLE]

According to [13], Peter Freyd suggested defining discrete maps in ${\mathcal{E}\!f\!f}$ by an internal orthogonality condition. It turns out that the same is possible in $\mathbb{EFF}$. First of all, let $\mathbb{J}=(J,j,\mathcal{J})$ be the object in $\mathbb{EFF}$ with

[TABLE]

If $(A,\alpha,\mathcal{A})$ is any object in $\mathbb{EFF}$, then the homotopy exponential $A^{\mathbb{J}}$ can be computed as follows:

1. (1)

The underlying set of $A^{\mathbb{J}}$ consists of pairs of elements $(a_{0},a_{1})$ in $A$ with $\alpha(a_{0})=\alpha(a_{1})$. 2. (2)

The realizer of such a pair $(a_{0},a_{1})$ is $\alpha(a_{0})=\alpha(a_{1})$. 3. (3)

The set $\mathcal{A}((a_{0},a_{1}),(b_{0},b_{1}))$ is the intersection of $\mathcal{A}(a_{0},b_{0})$ and $\mathcal{A}(a_{1},b_{1})$.

Moreover, there is an obvious diagonal map $A\to\mathcal{A}^{\mathbb{J}}$ which copies the 0- and 1-cells. If $f:B\to A$ is any map, then this induces a (strictly) commuting square

{B}$${B^{\mathbb{J}}}$${A}$${A^{\mathbb{J}},}$$\scriptstyle{f}$$\scriptstyle{f^{\mathbb{J}}}

and if $f$ is a fibration, then so is $f^{\mathbb{J}}$.

Proposition 5.5**.**

(ZFC)* The following are equivalent for a fibration $f:B\to A$:*

1. (1)

$f$* is discrete.* 2. (2)

The square above is a homotopy pullback. 3. (3)

There is a computable function which given two elements $b_{0},b_{1}\in B$ with $f(b_{0})=f(b_{1})$ and $n=\beta(b_{0})=\beta(b_{1})$ computes an element in $\mathcal{B}(b_{0},b_{1})$ from $n$.

Proof.

(1) $\Rightarrow$ (2): If $f$ is a standard discrete fibration, then the square above is actually a genuine pullback. Since the statement in (2) is homotopy invariant, the implication follows.

(2) $\Rightarrow$ (3): The statement in (2) means that the diagonal map

[TABLE]

is an equivalence. Since we have $\pi d=1$ where $\pi$ is the projection on the first coordinate, $d$ is an equivalence precisely when $d\pi\simeq 1$. Unwinding this gives the statement in (3).

(3) $\Rightarrow$ (1): Consider the equivalence relation $\sim$ on $B$ defined by

[TABLE]

and choose $B^{\prime}$ to be a subset of $B$ which contains precisely one element from each equivalence class. The inclusion of $B^{\prime}$ in $B$ determines a map $(B^{\prime},\beta,\mathcal{B})\to(B,\beta,\mathcal{B})$ with $\beta$ and $\mathcal{B}$ on $B^{\prime}$ just being the restrictions to $B^{\prime}$. The statement in (3) implies that this map is an equivalence, while its composition with $f$ is a standard discrete fibration by construction. ∎

Remark 5.6**.**

Superficially, $\mathbb{J}$ may look a bit like an interval, but it is really rather different from the object which should be considered as the interval object in $\mathbb{EFF}$, which is $\mathbb{I}=(I,\iota,\mathcal{I})$ with

[TABLE]

Indeed, for this object we have that $\mathbb{I}\to 1$ is a trivial fibration and that $PX\simeq X^{\mathbb{I}}$, while $\mathbb{J}\to 1$ is far from a trivial fibration and we have $X\simeq PX\simeq X^{\mathbb{J}}$ only if $X$ is discrete. Since $\mathbb{J}$ is a version of $\nabla(2)$, this also shows that our work here is rather different in spirit from that in [17] and [9]. Another difference is that these papers seek to define homotopy-theoretic structures on the effective topos and do not regard it as a homotopy-theoretic quotient of some other category.

6. Propositions in $\mathbb{EFF}$

It is not clear to me if the class of discrete fibrations has a representation: indeed, this is the same problem as the one whether the class of discrete maps (defined locally) has a representation in ${\mathcal{E}\!f\!f}$, which is still open. It will be possible to show, using a standard argument, that no representation of the class of discrete fibrations in $\mathbb{EFF}$ can be univalent (see Corollary 6.4 below).

But first we will show that one can obtain a univalent representation if we restrict to the discrete propositional fibrations. As a first step in this direction, we will explicitly construct propositional truncations in $\mathbb{EFF}$.

Proposition 6.1**.**

(Existence of propositional truncation) Every fibration $f:B\to A$ factors as a map $g:B\to C$ followed by a fibration of propositions $h:C\to A$, in a “universal” way: if $g^{\prime}:B\to C^{\prime}$ and $h^{\prime}:C^{\prime}\to A$ is another such factorisation, there is a map $d:C\to C^{\prime}$ over $A$ with $dg\simeq_{A}g^{\prime}$, with the map $d$ itself being unique up to fibrewise homotopy over $A$ with this property.

Proof.

Let me just give the construction: if $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a fibration, then we define $C:=(B,\beta,\mathcal{C})$ with $\mathcal{C}(b,b^{\prime})=\mathcal{A}(fb,fb^{\prime})$. It is now easy to see that $C\to C\times_{A}C$ is an equivalence, turning $C\to A$ into a propositional fibration; the remaining verifications are also easy and left to the reader. ∎

Note that this means that, up to equivalence, any propositional fibration

[TABLE]

can be assumed to satisfy $\mathcal{B}(b,b^{\prime})=\mathcal{A}(fb,fb^{\prime})$; if $f$ is also discrete, we may even assume that $B\subseteq A\times\mathbb{N}$ with $f$ being the projection on the first and $\beta$ the projection on the second coordinate (the reason for this is that propositional truncation as in the proof of the previous proposition preserves standard discrete fibrations). This is quite helpful when trying to prove:

Theorem 6.2**.**

The class of discrete propositional fibrations in $\mathbb{EFF}$ is an impredicative class of small fibrations with a univalent representation.

Proof.

It follows from Theorem 2.23 and Proposition 5.3 that the discrete propositional fibrations form an impredicative class of small fibrations, so it remains to construct a univalent representation $\pi:E\to U$. We do this as follows:

• •

$U$ consists of subsets $X$ of $\mathbb{N}$

• •

any such $X$ is realized by 0,

• •

a 1-cell between $X$ and $Y$ in $U$ consists of realizers $r:X\to Y$ and $s:Y\to X$ (that is, $r$ is a Gödel number of a partial recursive function which is defined on every element in $X$ and which on these elements in $X$ outputs an element in $Y$; similarly for $s$),

while:

• •

$E$ consists of pairs $(X,x)$ with $X$ a subset of $\mathbb{N}$ and $x\in X$,

• •

the pair $(X,x)$ is realized by $x$,

• •

a 1-cell between $(X,x)$ and $(Y,y)$ is the same as a 1-cell between $X$ and $Y$.

This is clearly a discrete propositional fibration, and to see that it is a univalent representation, consider a map $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ and assume that $\mathcal{B}(b,b^{\prime})=\mathcal{A}(fb,fb^{\prime})$ and $B\subseteq A\times\mathbb{N}$ with $f$ being the projection on the first and $\beta$ the projection on the second coordinate. This gives rise to map $k:A\to U$ which is obtained by sending $a\in A$ to $B_{a}=\{n\in\mathbb{N}\,:\,(a,n)\in B\}$ and by sending $\pi\in\mathcal{A}(a,a^{\prime})$ to a tracking of the equivalence $\Gamma^{B}_{\pi}:B_{a}\to B_{a^{\prime}}$. The remaining verifications are left to the reader. ∎

Proposition 6.3**.**

In $\mathbb{EFF}$ every fibration is a fibration of sets.

Proof.

If $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a fibration, then we can factor $B\to B\times_{A}B$ as an equivalence $B\to P$ followed by a fibration $P\to B\times_{A}B$ with $P=(P,\pi,\mathcal{P})$ given by:

[TABLE]

Since $P\to B\times_{A}B$ is a propositional fibration, $f$ is a fibration of sets. ∎

Corollary 6.4**.**

The class of discrete fibrations in $\mathbb{EFF}$ does not have a univalent representation.

Proof.

If a class of small fibrations has a univalent representation $\pi:E\to U$ with $U$ a set, then every small object $A$ has, up to homotopy, precisely one self-equivalence. Indeed, an object with more than one self-equivalence would give rise to a map $1\to U$ which is homotopic to itself in more than one way, which is impossible if $U$ is a set.

So because $2$ is a discrete object which is equivalent to itself in two different ways, the class of discrete fibrations cannot have a univalent representation in $\mathbb{EFF}$. (This is, in fact, a well-known argument: see [15].) ∎

Finally, let us point out that, assuming the axiom of choice in the metatheory, we can prove that the discrete (propositional) fibrations satisfy resizing.

Proposition 6.5**.**

(ZFC)* In $\mathbb{EFF}$ propositional fibrations are discrete. Therefore the the discrete (propositional) fibrations in $\mathbb{EFF}$ are a class of small fibrations satisfying resizing.*

Proof.

Suppose $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is propositional, and let

[TABLE]

with $\gamma(a,n)=n$ and $\mathcal{C}((a,n),(a^{\prime},n^{\prime}))=\mathcal{A}(a,a^{\prime})$. Clearly, the projection $\pi:C\to A$ is a discrete propositional fibration. There is an obvious morphism $B\to C$ over $A$, and, using AC, there is also a morphism $C\to B$ over $A$. Since $f$ and $\pi$ are propositional, the maps going back and forth between $B$ and $C$ are each other’s homotopy inverses, so $f$ is discrete as well. ∎

7. A remark on Church’s Thesis in $\mathbb{EFF}$

A classical result in the metamathematics of constructivism says that extensional Heyting arithmetic in finite types with the axiom of choice for finite types proves the negation of Church’s Thesis (saying that any function $f:\mathbb{N}\to\mathbb{N}$ is computable) (see, for instance, [22, Theorem 9.6.8.(i)]). This means in particular that if we work in Martin-Löf Type Theory with function extensionality, then this theory will refute Church’s Thesis in the following form:

[TABLE]

However, if we use propositional truncation $\|\ldots\|$ to turn the $\Sigma$ into $\exists$ (to use the terminology from Homotopy Type Theory) and we read Church’s Thesis as:

[TABLE]

then this statement holds in $\mathbb{EFF}$. One way of seeing this starts by observing that if $P$ is the functor from the proof of Proposition 3.7 and $f:B\to A$ is a fibration in $\mathbb{EFF}$, then $Pf$ is a monomorphism precisely when $f$ is propositional (this should be clear from the description of the functor $P$, the discussion on page 67 of [16] and Proposition 6.1). Therefore for any object $A$ in $\mathbb{EFF}$, the functor $P$ sets up an order isomorphism between the subobject lattice on $PA$ in ${\mathcal{E}\!f\!f}$ and the poset reflection of the full subcategory of the slice category $\mathbb{EFF}/A$ on the propositional fibrations. This means that what holds in the logic of $\mathbb{EFF}$, when we interpret statements using propositions in the sense of Homotopy Type Theory (as explained in Sections 3.6 and 3.7 in [19]), is precisely what holds in the internal logic of ${\mathcal{E}\!f\!f}$. Since Church’s Thesis holds there, the same is true for $\mathbb{EFF}$. (See also [8], especially Section 1.3.)

8. The path category $\mathbb{EFF}_{1}$

A univalent universe containing sets like $2,\mathbb{N}$ and $\mathbb{N}\to\mathbb{N}$ must have an hlevel at least one: that is, it must at least be a groupoid. This means that if we want a category like $\mathbb{EFF}$ in which there is a univalent representation classifying discrete sets, we have to consider objects with an additional level of complexity. Indeed, for the next step we need to consider tricategories which are locally codiscrete in the sense that any two parallel 2-cells are connected by a unique 3-cell. This sounds quite complicated, but it is not too bad: we have seen that locally codiscrete bigroupoids are in a sense easier than groupoids, and in the same way locally codiscrete tricategories are simpler objects than bicategories.

We define the following category $\mathbb{EFF}_{1}$:

• •

Objects consist of:

1. (1)

A set $A$. 2. (2)

A function $\alpha:A\to\mathbb{N}$. 3. (3)

For each pair of elements $a,a^{\prime}\in A$ a set of natural numbers (1-cells) $\mathcal{A}(a,a^{\prime})$. Instead of $\pi\in\mathcal{A}(a,a^{\prime})$ we will often write $\pi:a\to a^{\prime}$. 4. (4)

For each pair of elements $\pi,\pi^{\prime}\in\mathcal{A}(a,a^{\prime})$ a set of natural numbers (2-cells) $\mathcal{A}(\pi,\pi^{\prime})$. Instead of $n\in\mathcal{A}(\pi,\pi^{\prime})$ we will often write $n:\pi\Rightarrow\pi^{\prime}$. 5. (5)

An effective function picking for each $a\in A$ an element $1_{a}\in\mathcal{A}(a,a)$. 6. (6)

An effective function picking for each $a,a^{\prime}\in A$ and $\pi\in\mathcal{A}(a,a^{\prime})$ an element $\pi^{-1}\in\mathcal{A}(a^{\prime},a)$. 7. (7)

An effective function picking for each $a,a^{\prime},a^{\prime\prime}\in A$ and $\pi\in\mathcal{A}(a,a^{\prime})$ and $\rho\in\mathcal{A}(a^{\prime},a^{\prime\prime})$ an element $\rho\circ\pi\in\mathcal{A}(a,a^{\prime\prime})$. 8. (8)

Together with 2-cells $1_{b}\circ\pi\Rightarrow\pi$ and $\pi\circ 1_{a}\Rightarrow\pi$ (which can be computed from $a,b,\pi$). 9. (9)

Together with 2-cells $\pi^{-1}\circ\pi\Rightarrow 1$ and $\pi\circ\pi^{-1}\Rightarrow 1$ (which can be computed from the same data). 10. (10)

Together with 2-cells $(\sigma\circ\rho)\circ\pi\Rightarrow\sigma\circ(\rho\circ\pi)$ (which can be computed from $\pi,\rho,\sigma$ and realizers for the domains and codomains). 11. (11)

For each $\pi\in\mathcal{A}(a,a^{\prime})$ a 2-cell $1_{\pi}\in\mathcal{A}(\pi,\pi)$ (which can be computed from $\pi$ and realizers for $a$ and $a^{\prime}$). 12. (12)

For each pair of 2-cells $n\in\mathcal{A}(\pi,\rho)$ and $m\in\mathcal{A}(\rho,\sigma)$ a 2-cell $m\circ_{1}n\in\mathcal{A}(\pi,\sigma)$ (which can be computed from $n,m,\pi,\rho,\sigma$ and their domains and codomains). 13. (13)

For each 2-cell $n\in\mathcal{A}(\pi,\rho)$ a 2-cell $n^{-1}\in\mathcal{A}(\rho,\pi)$ (which can again be computed from the relevant data). 14. (14)

For each pair of 2-cells $n\in\mathcal{A}(\pi,\rho)$ and $m\in\mathcal{A}(\pi^{\prime},\rho^{\prime})$ a 2-cell $m\circ_{0}n\in\mathcal{A}(\pi^{\prime}\circ\pi,\rho^{\prime}\circ\rho)$ (which can also be computed from the relevant data).

• •

Morphisms $f:B\to A$ consist of:

1. (1)

A function $f:B\to A$. 2. (2)

For each $b_{1},b_{2}\in B$ a function $f_{b_{1},b_{2}}:\mathcal{B}(b_{1},b_{2})\to\mathcal{A}(fb_{1},fb_{2})$, as well as 3. (3)

For each $b_{1},b_{2}\in B$ and $\pi,\rho\in\mathcal{B}(b_{1},b_{2})$ a function $f_{\pi,\rho}:\mathcal{B}(\pi,\rho)\to\mathcal{A}(f\pi,f\rho)$,

such that:

• –

A realizer for $f(b)$ can be computed from a realizer for $b$.

• –

$f_{b_{1},b_{2}}(\pi)$ can be computed from realizers for $b_{1},b_{2}$ and $\pi$.

• –

$f_{\pi,\rho}(n)$ can be computed from $n,\pi$ and $\rho$ and realizers for the domain and codomain of both $\pi$ and $\rho$.

• –

An element in $\mathcal{A}(f(1_{b}),1_{fb})$ can be computed from a realizer for $b$.

• –

An element in $\mathcal{A}(f(\rho\circ\pi),f\rho\circ f\pi)$ can be computed from realizers for $\rho,\pi$ and domains and codomains for $\rho$ and $\pi$.

Remark 8.1**.**

It may look odd to not make the last two items (the “proof terms for functoriality”) part of the identity of a morphism. However, since we lack unit and associativity laws for 2-cells in the definition of an object in $\mathbb{EFF}_{1}$ adding such would no longer result in a category.

I will continue to denote objects by $(A,\alpha,\mathcal{A})$.

Definition 8.2**.**

A morphism $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ in $\mathbb{EFF}_{1}$ is called a fibration if

• •

for every $b\in B$, $a\in A$ and $\pi\in\mathcal{A}(fb,a)$ one can effectively find elements $b^{\prime}\in B$ with $f(b^{\prime})=a$ and $\pi^{\prime}\in\mathcal{B}(b,b^{\prime})$ with $f(\pi^{\prime})=\pi$.

• •

for any $\pi,\pi^{\prime}\in\mathcal{A}(fb,fb^{\prime})$, $n\in\mathcal{A}(\pi,\pi^{\prime})$ and $\rho\in\mathcal{B}(b,b^{\prime})$ such that $f(\rho)=\pi$, one can compute $\rho^{\prime}\in\mathcal{B}(b,b^{\prime})$ and $m\in\mathcal{B}(\rho,\rho^{\prime})$ with $f(\rho^{\prime})=\pi^{\prime}$ and $f(m)=n$.

• •

given a 2-cell $m\in\mathcal{B}(\pi,\pi^{\prime})$ and a 2-cell $n\in\mathcal{A}(f\pi,f\pi^{\prime})$ one can compute a 2-cell $m^{\prime}\in\mathcal{B}(\pi,\pi^{\prime})$ with $f(m^{\prime})=n$.

Lemma 8.3**.**

Isomorphisms are fibrations, fibrations are closed under composition and the unique map to the terminal object is always a fibration.

Lemma 8.4**.**

Fibrations are stable under pullback.

Proof.

Let $f:B\to A$ be a fibration and $g:C\to A$ be arbitrary. The pullback is computed as follows:

• •

The underlying set is $D:=C\times_{A}B$.

• •

A realizer of $(c,b)$ is the pair consisting of $\gamma(c)$ and $\beta(b)$.

• •

1-cells $(c,b)\to(c^{\prime},b^{\prime})$ are pairs of 1-cells $\pi:c\to c^{\prime}$ and $\rho:b\to b^{\prime}$ with $g(\pi)=f(\rho)$.

• •

2-cells $(\pi,\rho)\Rightarrow(\pi^{\prime},\rho^{\prime})$ are pairs of 2-cells $n:\pi\Rightarrow\pi^{\prime}$ and $m:\rho\Rightarrow\rho^{\prime}$ with $g(n)=f(m)$.

The main difficulty here is not to show the universal property, but to prove that it is an object of $\mathbb{EFF}_{1}$. As in Theorem 3.6, one defines identities or composition on the $C$-component of $D$ just as in $C$, whereas for the $B$-component of $D$ one uses the fact that $f$ is a fibration to choose something in $B$ which is both homotopic to the identity or composition of $B$ and which has the same $A$-image as the object chosen in the $C$-component. ∎

Definition 8.5**.**

A homotopy between two morphisms $f,g:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ in $\mathbb{EFF}_{1}$ consists of:

1. (1)

a function $H_{1}$ picking for every $b\in B$ an element in $H_{1}(b)\in\mathcal{A}(fb,gb)$. 2. (2)

a function $H_{2}$ picking for each $\pi\in\mathcal{B}(b,b^{\prime})$ a filler $H_{2}(\pi)$ for the square

{fb}$${fb^{\prime}}$${gb}$${gb^{\prime}}$$\scriptstyle{f(\pi)}$$\scriptstyle{H_{1}(b)}$$\scriptstyle{H_{1}(b^{\prime})}$$\scriptstyle{g(\pi)}

such that:

• –

$H_{1}(b)$ can be computed from $b$.

• –

$H_{2}(\pi)$ can be computed from $b,b^{\prime}$ and $\pi$.

If $H$ is such a homotopy, I will write $H:f\simeq g$. If such a homotopy $H$ exists, I will call $f$ and $g$ homotopic and write $f\simeq g$. A coded homotopy is a pair consisting of Gödel numbers for the trackings of $H_{1}$ and $H_{2}$. If a map has a homotopy inverse, it will be called a (homotopy) equivalence.

Note that the homotopy relation does not take into account the action of morphisms on 2-cells.

Lemma 8.6**.**

The homotopy relation is a congruence and hence isomorphisms are equivalences and equivalences satisfy 6-for-2.

Lemma 8.7**.**

Every diagonal $A\to A\times A$ factors as an equivalence followed by a fibration.

Proof.

The path object on $A=(A,\alpha,\mathcal{A})$ is the object $PA=(P,\pi,\mathcal{P})$, where:

1. (1)

$P$ consists of triples $(a,b,\rho)$ with $a,b\in A$ and $\rho\in\mathcal{A}(a,b)$, 2. (2)

$\pi(a,b,\rho)$ is a triple consisting of the realizers of $a$ and $b$, as well as the natural number $\rho$, and 3. (3)

$\mathcal{P}((a,b,\rho),(a^{\prime},b^{\prime},\rho^{\prime}))$ consists of pairs of maps $\mu:a\to a^{\prime}$ and $\nu:b\to b^{\prime}$, together with a natural number $n:\nu\rho\Rightarrow\rho^{\prime}\mu$. 4. (4)

2-cells between parallel $(\mu,\nu,n)$ and $(\mu^{\prime},\nu^{\prime},n^{\prime})$ consist of pairs of 2-cells $\mu\Rightarrow\mu^{\prime}$ and $\nu\Rightarrow\nu^{\prime}$.

In addition, there is an obvious factorisation of the diagonal

{A}$${PA}$${A\times A,}$$\scriptstyle{r}$$\scriptstyle{(s,t)}

in which the first map is an equivalence and the second a fibration. ∎

If $H,K:f\simeq g$ are homotopies between $f,g:B\to A$, let us write $M:H\sim K$ for a function $M$ which computes for each $b\in B$ a 2-cell in $A$ between $H_{b}:fb\to gb$ and $K_{b}:fb\to gb$.

The following proposition is a variation on a standard result from homotopy theory and higher category theory (see [19, Theorem 4.2.3]).

Proposition 8.8**.**

Suppose $f:A\to B$ and $g:B\to A$ are morphisms with homotopies $\eta:1\simeq gf$ and $\varepsilon:fg\simeq 1$. Then we can modify $\eta$ to a homotopy $\eta^{\prime}:1\simeq gf$ for which there are

[TABLE]

(A similar statement holds for $\varepsilon$.)

Proof.

Let us first observe that if $k:A\to A$ is an endomorphism and $H:1\simeq k$ is a homotopy, then there are two homotopies $k\simeq kk$, to wit $H_{k}$ and $kH$. There is however a homotopy $M:H_{k}\sim kH$ between those. The reason is that

[TABLE]

is a naturality square and $H_{a}$ is an isomorphism.

So let us define

[TABLE]

Since $\varepsilon_{f}:fgf\simeq f$ is a natural transformation and $\eta_{a}:a\to gfa$ is a morphism, we have that

[TABLE]

commutes up to some 2-cell. Since we also have 2-cells $fgf\eta_{a}\Rightarrow f(\eta_{gfa})$ and $\varepsilon_{fgfa}\Rightarrow fg(\varepsilon_{fa})$ by the previous observation, we find $M:\varepsilon_{f}\circ f(\eta^{\prime})\sim 1_{f}$.

Dually, we have the natural transformation $\eta_{g}:g\simeq gfg$ and the 1-cell $\varepsilon_{b}:fgb\to b$ leading to a 2-cell filling:

[TABLE]

Since there is a 2-cell $gfg\varepsilon_{b}\Rightarrow g(\varepsilon_{fgb})$, we also obtain $N_{b}:g\varepsilon_{b}\circ\eta^{\prime}_{gb}\sim 1_{gb}$. ∎

Proposition 8.9**.**

A fibration $f:B\to A$ is trivial if and only if $f$ has a section $s:A\to B$ for which there are $H:1_{B}\simeq sf$ and $M:fH\sim 1_{f}$.

Proof.

If such $s,H,M$ exist, $f$ is an equivalence, so it suffices to prove the other direction.

So assume $f:B\to A$ is a fibration which is also an equivalence. This means there are maps $g:A\to B$ and homotopies $\varepsilon:fg\simeq 1$ and $\eta:1\simeq gf$. By Proposition 8.8 we may assume that there is some $N:\varepsilon_{f}\circ f(\eta)\sim 1_{f}$.

Let $a\in A$ be arbitrary. Since $\varepsilon_{a}:fga\simeq a$ and $f$ is a fibration, we can effectively find an element $sa\in B$ and a 1-cell $\tau_{a}:ga\to sa$ such that $f(\tau_{a})=\varepsilon_{a}$. In addition, if $\pi:a\to a^{\prime}$, then for $\rho^{\prime}:=\tau_{a^{\prime}}\circ g(\pi)\circ\tau_{a}^{-1}:sa\to sa^{\prime}$, we can compute a 2-cell $n:f(\rho^{\prime})\simeq\pi$, so we can determine an element $s(\pi):sa\to sa^{\prime}$ such that $fs(\pi)=\pi$ and a 2-cell:

[TABLE]

Finally, if $n:\pi\Rightarrow\pi^{\prime}$ in $A$, then $g$ yields a 2-cell $m^{\prime}:s(\pi)\Rightarrow s(\pi^{\prime})$ whose $f$-image is parallel to $n$. So we find an element $s(n):s(\pi)\Rightarrow s(\pi^{\prime})$ with $f(s(n))=n$.

From this it follows that $s$ is a morphism and $\tau$ is a homotopy between $g$ and $s$. By construction, $s$ is a section of $f$. Finally, if $H=\tau_{f}\circ\eta$, then $fH\sim f(\tau_{f})\circ f(\eta)=\varepsilon_{f}\circ f(\eta)\sim 1_{f}$, as desired. ∎

Corollary 8.10**.**

Trivial fibrations have sections and are stable under pullback along arbitrary maps.

We have shown:

Theorem 8.11**.**

With the equivalences and fibrations as defined above, the category $\mathbb{EFF}_{1}$ carries the structure of a path category.

Remark 8.12**.**

The category $\mathbb{EFF}_{1}$ is similar to one considered by Pino Rosolini in a talk at the Wessex Theory Seminar in 2010; however, his category is actually a 2-category, not a path category, and also his goals were different.

9. Function spaces and function extensionality in $\mathbb{EFF}_{1}$

We now show that $\mathbb{EFF}_{1}$ is a path category with homotopy $\Pi$-types. We will just outline the constructions and omit the lengthy verifications.

Proposition 9.1**.**

The path category $\mathbb{EFF}_{1}$ has homotopy exponentials.

Proof.

If $B=(B,\beta,\mathcal{B})$ and $A=(A,\alpha,\mathcal{A})$ are two objects, then we define the homotopy exponential $A^{B}$ to be the following:

• •

At the set level it consists of all homomorphism $f:B\to A$ including all the trackings for 0,1 and 2-cells.

• •

A realizer for $f$ consists of trackings for its 0,1 and 2-cells (but there is no reason to include the proof terms for functoriality).

• •

1-cells between $f$ and $g$ are coded homotopies $H:f\simeq g$.

• •

2-cells between $H$ and $K$ are coded homotopies $M:H\sim K$.

Checking that this works is a lengthy but routine exercise. ∎

Proposition 9.2**.**

The path category $\mathbb{EFF}_{1}$ has homotopy $\Pi$-types.

Proof.

If $(A,\alpha,\mathcal{A})$ is an object in $\mathbb{EFF}_{1}$ and $a\in A$, then there is a morphism $1\to(A,\alpha,\mathcal{A})$, which we also call $a$, sending the unique 0-cell in 1 to $a$ and the higher cells in 1 to the identity arrows on $a$ and $1_{a}$. If $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a fibration, then we will write $B_{a}$ for the object in $\mathbb{EFF}_{1}$ obtained by pulling back $f$ along $a:1\to A$. Moreover, if $\pi:a\to a^{\prime}$ is any 1-cell in $A$, then this induces a homotopy between $a,a^{\prime}:1\to A$, which we will also call $\pi$. By Proposition 2.13 this induces a homotopy equivalence $\Gamma^{B}_{\pi}:B_{a}\to B_{a^{\prime}}$. In addition, if $n:\pi\Rightarrow\pi^{\prime}$ is any 2-cell in $A$, this induces a fibrewise homotopy $\Gamma_{n}$ between $\Gamma_{\pi}$ and $\Gamma_{\pi^{\prime}}$ (see Proposition 2.12.(2)).

If $g:(C,\gamma,\mathcal{C})\to(B,\beta,\mathcal{B})$ is another fibration, we define $\Pi_{f}(g)$ to be the obvious projection to $A$ from the following object:

• •

The set consists of elements $a\in A$ together with sections $s:B_{a}\to C$ of $g$ with the required tracking data for 0,1,2-cells.

• •

A realizer for such an element consists of a realizer for $a\in A$ together with the tracking data for the 0,1,2-cells.

• •

1-cells between $(a,s)$ and $(a^{\prime},s^{\prime})$ consist of a 1-cell $\pi:a\to a^{\prime}$ as well as a coded fibrewise homotopy $H:\Gamma_{\pi}^{C}\circ s\simeq s^{\prime}\circ\Gamma^{B}_{\pi}:B_{a}\to C$.

• •

2-cells between those consist of a 2-cell $n:\pi\to\pi^{\prime}$ in $A$ together with a coded homotopy $M:(s^{\prime}\circ\Gamma_{n}^{B})\circ H\sim H^{\prime}\circ(\Gamma^{C}_{n}\circ s)$ between the homotopies $\Gamma_{\pi}^{C}\circ s\simeq s^{\prime}\circ\Gamma_{\pi^{\prime}}^{B}$.

Some very lengthy verifications are now in order. ∎

10. Discrete fibrations in $\mathbb{EFF}_{1}$

Within the path category $\mathbb{EFF}_{1}$ we can again isolate an impredicative class of small fibrations given by the discrete fibrations.

Definition 10.1**.**

A fibration $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a standard discrete fibration if for elements $b,b^{\prime}\in B$ we have:

if $f(b)=f(b^{\prime})$ and $\beta(b)=\beta(b^{\prime})$, then $b=b^{\prime}$.

A fibration $f$ is discrete if $f$ can be written as $gw$ with $w$ being an equivalence and $g$ a standard discrete fibration.

By the same argument as before, we obtain:

Proposition 10.2**.**

The discrete fibrations form an impredicative class of small fibrations in that:

1. (1)

every isomorphism is a discrete fibration, 2. (2)

discrete fibrations are stable under homotopy pullback, 3. (3)

discrete fibrations are closed under composition, and 4. (4)

discrete fibrations are closed under $\Pi_{f}$ with $f$ a (not necessarily discrete) fibration.

Also, it is possible to again characterise discrete fibrations by an orthogonality condition, in the following sense. Let $\mathbb{J}$ be the object in $\mathbb{EFF}_{1}$ with two 0-cells both having realizer [math] and only identity 1- and 2-cells, also given by the natural number 0. If $f:B\to A$ is a fibration, then the natural way of computing the homotopy exponential $A^{\mathbb{J}}$ gives rise to a (strictly) commuting square

{B}$${B^{\mathbb{J}}}$${A}$${A^{\mathbb{J}},}$$\scriptstyle{f}$$\scriptstyle{f^{\mathbb{J}}}

in which the horizontal arrows are the diagonals map and $f^{\mathbb{J}}$ is also a fibration.

Proposition 10.3**.**

(ZFC)* The following are equivalent for a fibration $f:B\to A$:*

1. (1)

$f$* is discrete.* 2. (2)

The square above is a homotopy pullback. 3. (3)

There are computable functions $\varphi$ and $\psi$ such that for any two elements $b_{0},b_{1}\in B$ with $a=f(b_{0})=f(b_{1})$ and $n=\beta(b_{0})=\beta(b_{1})$ the element $\varphi(n)$ belongs to $\mathcal{B}(b_{0},b_{1})$ and $f(\varphi(n))=1_{a}$, and such that for elements $b_{0},b_{1},c_{0},c_{1}\in B$ with $f(b_{0})=f(b_{1})$, $f(c_{0})=f(c_{1})$, $n=\beta(b_{0})=\beta(b_{1}),m=\beta(c_{0})=\beta(c_{1})$ and $\pi\in\mathcal{B}(b_{0},c_{0})\cap\mathcal{B}(b_{1},c_{1})$ we have that $\psi(n,m,\pi)$ is a 2-cell filling

{b_{0}}$${c_{0}}$${b_{1}}$${c_{1}.}$$\scriptstyle{\pi}$$\scriptstyle{\varphi(n)}$$\scriptstyle{\varphi(m)}$$\scriptstyle{\pi}

11. Propositions in $\mathbb{EFF}_{1}$

Proposition 11.1**.**

(Existence of propositional truncation) Every fibration $f:B\to A$ factors as a map $g:B\to C$ followed by a fibration of propositions $h:C\to A$, in a “universal” way: if $g^{\prime}:B\to C^{\prime}$ and $h^{\prime}:C^{\prime}\to A$ is another such factorisation, there is a map $d:C\to C^{\prime}$ over $A$ with $dg\simeq_{A}g^{\prime}$, with the map $d$ itself being unique up to fibrewise homotopy over $A$ with this property.

Proof.

Let me just give the construction: if $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a fibration, then we define $C:=(B,\beta,\mathcal{C})$ with $\mathcal{C}(b,b^{\prime})=\mathcal{A}(fb,fb^{\prime})$ and $\mathcal{C}(\pi,\pi^{\prime})=\mathcal{A}(f\pi,f\pi^{\prime})$. ∎

Note that this means that, up to equivalence, any propositional fibration

[TABLE]

can be assumed to satisfy $\mathcal{B}(b,b^{\prime})=\mathcal{A}(fb,fb^{\prime})$ and $\mathcal{B}(\pi,\pi^{\prime})=\mathcal{A}(f\pi,f\pi^{\prime})$; if $f$ is also discrete, we may also assume that $B\subseteq A\times\mathbb{N}$ with $f$ being the projection on the first and $\beta$ the projection on the second coordinate.

Proposition 11.2**.**

In $\mathbb{EFF}_{1}$ the class of discrete propositional fibrations is an impredicative class of small fibrations with a univalent representation.

Proof.

Discrete propositional fibrations are classified by the following $\pi:E\to U$:

• •

$U$ consists of subsets $A$ of $\mathbb{N}$, with every such realized by 0.

• •

$\mathcal{U}(A,B)$ consists of a pair a realizers $(r:A\to B,s:B\to A)$.

• •

Between any two such parallel 1-cells there exists a unique 2-cell.

• •

$E$ consists of pairs $(A,a)$ with $A\subseteq\mathbb{N}$ and $a\in A$, realized by $a$.

• •

$\mathcal{E}((A,a),(B,b))$ is just $\mathcal{U}(A,B)$.

• •

And, again, any two parallel 1-cells are connected by a unique 2-cell.

The projection $\pi:E\to U$ is clearly a fibration of discrete propositions. We omit the verification that it is a univalent representation. ∎

Proposition 11.3**.**

(ZFC)* In $\mathbb{EFF}_{1}$ every propositional fibration is discrete. Hence the class of discrete fibrations satisfies propositional resizing.*

Proof.

Suppose $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is propositional, and let

[TABLE]

with $\gamma(a,n)=n$ and $\mathcal{C}((a,n),(a^{\prime},n^{\prime}))=\mathcal{A}(a,a^{\prime})$, and also the 2-cells in $C$ being those in $A$. Clearly, the projection $\pi:C\to A$ is a discrete fibration of propositions. There is an obvious morphism $B\to C$ over $A$, and, using the axiom of choice, there is also a morphism $C\to B$ over $A$. Since $f$ and $\pi$ are propositional, the maps going back and forth between $B$ and $C$ are equivalences, so $f$ is discrete as well. ∎

12. Sets in $\mathbb{EFF}_{1}$

So far we have only seen properties of $\mathbb{EFF}_{1}$ which are also properties of $\mathbb{EFF}$. The main difference, however, is that the fibrations of discrete sets also form an impredicative class of small fibrations in $\mathbb{EFF}_{1}$ with a univalent representation. Before we show this, let us first show that $\mathbb{EFF}_{1}$ allows a form of 0-truncation.

Proposition 12.1**.**

(Existence of 0-truncation) Every fibration $f:B\to A$ factors as a map $g:B\to C$ followed by a fibration of sets $h:C\to A$, in a “universal” way: if $g^{\prime}:B\to C^{\prime}$ and $h^{\prime}:C^{\prime}\to A$ is another such factorisation, there is a map $d:C\to C^{\prime}$ over $A$ with $dg\simeq_{A}g^{\prime}$, with the map $d$ itself being unique up to fibrewise homotopy over $A$ with this property.

Proof.

Let me again just give the construction: if $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ is a fibration, then we define $C:=(B,\beta,\mathcal{C})$ with $\mathcal{C}(b,b^{\prime})=\mathcal{B}(b,b^{\prime})$ and $\mathcal{C}(\pi,\pi^{\prime})=\mathcal{A}(f\pi,f\pi^{\prime})$. ∎

Note that this means that any fibration of sets $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ can be assumed to satisfy $\mathcal{B}(\pi,\pi^{\prime})=\mathcal{A}(f\pi,f\pi^{\prime})$; if $f$ is also discrete, we may even assume that $B\subseteq A\times\mathbb{N}$ with $f$ being the first and $\beta$ being the second projection. This means that the category of discrete sets in $\mathbb{EFF}_{1}$ looks essentially as follows.

Its objects are:

1. (1)

A subset $A$ of $\mathbb{N}$. 2. (2)

For each pair of elements $a,a^{\prime}\in A$ a subset $\mathcal{A}(a,a^{\prime})$ of $\mathbb{N}$. 3. (3)

A function which computes for any $a\in A$ an element in $\mathcal{A}(a,a)$. 4. (4)

A function which given $a,a^{\prime}$ and $\pi\in\mathcal{A}(a,a^{\prime})$ computes an element $\pi^{-1}\in\mathcal{A}(a^{\prime}a)$. 5. (5)

A function which given $a,a^{\prime},a^{\prime\prime}\in A$ and $\pi\in\mathcal{A}(a,a^{\prime}),\pi^{\prime}\in\mathcal{A}(a^{\prime},a^{\prime\prime})$ computes an element $\pi^{\prime}\circ\pi\in\mathcal{A}(a,a^{\prime\prime})$.

We will often just write $(A,\mathcal{A})$ for these objects. A morphism $f:(B,\mathcal{B})\to(A,\mathcal{A})$ between such objects consists of:

1. (1)

A computable function $f:B\to A$. 2. (2)

For each $b,b^{\prime}\in B$ a function $f_{(b,b^{\prime})}:\mathcal{B}(b,b^{\prime})\to\mathcal{A}(fb,fb^{\prime})$ such that $f_{(b,b^{\prime})}(\pi)$ can be computed from $b,b^{\prime}$ and $\pi$.

We will denote this category by $\mathbb{DISC}$. Note that $\mathbb{DISC}$ is a small category and it is also, essentially, the subcategory of discrete objects in $\mathbb{EFF}$. In fact, because the map $PA\to A\times A$ is always discrete in $\mathbb{EFF}$, the category $\mathbb{DISC}$ inherits a path category structure from $\mathbb{EFF}$.

Theorem 12.2**.**

In $\mathbb{EFF}_{1}$ the fibrations of discrete sets form an impredicative class of small fibrations with a univalent representation.

Proof.

It follows from Proposition 10.2 and Theorem 2.23 that the fibrations of discrete sets form an impredicative class of small fibrations in $\mathbb{EFF}_{1}$. That means that it remains to construct a univalent representation $\pi:E\to U$.

• •

The elements of $U$ are the objects $(A,\mathcal{A})$ of $\mathbb{DISC}$.

• •

A realizer for any such object $(A,\mathcal{A})$ is 0.

• •

The 1-cells are coded homotopy equivalences $(f,g,H,K)$ (in the sense of $\mathbb{DISC}$ and $\mathbb{EFF}$).

• •

The 2-cells between $(f,g,H,K)$ and $(f^{\prime},g^{\prime},H^{\prime},K^{\prime})$ consist of homotopies $U:f\simeq f^{\prime}$.

In addition:

• •

The elements of $E$ are $(A,\mathcal{A},a)$, where $(A,\mathcal{A})$ is an object of $\mathbb{DISC}$ and $a\in A$.

• •

A realizer for such a thing is just $a$.

• •

The 1-cells between $(A,\mathcal{A},a)$ and $(B,\mathcal{B},b)$ consist of a coded homotopy equivalence $(f,g,H,K):(A,\mathcal{A})\to(B,\mathcal{B})$ and a 1-cell in $\mathcal{B}(fa,b)$.

• •

The 2-cells in $E$ are as in $U$.

One can easily check that the projection $\pi:E\to U$ is a fibration of discrete sets, so it remains to verify that it is a univalent representation. So let $f:(B,\beta,\mathcal{B})\to(A,\alpha,\mathcal{A})$ be a fibration of discrete sets with $\mathcal{B}(\pi,\pi^{\prime})=\mathcal{A}(f\pi,f\pi^{\prime})$, $B\subseteq A\times\mathbb{N}$, and $f$ the first and $\beta$ the second projection. Then for each $a\in A$ the fibre $B_{a}$ can be regarded as an object of $\mathbb{DISC}$ as between every two parallel 1-cells in $B$ there is a unique 2-cell. This means that the classifying map $A\to U$ can be defined on 0-cells by sending $a\in A$ to $B_{a}$. In addition, every $\pi:a\to a^{\prime}$ induces an equivalence $\Gamma^{B}_{\pi}:B_{a}\to B_{a}^{\prime}$ by Proposition 2.13, while every $n:\pi\Rightarrow\pi^{\prime}$ induces a homotopy $\Gamma^{B}_{\pi}\simeq\Gamma^{B}_{\pi^{\prime}}$ by Proposition 2.12.(2); this completes the definition of $A\to U$. The properties of transport imply that this map is a morphism in $\mathbb{EFF}_{1}$.

Finally, if $f,g:A\to U$ are two maps and $w:f^{*}\pi\to g^{*}\pi$ is an equivalence, then for each $a\in A$ the objects $f^{-1}(a)$ and $g^{-1}(a)$ are equivalent in $\mathbb{DISC}$ by $w_{a}$: using the definition of the path objects in $\mathbb{EFF}_{1}$ in Lemma 8.7, one can show that this induces a morphism $H:A\to PU$ which in turn induces an equivalence $f^{-1}(a)\to g^{-1}(a)$ which is fibrewise homotopic to $w$. In other words, $\pi$ is univalent. ∎

It is impossible to show that the class of discrete fibrations in $\mathbb{EFF}_{1}$ has a univalent representation in view of the following facts.

Proposition 12.3**.**

In $\mathbb{EFF}_{1}$ every fibration is a fibration of groupoids.

Proof.

It is clear from the description of path objects in Lemma 8.7 that $PA\to A\times A$ is always a fibration of (discrete) sets. Since the description of fibrewise path objects $P_{I}(A)\to A\times_{I}A$ for fibrations $A\to I$ is similar, we see that every fibration is a fibration of groupoids. ∎

Corollary 12.4**.**

The class of discrete fibrations in $\mathbb{EFF}_{1}$ does not have a univalent representation.

Proof.

If a class of small fibrations has a univalent representation $\pi:E\to U$ with $U$ a groupoid, then for every small object $A$, self-equivalence $w:A\simeq A$ and homotopies $H,K:1\simeq w$, we must have that $H\sim K$. For otherwise there would be a loop in the universe which is homotopic to the constant loop in two different ways, which is impossible if the universe is a groupoid.

So consider the following discrete object $(A,\alpha,\mathcal{A})$ in $\mathbb{EFF}_{1}$:

• •

The set $A$ of 0-cells is $\{0,1\}$.

• •

The map $\alpha$ is the identity.

• •

The set $\mathcal{A}(i,j)=\{0,1\}$ for all 0-cells $i,j$.

• •

The set $\mathcal{A}(\pi,\pi^{\prime})$ for parallel 1-cells $\pi,\pi^{\prime}$ is $\{0\}$ if $\pi=\pi^{\prime}$ and empty otherwise.

• •

The identity 1- and 2-cells are 0.

• •

Composition of 1-cells is addition modulo 2.

This object has an endomorphism $w:A\to A$ which is obtained by sending 0-cells to themselves and 1-cells $\pi\in\mathcal{A}(i,j)$ to themselves if $i=j$ and to $1-\pi$ if $i\not=j$; because $w^{2}=1$, the map $w$ is an isomorphism and hence a self-equivalence.

There are two homotopies $H,K:1\simeq w$ obtained by putting $H_{i}=i:i\to i$ and $K_{i}=1-i:i\to i$. These homotopies $H$ and $K$ are not homotopic to each other because $A$ only has identity 2-cells and the homotopies $H$ and $K$ are distinct. ∎

Remark 12.5**.**

It is unclear to me if the class of discrete fibrations in $\mathbb{EFF}_{1}$ has a non-univalent representation.

13. Conclusion and directions for future research

The contents of this paper can be summarised by the following two theorems:

Theorem 13.1**.**

There exists a path category with homotopy $\Pi$-types $\mathbb{EFF}$ whose homotopy category is equivalent to the effective topos. Within this path category one can identify a class of small fibrations (viz., the ones which are discrete and propositional) which is impredicative and has a univalent representation. In addition, propositional resizing holds.

Theorem 13.2**.**

There exists a path category with homotopy $\Pi$-types $\mathbb{EFF}_{1}$ in which there is a class of small fibrations (viz., the fibrations of discrete sets) which is impredicative and has a univalent representation. In addition, propositional resizing holds.

It is not entirely clear when two path categories should be considered equivalent, but one would expect that if one had such a notion, the path category of sets in $\mathbb{EFF}_{1}$ would be equivalent as a path category to $\mathbb{EFF}=\mathbb{EFF}_{0}$. Indeed, as I already suggested in the introduction, one would expect that there would be path categories $\mathbb{EFF}_{n}$ such that the $n$-types in $\mathbb{EFF}_{n+1}$ would be equivalent as a path category to $\mathbb{EFF}_{n}$. Ultimately, there should be a path category $\mathbb{EFF}_{\infty}$ such that each $\mathbb{EFF}_{n}$ is equivalent to the path category of $n$-types in $\mathbb{EFF}_{\infty}$. For this path category $\mathbb{EFF}_{\infty}$ one should have the following:

Conjecture 13.3**.**

There exists a path category with homotopy $\Pi$-types $\mathbb{EFF}_{\infty}$ in which there is a class of small fibrations, the discrete ones, which is impredicative and has a univalent representation. These discrete fibrations can be defined using an internal orthogonality condition and for these discrete fibrations propositional resizing holds.

In addition, the following problems remain.

**Models of CoC and coherence issues: **

The categories $\mathbb{EFF}$ and $\mathbb{EFF}_{1}$ come close to being models of some version of CoC, but fall short in two ways. First of all, the version of CoC we have in mind is one in which all definitional equalities have been replaced by propositional ones. It remains to make this more precise and in particular write down a syntax for this version of CoC. Secondly, we should address coherence issues and formulate these categories as categories with families [7, 10] or some other standard notion of model of type theory.

**Choice issues: **

We have used the axiom of choice in the proof of propositional resizing and in the proof of the fact that the discrete fibrations can be characterised by an internal orthogonality condition (see Proposition 5.5 and Proposition 6.5 for the case of $\mathbb{EFF}$). It seems likely that both applications of the axiom of choice can be eliminated by changing the definition of $\mathbb{EFF}$ slightly. The idea would be to say that every object $(A,\alpha,\mathcal{A})$ in $\mathbb{EFF}$ should also come equipped with a section of the surjection $\alpha:A\to{\rm Im}(\alpha)$, but that morphisms are as before (so they do not have to preserve this additional structure). For the fibres of fibrations one should do something similar, so it might be that this would work best in the setting of categories with families. We leave the question whether this would give us a choice-free model of CoC to future work.