Not signed in (Sign In)

# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Sign in using OpenID

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeNov 24th 2011
• (edited Nov 24th 2011)
• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeDec 14th 2011

added to univalence a section In simplicial sets, making things a bit explicit.

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeDec 15th 2011

The References section at univalence axiom attributes it jointly to Awodey and Voevodsky. I always thought it was Voevodsky’s alone; where is the attribution to Awodey from? Awodey and his collaborators and students did independently come at the idea of homotopy type theory, and especially identity types as path spaces, but I thought univalence was Voevodsky’s invention.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeDec 15th 2011
• (edited Dec 15th 2011)

Right, I have fixed it.

Not that it’s very important, but what’s the right date to give in “Univalence was proposed by Voevodsky around 20xx.” ?

Is it 2005, or is this also just when he envisioned homotopy type theory without univalence?

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeDec 15th 2011
• (edited Dec 15th 2011)

I am working on a more general section In categorical semantics.

I am still fiddling with some details. (But I notice that the only reference (pages 5 and 6) is, too ;-)

For instance: Voevodsky and these authors speak about the morphism $B\to \left[E×B,B×E{\right]}_{𝒞{/}_{B×B}}$. But we need a morphism ${B}^{I}\to \left[E×B,B×E{\right]}_{𝒞{/}_{B×B}}$ instead. I understand that by 2-out-of-3 the latter is a weak equivalence if the former is, but I still need to think about how to define the latter in the first place.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeDec 15th 2011
• (edited Dec 15th 2011)

Oh, I get it.

Let’s see, what is path induction really in the model categorical semantics? It is lifting in

$\begin{array}{ccc}B& \stackrel{f}{\to }& X\\ ↓& ↗& ↓\\ {B}^{I}& \to & *\end{array}$

using that the left vertical morphism can be chosen to be an acyclic cofibration and that $X$ is fibrant. Right?

[edit: I have added a bit more along these lines.]

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeDec 15th 2011

what’s the right date to give

I don’t know.

Yes, your definition of the univalence morphism is right. I changed the definition of the map $q$ to an equivalent one which I find more intuitive (I think it explains better why this is really just the identity map), but if you prefer the other one we can discuss it.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeDec 15th 2011

Although, I think it requires an extra hypothesis on $𝒞$, such as all objects (or certain objects) being cofibrant, in order to identify this statement with the univalence axiom holding in the internal type theory. The point is that a given map being a weak equivalence in the model category has to be identified with the inhabitation of the corresponding $\mathrm{isEquiv}$ type in the type theory. I’ve worked this out to a certain degree, so I should put it on the lab somewhere.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeDec 15th 2011
• (edited Dec 15th 2011)

Thanks, Mike.

such as all objects (or certain objects) being cofibrant,

It occured to me today during lunch that I should have added some cofibrancy condition also to be able to deduce that $\left[E×B,B×E{\right]}_{𝒞{/}_{B×B}}$ is indeed fibrant. But it is not until many hours later now that I have the leisure to come back to this.

I feel like I should say that these days I only have a few stolen moments here and there to think about these things, such as yesterday on a night train from Hamburg, which is why I keep leaving stubby entries.

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeDec 16th 2011
• (edited Dec 16th 2011)

I am guessing the following is true.

The univalent fibrations in $\mathrm{sSet}$ (not necessarily universal) are, up to equivalence, precisely the canonical associated infinity-bundles which are associated to $\mathrm{Aut}\left(F\right)$-principal $\infty$-bundles, namely the fibrations

$F↪\mathrm{B}\left(*,\mathrm{Aut}\left(F\right),F\right)\stackrel{{p}_{F}}{\to }\mathrm{B}\left(*,\mathrm{Aut}\left(F\right),*\right)\phantom{\rule{thinmathspace}{0ex}},$

where $\mathrm{B}\left(-,-,-\right)$ is the two-sided bar-construction.

I know that the universal fibration is ${\coprod }_{\left[F\right]}{p}_{F}$, where the coproduct runs over all small homotopy types. The above statement (“I am guessing”) immediately implies univalence for this.

The guess is obviously “morally right”, unless I am mixed up. It seems one only needs to fiddle a bit to show that the canonical morphisms discussed at univalence do exactly what one expects them to do.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeDec 16th 2011

Yes, that seems right. It’s the “up to equivalence” that is the kicker — we need a good point-set model which classifies al small fibrations via strict pullback. This is what Voevodsky’s trick with the universal Kan fibration accomplishes.

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeDec 16th 2011
• (edited Dec 16th 2011)

Yes, I understand. But once you have the strict classifier, the statement of univalence should not depend on the model that much, since it mentions weak equivalence, and not isomorphism.

Take the $\left[F\right]$-component of some strict model for the small object classifier. It should be equivalent, as an $F$-bundle to, say, $B\left(*,\mathrm{Aut}\left(F\right),F\right)\to B\left(*,\mathrm{Aut}\left(F\right),*\right)$, or some other convenient model of the weak small object classifier. Showing univalence for the latter should imply it for the former, I’d think.

