Segal-Completeness and Univalence

May 18, 2012

Posted by Urs Schreiber

$MathML-enabled post (click for more details).$

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

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2529

21 Comments & 0 Trackbacks

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

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.

Posted by: Charles Rezk on May 19, 2012 3:58 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

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

Okay, great! It is really obvious in a way. What stopped me from seeing it earlier is that I had not been thinking about “path induction” in HoTT in a good way until recently. But of course that, too, is in itself very simple.

And for bystanders who don’t know about complete Segal spaces I should maybe point out that what I call “Segal-completeness” here, because you called it so, would better be called Rezk completeness.

I think this is what you mean by the classifier of the small codomain fibration, yes?

Yes. I was just trying to make the distinction between the classifier for the core of the small codomain fibration (“small” referring to: consisting only of relatively $\kappa$ -compact morphisms for some regular cardinal $\kappa$ , or otherwise bounded in size), which is the groupoid object called the object classifier, and the thing that actually classifies the full small codomain fibration, including its non-invertible morphisms. This is a category object that is the “small model of $E$ in itself”.

There should really be a standard unambiguous term for this, since its such a fundamental concept. But it seems such a term does not quite exist. Maybe “the self-indexing” is the closest generally-understood term that there is, but unfortunately this invokes the codomain fibration itself more than the category object that classifies it.

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

So this is certainly expected to be true, and most of it is known to be true, but there remains one little gap. Naturally Mike Shulman is the local expert to say more about this, but until he comes back online, maybe I can say a bit:

One thing that has been fully established is that every presentable and locally cartesian closed $(\infty,1)$ -category models all of HoTT except possibly univalence and higher inductive types. This is precisely what one expects.

What makes the proof that every $(\infty,1)$ -topos models univalence in the HoTT sense non-immediate is – as far as I understand – that in HoTT the statement about univalence is much stricter than its evident formulation in the $(\infty,1)$ -topos. The HoTT language is strictly speaking a formal way of speaking about a suitable model category presentation of the $(\infty,1)$ -topos, and the problem is to verify that a very specific model category theoretic construction exhibits the Segal-completeness condition.

Recently Mike has shown this here for presheaf $\infty$ -toposes over inverse diagrams, and a generalization of this for slightly more general diagrams is in the making. He has also indicated an argument how to induce from univalence in a presehaf $\infty$ -topos that in any of its sheaf localizations.

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?

Again, I think everybody expects this to be true – if by $\infty$ -topos one means a suitable notion of elementary ∞-topos (because HoTT does not know about the (what do you call them?) Giraud-Rezk-Lurie axioms for $\infty$ -sheaf $\infty$ -toposes). But this has not been formally established yet.

Posted by: Urs Schreiber on May 19, 2012 5:16 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

I think this means that any infinity-topos satisfies the axioms [of] HoTT. Is that right?

As Urs says, the problem is exactly one of coherence/strictification. Substitution of terms in type theory is strictly associative and unital, and so we must use some model of an $(\infty,1)$ -topos which has an underlying strict 1-category. Then a dependent type

$x:A \;\vdash\; P(x) \; type$

in homotopy type theory must be modeled by some sort of morphism $P\to A$ . In order to be able to model the identity types correctly, these morphisms must be the right class of a weak factorization system on the 1-category, i.e. “fibrations” of a sort. Now if we have a term $y:B \;\vdash\; f(y):A$ , representing a morphism $f : B\to A$ , then the substituted dependent type

$y:B \;\vdash\; P(f(x))\; type$

will be modeled by the pullback of $P\to A$ along $f$ . It must be a strict 1-categorical pullback in order that terms belonging to these dependent types are typeable. But this sort of substitution is also strictly associative, so we need some way to represent pullbacks of fibrations which is strictly associative, i.e. $g^\ast (f^\ast P) = (f g)^\ast P$ , not just canonically isomorphic.

And so on.

