Object Classifier implies Univalence in Type Theory?

Question

There is a correspondence between univalence in Type Theory and object classifiers in $\infty$-toposes. This, for example, is suggested in the article Univalent Foundations for Mathematics on nlab.

Section 4.8 of the HoTT book describes how univalent universes $\mathcal U$ give rise to object classifiers in Type Theory $$\require{AMScd} \begin{CD} A @>{\theta_f}>> \mathcal U_\bullet\\ @V{f}VV @VV{\texttt{pr}}V \\ B @>>{\chi_f}> \mathcal U \end{CD}$$ where $ \mathcal U_\bullet :\equiv \sum_{A \, : \, \mathcal U} A $ is the type of pointed types and $ \texttt{pr} $ the corresponding projection, $ A : \mathcal U $ and \begin{equation} \chi_f(b) \equiv \texttt{fib}_f(b), \qquad \theta_f(a) \equiv \big( \texttt{fib}_f(f \, a), (a,\texttt{refl}_{f \,a}) \big). \end{equation}

Does the other direction also hold? Is it possible to show that a universe $ \mathcal U$ in Martin-Löf Type Theory is univalent, assuming that the canonical projection $ \texttt{pr} : \sum_{A\, : \, \mathcal U} A \to \mathcal U $ is an object classifier in the sense of section 4.8 of the HoTT book?

A naive idea I have considered is to put the function $ \texttt{idtoeqv} : (A=_{\mathcal U} B) \to (A \simeq B) $, or $ \texttt{i} $ for short, on the left of the pullback,* as in the following diagram $$\require{AMScd} \begin{CD} A=_{\mathcal U} B @>>> \mathcal U_\bullet\\ @V{\texttt{i}}VV @VV{\texttt{pr}}V \\ A \simeq B @>>{\chi_\texttt{i}}> \mathcal U \end{CD}$$ hoping that $ \chi_{\texttt{i}} $ factors through $ \texttt{pr}$, so that the universal property of the pullback will produce a candidate for the quasi-inverse. This approach failed however, since given an $ f : A \simeq B$, I must already have a path $ p : A =_{\mathcal U} B $ in the fiber $\texttt{fib}_{\texttt{i}}(f)$ at hand, in order to define the factorization $ (A \simeq B) \to \mathcal U_\bullet$ in the first place.

*Here I'm assuming that the universe is closed under identity types, i.e. $ A =_{\mathcal U} B : \mathcal U $. It sounds like a desirable property for a universe to have, but I don't know if this is included in Homotopy Type Theory or if this leads to any problems.

Answer 1

Since you said "object classifier in the sense of section 4.8", I'm going to assume that the other lemmas in that section - in particular, lemma 4.8.3, are fair game. It should be possible to recover it from 4.8.4, but I haven't formalised that.

As far as I can tell, it's not possible to prove univalence from just the lemmas in this section; You also appear need propositional extensionality and function extensionality. Using these three assumptions, we can establish univalence as follows:

We have a function $\chi : (\sum_{(A : \mathcal{U})} (A \to B)) \to B \to \mathcal{U}$, which by lemma 4.8.3 is an equivalence. Recall that this function is $\lambda\ (E , f)\ x. \mathrm{fibre}_f(x)$. We can use this result to conclude that "maps with $P$-fibres", for our choice of $P$, are classified by the object $\sum_{(A : \mathcal U)}P(A)$. For this, let $P : \mathcal{U} \to \mathcal{U}$ be a predicate on types, and observe that lemma 4.8.3 + some pair munging gives us the following chain of equivalences

(Σ[ A ∈ Type _ ] Σ[ f ∈ (A → B) ] ((x : B) → P (fibre f x)))       ≃
(Σ[ (x , f) ∈ Σ[ A ∈ Type _ ] (A → B) ] ((x : B) → P (fibre f x))) ≃
(Σ[ A ∈ (B → Type _) ] ((x : B) → P (A x)))                        ≃
(B → Σ P)

Where we go from the first line to the second by rearranging pairs (associativity of $\sum$; exercise 2.10), from the second to the third using our equivalence $\chi$ on the index type (exercise 2.17), and the last uses the "type-theoretic axiom of choice", theorem 2.15.7, applied backwards.

We know that the equivalences are precisely the maps with contractible fibres (theorem 4.4.5); We will show that the type $\sum_{(A : \mathcal{U})} A \simeq B$ is contractible. Using the equivalence above, and the closure of h-levels under retracts, we can reduce this to showing

$$ \mathrm{isContr}\ (B \to \sum_{(A : \mathcal{U})} \mathrm{isContr}(A)) $$

By our assumption of function extensionality, it suffices to show that the codomain type is contractible; Since a contractible type is an inhabited proposition, it suffices to show that it is a proposition (it is inhabited by the unit type). For this, let $(A, c)$ and $(B, c')$ be two contractible types (and the witnesses that they are contractible): we have maps $A \to B$ (resp $B \to A$) sending everything to the centre of contraction of $B$ (resp $A$), so by propositional extensionality, $A = B$; Since $\mathrm{isContr}$ is a family of propositions, the claimed result follows.

We now know that $\sum_{(A : \mathcal{U})} A \simeq B$ is contractible, and since the map $(-)^{-1} : (A \simeq B) \to (B \simeq A)$ is an equivalence, so is $\sum_{(A : \mathcal{U})} B \simeq A$; To show that $\mathrm{pathToEquiv}$ is an equivalence, it suffices to show it induces an equivalence of total spaces (theorem 4.7.6), i.e. we need

$$ \left(\sum_{(A : \mathcal{U})} (B \simeq A)\right)\simeq \left(\sum_{(A : \mathcal{U})} (B = A)\right) $$

But we've just established that the left-hand-side type is contractible, and the right-hand type is contractible by path induction, so we are done. I do not know if it's possible to show univalence from the existence of an object classifier without the use of function and propositional extensionality, but I suspect that it isn't. As for the adequacy of this proof, funext and propext hold in any $(\infty,1)$-topos.

Apologies for the use of monospaced text, I couldn't get array to render properly. I've also formalised this argument in Cubical Agda, avoiding the fact that univalence is a theorem. In particular, the file begins with a postulate for lemma 4.8.3, and a postulate of propositional extensionality: You can check it out here.

Quick edit: While universe types aren't directly closed under paths, they are essentially closed under paths, in that while $A =_\mathcal{U} B$ is a large type, it is equivalent to the small $A \simeq B$. (I can't comment, my account is new)

Answer 2

As an alternative answer, if, instead of assuming the statement of theorem 4.8.3, we assume that $\mathcal U$ is an object classifier in the sense of higher topos theory (that is, that the projection $\mathcal U_\bullet \to \mathcal U$ is a terminal object in the category of arrows and pullback squares), then we can show that $\mathcal U$ is a univalent universe without relying on propositional extensionality.

The key observation is that a pullback square like

$$\require{AMScd} \begin{CD} A @>{\theta}>> \mathcal U_\bullet\\ @V{!}VV \lrcorner @VV{\texttt{pr}}V \\ 1 @>>{'B'}> \mathcal U \end{CD}$$

is equivalent to an equivalence $A \simeq B$, and the top map $\theta$ is entirely determined by the equivalence. Thus, since by assumption there is a contractible space of such pullback squares, the space of types equivalent to $A$ is also contractible, which is equivalent to univalence by the standard theory of identity systems.

This argument is formalised in Cubical Agda here, and does make use of function extensionality.