Ieke Moerdijk presented a proof of univalence along these lines two weeks ago in Leiden, by passing through a Kan minimal model for the universal $F$-associated bundle.

I was thinking that with Wendt’s arguments for classification of associated bundles in $\infty$-stacks one could make progress towards the parameterized version. But looking at Peter May’s argument from 1975 that he keeps refering to, I get the feeling now that there is still a bit of a gap to be filled here.

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeDec 16th 2011

Let me turn this around:

we can ask “is it univalent?” about the $\kappa$-compact object classifier in any $\left(\infty ,1\right)$-topos, quite independently of the question of how to find a strict model for it in some presentation.

That is: are object classifiers in general $\left(\infty ,1\right)$-toposes associated $\infty$-bundles?

Do we have an argument for this in the context of $\left(\infty ,1\right)$-topos theory (independently of the needs of homotopy type theory)??

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeDec 16th 2011

Yes, I think that’s easy to see. By the Yoneda lemma, ${B}^{I}\to \mathrm{Eq}\left(E\right)$ is an equivalence if it induces an equivalence on all hom-$\infty$-groupoids $\mathrm{Hom}\left(X,{B}^{I}\right)\to \mathrm{Hom}\left(X,\mathrm{Eq}\left(E\right)\right)$, which is a fiberwise map over $\mathrm{Hom}\left(X,B×B\right)$. For a given map $\left(f,g\right):X\to B×B$, classifying two objects $F\to X$ and $G\to X$ of $H/X$, lifts to ${B}^{I}$ form the space ${\mathrm{Hom}}_{\mathrm{Hom}\left(X,B\right)}\left(f,g\right)$, while lifts to $\mathrm{Eq}\left(E\right)$ form the space $\mathrm{Core}\left(H/X\right)\left(F,G\right)$. These two are naturally equivalent by the obvious map, by definition of what it means to be an object classifier; hence ${B}^{I}\to \mathrm{Eq}\left(E\right)$ is also an equivalence.

• CommentRowNumber15.
• CommentAuthorUrs
• CommentTimeJan 3rd 2012
• (edited Jan 3rd 2012)

Thanks, Mike. That’s of course an evident argument, which I should have noticed.

So to prove univalence for a given fibration, it almost seems sufficient to prove that the fibration indeed presents the $\kappa$-small object classifier in the $\infty$-topos theoretic sense.

In $\infty \mathrm{Grpd}$ I know how to prove that the $\kappa$-small object classifier is $\mathrm{Core}\left(\infty {\mathrm{Grpd}}_{\kappa }\right)\simeq {\coprod }_{\mathrm{homotopy}\mathrm{types}\left[F\right]}B\mathrm{AUT}\left(F\right)$. From Stasheff (1963) and then May (1975) we know that this is the base for the coproduct of universal $F$-fibrations. (The pdf that went over the HoTT list a few hours back rederives this, up to and including its equation (3) on the second but last page.)

So to see that it’s univalent, by the above it suffices to observe that the relevant morphism from the path object to $\mathrm{Eq}\left(E\right)$ indeed presents the abstractly defined morphism, which you point out is an an equivalence by definition of object classifier.

By this kind of argument I seem to deduce that to prove univalence in a general local model structure on simplicial presheaves. the work is in producing a model for the universal fibration. Once one has it, it must be univalent since the thing that it models trivially is.

(I may still be mixed up. Hope you don’t mind chatting about it a bit more, nevertheless.)

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeJan 3rd 2012

Yes, the work is in producing a model, but it has to not just be a model of the universal fibration (we know, of course, that some model of that exists, even if we don’t have an explicit construction on the model category level) but we also need good closure properties of the class of morphisms that it strictly classifies, as I said in #11.

• CommentRowNumber17.
• CommentAuthorUrs
• CommentTimeJan 3rd 2012

Okay, thanks. Sorry for going in circles.

But one last question for the moment, which I should have asked long before:

what is the/a good detailed reference for Voevodsky’s proof of his univalent model?

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeJan 9th 2012

The only references I know are Voevodsky’s notes on type systems and more recently these notes taken by Chris Kapulkin on a talk by Ieke Moerdijk presenting a shorter proof of the univalence (which could equivalently be considered a proof that the particular object in question does in fact repreesent the object classifier).

• CommentRowNumber19.
• CommentAuthorMike Shulman
• CommentTimeMar 13th 2012

A nice readable exposition of the proof of univalence in simplicial sets has just appeared on the arXiv.

• CommentRowNumber20.
• CommentAuthorMike Shulman
• CommentTimeMar 16th 2012

And, at last, a construction of a few new models of univalence.

• CommentRowNumber21.
• CommentAuthorUrs
• CommentTimeMar 16th 2012

Great! I have added the reference to univalence.

(for other readers: related discussion is on the HoTT site here.)