These sorts of problems already arise in the modeling of ordinary extensional dependent type theory by locally cartesian closed 1-categories. Martin Hofmann showed how to deal with it there by passing to a certain split replacement of the codomain fibration.

In homotopy type theory, we can try to use a similar trick, and it comes close to working. Michael Warren worked this out in his thesis. However, my current understanding is that it doesn’t quite fully solve the coherence problem in general, because of problems with the identity types. That is, the assertion

…every presentable and locally cartesian closed (∞,1)-category models all of HoTT except possibly univalence and higher inductive types

which I have made myself, is actually not quite true.

Specifically, if we have a locally cartesian closed, right proper, simplicial model category in which the cofibrations are the monomorphisms, then we can model sum and product types directly using a split replacement of the sub-fibration of the codomain fibration on the (model-categorical) fibrations. And we can model the identity types as simplicial path-objects which are pullback-stable up to isomorphism, hence can be made strictly pullback-stable in the splitting of the codomain fibration. And Denis-Charles Cisinski has recently argued that any locally presentable, locally cartesian closed $(\infty,1)$ -category can be presented by such a model category.

However, I don’t think Michael Warren found any general way to make the eliminator of the identity types be strictly pullback-stable. I think this is why he calls what he gets a “quasi-model” of identity types. He, and later Richard Garner and Benno van den Berg, studied when a model category can be given extra structure that makes this possible, but I believe their results are all very limiting; they require the path-objects to be internal categories or to be generated by a cocategory interval.

I feel that every $(\infty,1)$ -topos ought to be a model of a sort of “HoTT with fully explicit substitution.” But I don’t know anything about type theories with explicit substition. I do know they are quite a pain to work with! Both in terms of doing concrete things, and probably in terms of constructing models too. So there would probably be a nontrivial amount of coherence work involved as well in actually proving that this works, in addition to it being much more work to do anything with.

Now there is one way to get coherence for the eliminator of the identity types as well. This is due to Voevodsky, and it simultaneously solves the problem of how to model a universe type (which of course we need in order to even state the univalence axiom). The idea is to find an object in the model category which “represents an object classifier” and strictly represents fibrations, i.e. every fibration (of a certain bounded size) is a strict pullback of some given universal fibration.

Now we model type theory by interpreting a dependent type $x:A \;\vdash\; P(x)\;type$ not directly by a fibration over $A$ , but by a map from $A$ into the universe object $U$ which classifies it. Then we can get coherence for all type-forming operations and eliminators by constructing them once in the universal case, choosing classifying maps for those constructions, and then operating on other classifying maps by mere composition.

This is explained in somewhat more detail at the beginning of this paper.

Currently, we don’t know how to construct strict models for object classifiers in models of all $(\infty,1)$ -toposes. Voevodsky did it in simplicial sets, which of course models $\infty Gpd$ . My preprint that I just cited builds to diagrams of simplicial sets on inverse categories. Currently I think I can generalize this slightly, but not very much. In all of these cases, the universe objects that we get do satisfy the univalence axiom.

I have various ideas for ways to bootstrap ourselves up to all $(\infty,1)$ -toposes, but none of them have panned out just yet (despite a provisional claim I made to that effect in Swansea — I discovered afterwards a flaw in the approach I was taking at that time). I expect other people are thinking about this as well. If no one has solved it on their own by this fall, then I bet that over the course of the IAS special year we’ll work something out.

Is every (model of) HoTT an infinity-topos?

Well, as you know very well, a locally presentable $(\infty,1)$ -category is an $(\infty,1)$ -topos as soon as it is locally cartesian closed and has object classifiers of $\kappa$ -compact objects for $\kappa \gg 0$ . (Higher Topos Theory 6.1.6.8, attributed to you.) An $(\infty,1)$ -category which models HoTT is definitely lccc, so the question is whether univalent universes give you object classifiers.

I believe a univalent universe is certainly “an object classifier” in some elementary sense, in that the map

$Hom(X,U) \to E/X$

