7
$\begingroup$

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.

$\endgroup$

1 Answer 1

4
$\begingroup$

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)

$\endgroup$
10
  • $\begingroup$ Thank you so much for taking the time to write down such a detailed answer and thank you also for sharing your formalized solution! The use of the other results in section 4.8 and specifically the equivalence $\chi$, giving the uniqueness of classifying maps, could be expected I think, since that's where univalence flows in. I must admit I was hoping for a more ``categorical solution'' which makes use also of the pullback (probably because I feel more comfortable with category theory) but your neat solution definitely answers the question! $\endgroup$
    – TJM
    Jan 24 at 14:50
  • $\begingroup$ As a followup, why does function extensionality hold in every ($\infty$,1)-topos? Thinking of it as the analogue of the well-pointedness axiom in (ordinary) topos theory, I would have expected it to be something that must be imposed as an additional axiom also in the ($\infty$,1)-world. $\endgroup$
    – TJM
    Jan 24 at 14:50
  • 1
    $\begingroup$ Isn't what you're calling 4.8.2 actually 4.8.3? $\endgroup$ Jan 24 at 16:14
  • 1
    $\begingroup$ @TJM Function extensionality has nothing to do with well-pointedness. Categorically, function extensionality is the statement that the (locally) cartesian-closed exponential objects satisfy a full universal property rather than just a weak one. Well-pointedness is undetectable to the internal logic, it's more about the interaction of internal and external properties. $\endgroup$ Jan 24 at 19:07
  • 1
    $\begingroup$ @AméliaLiao Somewhat belated, thank you too for your comment with the links! $\endgroup$
    – TJM
    Jan 26 at 22:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.