• CommentRowNumber22.
• CommentAuthorUrs
• CommentTimeMay 18th 2012

here a comment/question just on terminology:

in the entry univalence it says “path reduction” for the non-dependent or “simple” version of the elimination rule. Elsewhere we had agreed that this should be called recursion, with induction being the dependent / non-simple version.

Unless I am mixed up: is it still too late to change terminology? I would enjoy seeing the induction/recursion distinction be used systematically, as it is kind of nice, conceptually.

• CommentRowNumber23.
• CommentAuthorMike Shulman
• CommentTimeMay 19th 2012

Well, recursion is a special case of induction, so I don’t see what’s wrong with using “induction” to refer to cases that don’t happen to be dependent.

• CommentRowNumber24.
• CommentAuthorUrs
• CommentTimeMay 19th 2012
• (edited May 19th 2012)

They are both special cases of each other. So there is nothing wrong with it either way, as it is equivalent.

But I thought it would still be nice to make the distinction in words anyway, because even though they are equivalent, when written out one is verbatim the generalization of traditional induction, the other verbatim that of traditional recursion.

It’s not so important, though.

• CommentRowNumber25.
• CommentAuthorMike Shulman
• CommentTimeMay 20th 2012

I thought you said that “recursion” meant the non-dependent elimination rule. The dependent one is not a special case of that, is it?

• CommentRowNumber26.
• CommentAuthorUrs
• CommentTimeMay 20th 2012

Hm, I had indeed thought that that’s what the article by Awodey-Gambino-Sojakova said on p. 9, but now I remember that it is only true if one adds some $\eta$-rule to the simple elimination.

Okay, I understand.

• CommentRowNumber27.
• CommentAuthorUrs
• CommentTimeAug 16th 2012

I have only right now become aware of the recent preprint

and so I added it to the References-section at univalence.

• CommentRowNumber28.
• CommentAuthorUrs
• CommentTimeNov 23rd 2012
• (edited Nov 23rd 2012)

added to univalence a pointer to the IAS video recording of somebody’s lecture The computational interpretation of HoTT.

NOTICE: the web-site has that video mixed up with the page for On the setoid model of type theory. (the titles are interchanged, or else the titles are right, but the links to the videos are intechanged).

• CommentRowNumber29.
• CommentAuthorMike Shulman
• CommentTimeNov 23rd 2012

You’re right. (-:

• CommentRowNumber30.
• CommentAuthorUrs
• CommentTimeNov 23rd 2012
• (edited Nov 23rd 2012)

Took me a while: I got really annoyed when after 20 minutes the speaker was still talking about setoids without even having mentioned univalence… before I noticed that I am watching a talk on setoids ;-) (Well, I was listening with only half an ear it while working on something else.)

When I then switched to the correct talk on univalence, I found the following kind of curious, given our earlier discussion here: the speaker (that’s Dan Licata, I suppose? Somebody should really fix these websites…) begins with saying something like “I don’t have to review natural deduction, do I?” only to be flooded with questions from the audience, for the whole first 15 minutes, before he can even mention the topic of univalence.

While I have your attention (if I still do after these ramblings): do you have an opinion on the program by Harper&Licata on canonicity for univalence? I am asking because I gather it’s still somewhat inconclusive, so it would be helpful to hear what an inside perspective would be.

Also, after watching the talk I realized a mistake that I had once introduced in the entry canonicity: I had claimed there that Harper-Licata speak about 2-type theory (directed type theory), but instead they just talk about h-level 3 HoTT. (right?) I have fixed that now.

• CommentRowNumber31.
• CommentAuthorMike Shulman
• CommentTimeNov 24th 2012

I’m still figuring out my opinion. I agree that eventually, we will need some sort of better computational understanding of univalence. It’s not clear (and Dan Licata, who is indeed the speaker in that talk, agrees with this) that this understanding will look like their presentation of (undirected) 2-dimensional type theory in which operations on equalities are given as basic operations, rather than derived from the elimination rule for identity types. After hearing Dan’s talk, I’m a bit more sympathetic towards that approach than I was — but it’s certainly not clear how to extend it to infinite dimensions. Dan has said he thinks an alternative approach would be an algorithm that can “compute” with propositional equalities in some way, taking a term and “evaluating” it, not by definitional beta-reductions, by but transformations connected to it by paths, until it reaches a term of canonical form.

Perhaps I should mention that Thierry Coquand and some other people here have a related project: to build something like Voevodsky’s simplicial set model of type theory starting from a constructive type-theoretic foundation. Essentially, to build a model of intensional type theory (with univalence) starting from extensional type theory, or even better starting from type theory that doesn’t even have identity types (“un-tensional” type theory?). If this succeeds, then arguably it would automatically result in a computational understanding of univalence, since “everything in type theory is computational”. I don’t fully understand to what extent this would answer the same question that Harper&Licata are after, but it’s certainly closely related.

Add your comments
• Please login, or your comments will be posted as "Guest".

Type the two words.

• Format comments as (Help) (Help)