is an equivalence onto the core of some full subcategory of $E/X$ . But since HoTT is entirely “elementary”, there seems no reason that this full subcategory should consist of the relatively $\kappa$ -compact morphisms for any $\kappa$ . We can say that the morphisms classified by $U$ are closed under various operations, like composition and dependent product. (In fact, I believe that these closure properties would force $\kappa$ to be not only regular but inaccessible.)

In the particular models that we have constructed, though, I believe that the univalent universes do model object classifiers of relatively $\kappa$ -compact morphisms. By construction, Voevodsky’s univalent universe in simplicial sets, and those that I derived from it, strictly classify fibrations all of whose whose fibers are of size $\lt\kappa$ . And Jacob claims that for sufficiently large $\kappa$ , being $\kappa$ -small in a model category is equivalent to being $\kappa$ -compact in the underlying $(\infty,1)$ -category.

Posted by: Mike Shulman on May 20, 2012 7:16 AM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

You write:

Currently, we don’t know how to construct strict models for object classifiers in models of all (∞,1)-toposes.
Voevodsky did it in simplicial sets, which of course models ∞Gpd. My preprint that I just cited builds to diagrams of simplicial sets on inverse categories. Currently I think I can generalize this slightly, but not very much. In all of these cases, the universe objects that we get do satisfy the univalence axiom.

Let me throw a thought out, though it probably doesn’t do exactly what you want.

In a category with weak equivalences, say that a morphism $f$ is sharp if base change along $f$ carries weak equivalences to weak equivalences. Thus, in a right proper model category all model-category fibrations are sharp, but sharpness is a much weaker property than being a fibration.

You can show that in any Joyal-Jardine model category of simplicial sheaves, the condition that $f\colon X\to Y$ is sharp is local in the codomain $Y$ . (I proved this in arXiv:math/9811038, though in retrospect I worked much harder than I needed to. I think the proof should go through for more general $\infty$ -topos model structures.)

Therefore, in this setting, you can build a universal sharp map $\overline{U}\to U$ , and it should not be too hard to build a strict model of this map. The proposal is that the universal sharp map also models the object classifier. This is certainly true in simplicial sets; I don’t have a general proof.

Sharp maps don’t participate in a weak factorization system, although they contain the fibrations (which do).

Posted by: Charles Rezk on May 20, 2012 5:03 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

Thanks for that thought! It’s certainly an intriguing direction. I’m a little confused about what you mean by “local” — is that in the 1-category sense or in the $(\infty,1)$ -category sense? Surely it can’t be the latter, because sharpness is a purely model-categorical notion. For the same reason, I don’t understand what it would mean to have a universal sharp map other than in terms of a strict model. However, the statements I see in the paper you linked to are talking about homotopy colimits, so 1-categorical locality doesn’t seem right either.

(Why “sharp”?)

Anyway, as far as I can tell, we really do need to consider only fibrations for purposes of modeling type theory, because the interpretation of identity types seems to require a weak factorization system. Whatever class of “display maps” we take as our representatives of dependent types, the type-formation for identity types has to factor the diagonal as $A\to P A \to A\times A$ , where $P A \to A\times A$ is a display map (since the identity type $Id_A(x,y)$ depends on $x:A, y:A$ ) and $A\to P A$ has the left lifting property with respect to display maps (this is the dependent eliminator — the induction principle — for identity types). That’s most of the way to a weak factorization system already, and Gambino+Garner showed that you can get the rest of the way from there.

Posted by: Mike Shulman on May 21, 2012 7:20 AM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

“Local” is in the 1-category sense. In a Joyal-Jardine model category, if $f:X\to Y$ is a map, and $g:Y'\to Y$ is an epimorphism, then $f$ is sharp iff the base change $f':X'\to Y'$ along $g$ is sharp.

Sharpness isn’t exactly a model category notion. It’s a category and weak equivalences notion.

“Sharp” because its dual to “flat”; Mike Hopkins had started using flat for the dual notion in a model category.

