### Segal-Completeness and Univalence

#### Posted by Urs Schreiber

Here is a charming statement:

*Univalence in homotopy type theory is a special case of the Segal-completeness condition in internal (∞,1)-category theory .*

Do you see it? Once you know what these terms mean this is pretty obvious, once stated. But it seems not to have been stated before.

I now briefly spell this out and give further pointers. This might be the beginning of a nice story. I am posting this here in the hope of discussing it a bit more.

Consider some ambient (∞,1)-topos and inside it an internal (∞,1)-category, hence a complete Segal space object $X_\bullet$. Its 1-skeleton, on which I will focus attention here, looks as follows (in this and the following formulas I display on the left the syntax and on the right its semantics, see *HoTT methods for homotopy theorists* if you are a homotopy theorist and need more background):

the object of morphisms $X_1$ sits by the source-and-target map $(d_0,d_1)$ over the object of objects $X_0$

$[x,y : X_0 \vdash X_1(x,y) : Type] \;\;\;\;\;\;\;\;\;\;\; \left[ \array{ X_1 \\ \downarrow^{\mathrlap{(d_0, d_1)}} \\ X_0 \times X_0 } \;\;\;\;\; \right]$

and the identity-assigning map $s_0$ is a diagonal section

$[ x : X_0 \vdash s_0(x) : X_1(x,x)] \;\;\;\;\;\;\;\;\; \left[ \array{ X_0 &&\stackrel{s_0}{\to}&& X_1 \\ & {}_{\mathllap{\Delta}}\searrow && \swarrow_{\mathrlap{(d_0,d_1)}} \\ && X_0 \times X_0 } \right] \,.$

Syntactically, the recursion principle / simple elimination rule for the inductive identity types, and semantically the (acyclic cofibrations $\perp$ fibrations)-weak factorization system, says that this section factors through the identity type $[x,y : X_0 \vdash (x = y) : Type]$ (syntactically) respectively the path space object $X_0^I\to X_0 \times X_0$ (semantically):

$[ x,y : X_0 \vdash \hat s_0(x,y) : (x = y) \to X_1(x,y)] \;\;\;\;\;\;\; \left[ \array{ X_0 &\stackrel{s_0}{\to}& X_1 \\ \downarrow &\nearrow_{\mathrlap{\hat s_0}}& \downarrow \\ X_0^I &\to& X_0 \times X_0 } \right] \,.$

Now, Segal-completeness of $X_\bullet$ is the statement that this $\hat s_0$ exhibits the inclusion of the core, hence of those morphisms $f \in X_1$ that are equivalences under the composition operation of $X_\bullet$.

Specifically, consider the case that $X_\bullet$ is the *universal* small internal category object, equivalently the small reflection of the ambient $(\infty,1)$-topos into itself, equivalently the classfier of the small codomain fibration, equivalently its stack semantics, or whatever you want to call it, that whose 1-skeleton is

$\array{ [A,B : Type \vdash A \to B : Type] \\ {}^{\mathllap{d_0}}\downarrow \uparrow^{\mathrlap{s_0}} \downarrow^{\mathrlap{d_1}} \\ Type } \,,$

where “$Type$” denotes the small universe / small object classifier.

Then the Segal-completeness condition of this internal category object is the univalence condition on $\widetilde Type \to Type$.

Posted at May 18, 2012 11:12 PM UTC
## Re: Segal-completeness and univalence

I’ve certainly noticed this, though I don’t know if I’ve ever pointed it out to anyone.

I think of it like this: an infinity-topos $E$ is a presentable (infinity,1)-category which “contains” an internal model of itself, in the sense that there is a complete segal object $X_\bullet$ in $E$ such that $map(B,X_\bullet)$ is the complete segal space modelling $E/B$. (“Contains” carries the usual set-theoretic difficulties.)

In particular, an infinity-topos “contains” an “object classifier” $Y\to X_0$ (I think this is what you mean by the classifier of the small codomain fibration, yes?), so that a map $f:B\to X_0$ classifies the object $Y\times_{X_0} B\to B$ in $E/B$. (So you can think of this as a higher analogue of a “subobject classifier”.)

As you point out: any infinity-topos satisfies univalence, which is exactly the completeness part of “$X_\bullet$ is a complete segal space”.

I think this means that any infinity-topos satisfies the axioms HoTT. Is that right? (Or should I say, “is a model of HoTT”?)

Question: Does this go the other way around. Is every (model of a) HoTT an infinity-topos. It looks like you are assuming this in what you’ve written, but is this known?

More concretely, under reasonable hypotheses on an infinity-1 category $E$ (say it is presentable), does “univalence” imply that $E$ is an infinity-topos? (I.e., does “univalence” imply “descent”?) I suspect perhaps not, but I don’t really know.