Barwick and Kan have taken to calling these by the heart-attack inducing name “fibrillations”, instead of “sharp”.

Posted by: Charles Rezk on May 21, 2012 3:39 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

By coincidence, today I was looking at this paper, and noticed that what you call a “sharp map” is there called a “right proper map” (Def. 1.8.3, page 18).

Posted by: Mike Shulman on May 22, 2012 6:29 AM | Permalink | Reply to this

Re: Segal-completeness and univalence

Mike believes that a univalent universe is certainly “an object classifier” in some elementary sense…

I just proved the following in Coq:
—
Variable A:Type.
Definition Fam A:=sigT (fun I:Type => I->A).

Definition p2f: (A->Type)-> Fam A:=
fun Q => ( (sigT Q) ; pr1).
Definition f2p: Fam A -> (A->Type):=
fun F => let (I, f) := F in (fun a => (hfiber f a)).

Hypothesis fs : funext_statement.
Hypothesis univalence : univalence_statement.

Theorem PowisoFam: is_hiso p2f.
—

This seems to be an elementary/internal way of stating that Type is an object classifier, but perhaps it is not the only way.

Bas

Posted by: Bas Spitters on May 21, 2012 12:49 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

Nice! That seems like a version that is “extra-internalized”, in that even the $\infty$ -groupoids $Core(E/A)$ and $U^A$ are internal — analogous to the isomorphism $Z^{X\times Y} \cong (Z^Y)^X$ in a ccc that we can derive by Yoneda from the defining external isomorphism of sets $Hom(X\times Y,Z)\cong Hom(X,Z^Y)$ .

Posted by: Mike Shulman on May 21, 2012 6:12 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

Regarding the question of constructing models out of quasi-models, Peter Lumsdaine and I have recently found a way to turn any “quasi-model” of type theory which satisfies a couple of very natural conditions into a strict model of type theory (without having to use universes). We will post a preprint with the details of this result on the arXiv fairly soon and I would be happy to send copies of it to anyone who is interested.

Posted by: Michael Warren on May 21, 2012 11:41 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

Ooh, mememe!

Posted by: Mike Shulman on May 22, 2012 6:12 AM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

This might be the beginning of a nice story.

How might the next chapter go?

…the small reflection of the ambient $(\infty,1)$ -topos into itself

is beginning to sound like Leibniz’s God as monad, perfectly mirroring all the other monads.

Posted by: David Corfield on May 20, 2012 4:10 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

This might be the beginning of a nice story.

How might the next chapter go?

I am hoping that we can find a nice way of talking about internal categories in homotopy type theory.

We had discussed this, and the technical problems to be overcome, here and elsewhere every now and then. For a while I played with the thought that the notion of Segal categories might lend itself more naturally to a HoTT formulation, because – at least in something like cohesive homotopy type theory the discreteness condition that they involve is easily formulated: it says that the object of objects is a discrete h-set. But it is also a very restrictive condition if one is really interested in general internalization: Segal categories rather model $\infty$ -enrichment than $\infty$ -internalization.

The notion that genuinely models internal $\infty$ -categories is that of complete Segal space objects. For a while I thought that the completeness condition would be hard to deal with, but that was completely mislead: in fact the completeness Segal-condition is already, somewhat secretly, at the center of attention in homotopy type theory (that is what the above post tries to highlight).

…the small reflection of the ambient (∞,1)-topos into itself

is beginning to sound like Leibniz’s God as monad, perfectly mirroring all the other monads.

It is however a very familiar idea already in ordinary topos theory, even though it is maybe not being highlighted in standard texts to the extent it deserves. In the entry internal sheaf on the $n$ Lab is discussed how an internal sheaf in a topos $\mathcal{T}$ on an internal category object $\mathbb{C}$ is a morphism from $\mathbb{C}^{op}$ to the “small reflection of the topos into itself”, denoted $\bar\mathcal{S}$ in the entry, and which lemma in the Elephant says this – albeit maybe not fully explicitly.

So the next chapter to be opened here is that we speak about (∞,2)-sheaves in HoTT, such as the canonical $(\infty,2)$ -sheaf of quasicoherent ∞-modules. At some point this clearly needs to be done, if HoTT lives up to its promise.

So this post here is meant to express that parts of this are already more naturally expressed in univalent homotopy type theory than has been made explicit before.

For instance, to expand on the above brief description, that internal reflection of the $\infty$ -topos into itself, or the canonical internal base topos $\mathcal{Type}$ , to coin a term, is, I think, the internal category object which in low degree is simply given as follows

$\array{ \vdots &\vdots && \vdots \\ & & & \downarrow \downarrow \downarrow \downarrow \\ [(f,g,h) : \sum_{(A,B,C) : Type \times Type \times Type} (A \to B) \times (B \to C) \times (A \to C) & \vdash (g \circ f = h) : Type ] &=:& \mathcal{Type}_3 \\ & && \downarrow \downarrow \downarrow \\ [(A,B) : Type \times Type & \vdash A \to B : Type] &=:& \mathcal{Type}_1 \\ & & & \downarrow \downarrow \\ & [\vdash Type : Type_1] &=:& \mathcal{Type}_0 }$

equipped with the evident degeneracy maps

$A : Type \vdash s_0 : A \to (A \to A)$

etc. Here $\mathcal{Type}_0$ is the type of objects of the canonical internal base topos / internal self-reflection, $\mathcal{Type}_1$ is the type of morphisms, $\mathcal{Type}_2$ that of 2-morphisms, etc. The fact that these are formed as dependent types as indicated makes this simplicial object be Reedy fibrant, and it is automatically Reedy cofibrant if we think of interpretation in a type-theoretic model category where the cofibrations are the monomorphisms. Finally univalence makes this a complete Segal object.

If nothing else, playing around with this “canonical self-reflection” seems to be a good example to test ideas about formulating internal categories in HoTT against.

Posted by: Urs Schreiber on May 20, 2012 7:49 PM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

if HoTT lives up to its promise

HoTT didn’t promise me personally that it would be able to talk about the $(\infty,2)$ -sheaf of quasicoherent $\infty$ -modules. (-:

It’s quite possible that it will be able to, but I don’t want anyone to get the impression that it will be a failure if it doesn’t.

Posted by: Mike Shulman on May 21, 2012 5:02 AM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

I don’t want anyone to get the impression that it will be a failure if it doesn’t.

Right, sorry, I put that badly. What I tried to express what that this is a natural question, quite independently of my particular comments above. The “At some point this clearly needs to be done” was meant as “Even if what I say here will lead nowhere, this is a natural question to ask.”

On the other hand, I am growing fond of a kind of “hybrid HoTT” where I don’t worry about whether I can strictly formulate something so that Coq or Agda will understand me (for instance the ellipses in the above diagram!), but where I just use the HoTT perspective on higher topos theory to enhance my understanding of the latter, say by noticing that HoTT suggests certain nice constructions in $\infty$ -topos theory not otherwise noticed (we talked about it). Speaking HoTT as a way to help me think internally in an $\infty$ -topos.

From this perspective there is no question if HoTT can help with $(\infty,2)$ -sheaves, but just how. And for me it already was of help in this respect.

Posted by: Urs Schreiber on May 21, 2012 6:44 AM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

I think there’s a lot to be said for that sort of “hybrid” approach, using type-theoretic ways of thinking without needing to worry about formalizing it precisely. If nothing else, it lets one leave the coherence worries to someone else!

Posted by: Mike Shulman on May 21, 2012 7:33 AM | Permalink | Reply to this

Re: Segal-completeness and univalence

$MathML-enabled post (click for more details).$

…where I just use the HoTT perspective on higher topos theory to enhance my understanding of the latter, say by noticing that HoTT suggests certain nice constructions in ∞-topos theory not otherwise noticed.

So that seems to involve the carving concepts correctly aspect of foundational systems.

Posted by: David Corfield on May 21, 2012 8:17 AM | Permalink | Reply to this

Univalence in locally cartesian closed infinity-categories

$MathML-enabled post (click for more details).$

It seems worth amplifying the existence of the following recent preprint somewhere (and so I am doing it hereby), which claims to pretty comprehensively and positively solve the univalence issue:

David Gepner, Joachim Kock, Univalence in locally cartesian closed infinity-categories (arXiv:1208.1749)

Abstract In the setting of presentable locally cartesian closed infinity-categories, we show that univalent families, in the sense of Voevodsky, form a poset isomorphic to the poset of bounded local classes, in the sense of Lurie. It follows that every infinity-topos has a hierarchy of “universal” univalent families, indexed by regular cardinals, and that n-topoi have univalent families classifying (n-2)-truncated maps. We show that univalent families are preserved (and detected) by right adjoints to locally cartesian localizations, and use this to exhibit certain canonical univalent families in infinity-quasitopoi (infinity-categories of “separated presheaves”). We also exhibit some more exotic examples of univalent families, illustrating that a univalent family in an n-topos need not be (n-2)-truncated, as well as some univalent families in the Morel-Voevodsky infinity-category of motivic spaces, an instance of a locally cartesian closed infinity-category which is not an $n$ -topos for any $0 \leq n \leq \infty$ . Lastly, we show that any presentable locally cartesian closed infinity-category is modeled by a type-theoretic model category, and conversely that the infinity-category underlying a type-theoretic model category is presentable and locally cartesian closed; moreover, univalent families in presentable locally cartesian closed infinity-categories correspond precisely to univalent fibrations in type-theoretic model categories.

(I guess the last statement is essentially the same that Denis-Charles Cisinski recently helped prove in discussion with Mike, as recorded here.)

Posted by: Urs Schreiber on August 16, 2012 11:34 AM | Permalink | Reply to this

Re: Univalence in locally cartesian closed infinity-categories

$MathML-enabled post (click for more details).$

…claims to pretty comprehensively and positively solve the univalence issue.

That sounds impressive. Can someone give us a sense of its significance? Were univalent families hard to find before now?

Posted by: David Corfield on August 16, 2012 12:02 PM | Permalink | Reply to this

Re: Univalence in locally cartesian closed infinity-categories

$MathML-enabled post (click for more details).$

Were univalent families hard to find before now?

At least not at a heuristic level in the $\infty$ -topos theory: there the statement that is now formalized as corollary 2.6 in the above article – in view of example 2.3 there (from HTT) – was the basis of all the interest into this issue in the first place: that object classifiers in an $\infty$ -topos are univalent universes.

The stumbling block, as far as I am aware, was the strictification of this statement to the strict interpretations of homotopy type theory in suitable model categories. In this respect the key observation of the above article is the discussion in section 6, which shows how to deduce strict univalence in a (canonical) strict presentation from the (easier) univalence in the corresponding $\infty$ -category.

Posted by: Urs Schreiber on August 16, 2012 2:04 PM | Permalink | Reply to this

Re: Univalence in locally cartesian closed infinity-categories

$MathML-enabled post (click for more details).$

I am not yet convinced that this preprint really contributes anything to the strictification problem. As Urs says, we knew already that $(\infty,1)$ -toposes contained homotopically-univalent universes; the problem is lifting them to the model-categorical level in a sufficiently strict way to serve as “universes a la Russell” and handle the coherence questions of modeling type theory. I don’t see this question addressed at all in their section 6; what they call “strict univalence” has nothing to do with the real strictness problem, which is that the collection of fibrations classified – via strict 1-pullbacks in the model category – by the universal fibration must be closed under all the categorical operations which model type-formers, such as composition (for dependent sum) and exponentials (for dependent product).

But I could be wrong. I’ve emailed Joachim and David for clarification.

Posted by: Mike Shulman on August 16, 2012 8:04 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

May 18, 2012