Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 24th 2011
   • (edited Nov 24th 2011)
   • PermaLink
   Author: Urs
   Format: MarkdownItexcreated [[univalence axiom]]

   created univalence axiom

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeDec 14th 2011
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded to [[univalence]] a section [In simplicial sets](http://www.ncatlab.org/nlab/show/univalence+axiom#InSimplicialSets), making things a bit explicit.

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

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeDec 15th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeDec 15th 2011
   • (edited Dec 15th 2011)
   • PermaLink
   Author: Urs
   Format: MarkdownItexRight, 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?

   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?

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeDec 15th 2011
   • (edited Dec 15th 2011)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI am working on a more general section [In categorical semantics](http://ncatlab.org/nlab/show/univalence+axiom#InCategoricalSemantics). I am still fiddling with some details. (But I notice that the [only reference](http://arxiv.org/PS_cache/arxiv/pdf/1111/1111.3489v1.pdf) (pages 5 and 6) is, too ;-) For instance: Voevodsky and these authors speak about the morphism $B \to [E \times B, B \times E]_{\mathcal{C}/_{B \times B}}$. But we need a morphism $B^I \to [E \times B, B \times E]_{\mathcal{C}/_{B \times 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.

   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 [E \times B, B \times E]_{\mathcal{C}/_{B \times B}}$. But we need a morphism $B^I \to [E \times B, B \times E]_{\mathcal{C}/_{B \times 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.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeDec 15th 2011
   • (edited Dec 15th 2011)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOh, I get it. Let's see, what is path induction really in the model categorical semantics? It is lifting in $$ \array{ B &\stackrel{f}{\to}& X \\ \downarrow &\nearrow& \downarrow \\ B^I &\to& * } $$ using that the left vertical morphism can be chosen to be an acyclic cofibration and that $X$ is fibrant. Right? [edit: I have [added](http://ncatlab.org/nlab/show/univalence+axiom#InCategoricalSemantics) a bit more along these lines.]

   Oh, I get it.

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

   $$\array{ B &\stackrel{f}{\to}& X \\ \downarrow &\nearrow& \downarrow \\ B^I &\to& * }$$

   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.]

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeDec 15th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeDec 15th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAlthough, I think it requires an extra hypothesis on $\mathcal{C}$, 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 $isEquiv$ type in the type theory. I've worked this out to a certain degree, so I should put it on the lab somewhere.

   Although, I think it requires an extra hypothesis on $\mathcal{C}$, 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 $isEquiv$ type in the type theory. I’ve worked this out to a certain degree, so I should put it on the lab somewhere.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeDec 15th 2011
   • (edited Dec 15th 2011)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, 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 $[E \times B , B \times E]_{\mathcal{C}/_{B \times 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.

   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 $[E \times B , B \times E]_{\mathcal{C}/_{B \times 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.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 16th 2011
    • (edited Dec 16th 2011)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI am guessing the following is true. The univalent fibrations in $sSet$ (not necessarily universal) are, up to equivalence, precisely the canonical [[associated infinity-bundles]] which are associated to $Aut(F)$-principal $\infty$-bundles, namely the fibrations $$ F \hookrightarrow \mathrm{B}(*, Aut(F), F) \stackrel{p_F}{\to} \mathrm{B}(*, Aut(F), *) \,, $$ where $\mathrm{B}(-,-,-)$ is the two-sided bar-construction. I know that the universal fibration is $\coprod_{[F]} 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.

    I am guessing the following is true.

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

    $$F \hookrightarrow \mathrm{B}(*, Aut(F), F) \stackrel{p_F}{\to} \mathrm{B}(*, Aut(F), *) \,,$$

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

    I know that the universal fibration is $\coprod_{[F]} 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.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 16th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, 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.

    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.

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 16th 2011
    • (edited Dec 16th 2011)
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, 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 $[F]$-component of some strict model for the small object classifier. It should be equivalent, as an $F$-bundle to, say, $B(*, Aut(F), F) \to B(*,Aut(F),*)$, 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](http://arxiv.org/PS_cache/arxiv/pdf/1009/1009.2930v3.pdf#page=31) 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.

    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 $[F]$-component of some strict model for the small object classifier. It should be equivalent, as an $F$-bundle to, say, $B(*, Aut(F), F) \to B(*,Aut(F),*)$, 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.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 16th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItexLet me turn this around: we can ask "is it univalent?" about the $\kappa$-compact object classifier in any $(\infty,1)$-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 $(\infty,1)$-toposes associated $\infty$-bundles? Do we have an argument for this in the context of $(\infty,1)$-topos theory (independently of the needs of homotopy type theory)??

    Let me turn this around:

    we can ask “is it univalent?” about the $\kappa$-compact object classifier in any $(\infty,1)$-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 $(\infty,1)$-toposes associated $\infty$-bundles?

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

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeDec 16th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, I think that's easy to see. By the Yoneda lemma, $B^I \to Eq(E)$ is an equivalence if it induces an equivalence on all hom-$\infty$-groupoids $Hom(X,B^I) \to Hom(X,Eq(E))$, which is a fiberwise map over $Hom(X,B\times B)$. For a given map $(f,g)\colon X\to B\times B$, classifying two objects $F\to X$ and $G\to X$ of $\mathbf{H}/X$, lifts to $B^I$ form the space $Hom_{Hom(X,B)}(f,g)$, while lifts to $Eq(E)$ form the space $Core(\mathbf{H}/X)(F,G)$. These two are naturally equivalent by the obvious map, by definition of what it means to be an object classifier; hence $B^I\to Eq(E)$ is also an equivalence.

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

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2012
    • (edited Jan 3rd 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, 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 Grpd$ I know how to prove that the $\kappa$-small object classifier is $Core( \infty Grpd_{\kappa}) \simeq \coprod_{homotopy types [F]} \mathbf{B} AUT(F)$. From Stasheff (1963) and then [May (1975)](http://www.math.uchicago.edu/~may/BOOKS/Classifying.pdf) we know that this is the base for the coproduct of universal $F$-fibrations. (The [pdf](http://www.pitt.edu/~krk56/fiber_bundles_univalence.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 $Eq(E)$ 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.)

    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 Grpd$ I know how to prove that the $\kappa$-small object classifier is $Core( \infty Grpd_{\kappa}) \simeq \coprod_{homotopy types [F]} \mathbf{B} AUT(F)$. 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 $Eq(E)$ 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.)

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 3rd 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, 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.

    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.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, 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?

    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?

18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 9th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe only references I know are Voevodsky's [notes on type systems](http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html) and more recently [these notes](http://www.pitt.edu/~krk56/fiber_bundles_univalence.pdf) 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).

    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).

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexA nice readable exposition of the proof of univalence in simplicial sets has just [appeared on the arXiv](http://arxiv.org/abs/1203.2553).

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

20. • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMar 16th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAnd, at last, a construction of a few [new models of univalence](http://homotopytypetheory.org/2012/03/15/inverse-diagrams/).

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

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMar 16th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexGreat! I have added the reference to _[[univalence]]_. (for other readers: related discussion is on the HoTT site [here](http://homotopytypetheory.org/2012/03/15/inverse-diagrams/).)

    Great! I have added the reference to univalence.

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

22. • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexhere 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.

    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.

23. • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMay 19th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWell, 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.

    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.

24. • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2012
    • (edited May 19th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThey 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.

    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.

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeMay 20th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI thought you said that "recursion" meant the non-dependent elimination rule. The dependent one is not a special case of that, is it?

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

26. • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeMay 20th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexHm, I had indeed thought that that's what the article by Awodey-Gambino-Sojakova said on [p. 9](https://arxiv.org/pdf/1201.3898v2.pdf#page=9), but now I remember that it is only true if one adds some $\eta$-rule to the simple elimination. Okay, I understand.

    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.

27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeAug 16th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have only right now become aware of the recent preprint * [[David Gepner]], [[Joachim Kock]], _Univalence in locally cartesian closed infinity-categories_ ([arXiv:1208.1749](http://arxiv.org/abs/1208.1749)) and so I added it to the References-section at _[[univalence]]_.

    I have only right now become aware of the recent preprint

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

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

28. • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeNov 23rd 2012
    • (edited Nov 23rd 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded to _[[univalence]]_ a pointer to the IAS video recording of somebody's lecture _[The computational interpretation of HoTT](http://video.ias.edu/stream&ref=1674)_. NOTICE: the web-site has that video mixed up with the page for _[On the setoid model of type theory](http://video.ias.edu/univalent/palmgren)_. (the titles are interchanged, or else the titles are right, but the links to the videos are intechanged).

    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).

29. • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeNov 23rd 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYou're right. (-:

    You’re right. (-:

30. • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeNov 23rd 2012
    • (edited Nov 23rd 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexTook 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.

    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.

31. • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeNov 24th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI'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.

    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.

32. • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeOct 1st 2013
    • (edited Oct 1st 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded a section _[univalance -- Canonicity](http://ncatlab.org/nlab/show/univalence+axiom#Canonicity)_ with a basic pointer to Mike's result and to the Coquand-Huber approach. (I wrote this three times, losing previous versions twice with the nLab and my computer crashing in turn. The version now is not as good as a previous one, but I am out of good spirits now.)

    added a section univalance – Canonicity with a basic pointer to Mike’s result and to the Coquand-Huber approach.

    (I wrote this three times, losing previous versions twice with the nLab and my computer crashing in turn. The version now is not as good as a previous one, but I am out of good spirits now.)

33. • CommentRowNumber33.
    • CommentAuthorTobyBartels
    • CommentTimeOct 4th 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexExternal editors! [It\'s All Text](https://addons.mozilla.org/en-US/firefox/addon/its-all-text/) helps make it convenient with Firefox.

    External editors! It's All Text helps make it convenient with Firefox.

34. • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2013
    • (edited Nov 12th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexcorrected qualifications in the first paragraph at _[[univalence|univalence -- Canonicity]]_ (thanks to discussion with Andrej Bauer and Mike Shulman and Bob Harper)

    corrected qualifications in the first paragraph at univalence – Canonicity (thanks to discussion with Andrej Bauer and Mike Shulman and Bob Harper)

35. • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThe link doesn't work for >Simon Huber (with Thierry Coquand), Towards a computational justification of the Axiom of Univalence , talk at TYPES 2011 (pdf) Is [this](https://www.humboldt-kolleg.iam.unibe.ch/talks/Coquand.pdf‎) a similar talk?

    The link doesn’t work for

    Simon Huber (with Thierry Coquand), Towards a computational justification of the Axiom of Univalence , talk at TYPES 2011 (pdf)

    Is this a similar talk?

36. • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThe latest details are being discussed [here](https://plus.google.com/u/0/104899653423422914048/posts/UyW11hFXdSE). (Can you see this?)

    The latest details are being discussed here.

    (Can you see this?)

37. • CommentRowNumber37.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexYes, thanks. Hopefully this is building towards making Martin-Lof happy with a computational justification. I was wondering also though for that dead link whether the suggested replacement is adequate.

    Yes, thanks. Hopefully this is building towards making Martin-Lof happy with a computational justification.

    I was wondering also though for that dead link whether the suggested replacement is adequate.

38. • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexSorry, which dead link? (I guess I wasn't paying attention.)

    Sorry, which dead link? (I guess I wasn’t paying attention.)

39. • CommentRowNumber39.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThe link to the talk mentioned at [univalence axiom](univalence+axiom#References) >Simon Huber (with Thierry Coquand), Towards a computational justification of the Axiom of Univalence , talk at TYPES 2011 Now, I see I gave a wrong link to a talk by Coquand in #35, which if I can get it right is [here](http://www.humboldt-kolleg.iam.unibe.ch/talks/Coquand.pdf). Presumably it's the same material.

    The link to the talk mentioned at univalence axiom

    Simon Huber (with Thierry Coquand), Towards a computational justification of the Axiom of Univalence , talk at TYPES 2011

    Now, I see I gave a wrong link to a talk by Coquand in #35, which if I can get it right is here. Presumably it’s the same material.

40. • CommentRowNumber40.
    • CommentAuthorRodMcGuire
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: RodMcGuire
    Format: MarkdownItex> Is [this](https://www.humboldt-kolleg.iam.unibe.ch/talks/Coquand.pdf‎) a similar talk? Bad link - missing "http" and a trailing [invisible Unicode LRM](http://nforum.mathforge.org/discussion/5291/make-visible-or-surpress-invisible-characters/) David - where you copying and pasting those LRMs from? [http://www.humboldt-kolleg.iam.unibe.ch/talks/Coquand.pdf‎](http://www.humboldt-kolleg.iam.unibe.ch/talks/Coquand.pdff)

    Is this a similar talk?

    Bad link - missing “http” and a trailing invisible Unicode LRM

    David - where you copying and pasting those LRMs from?

    http://www.humboldt-kolleg.iam.unibe.ch/talks/Coquand.pdf‎

41. • CommentRowNumber41.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI really don't know where the LRM comes from. I just copy out of my browser and it seems to appear sometimes.

    I really don’t know where the LRM comes from. I just copy out of my browser and it seems to appear sometimes.

42. • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2013
    • (edited Nov 12th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThose LRMs come from copying the green URLs in Google's result list! One can fix it by removing what looks like "pdf" at the end with the backspace key and then re-typing "pdf" (and pre-fixing the url with its "http://"). Maybe this didn't always used to be this way with Google. I do this fixing a lot lately.

    Those LRMs come from copying the green URLs in Google’s result list!

    One can fix it by removing what looks like “pdf” at the end with the backspace key and then re-typing “pdf” (and pre-fixing the url with its “http://”).

    Maybe this didn’t always used to be this way with Google. I do this fixing a lot lately.

43. • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have added the Humboldt-Kolleg talk link to the entry [here](http://ncatlab.org/nlab/show/univalence+axiom#Coquand13)

    I have added the Humboldt-Kolleg talk link to the entry here

44. • CommentRowNumber44.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Urs 36 - is that a private discussion? I can't see it.

    @Urs 36 - is that a private discussion? I can’t see it.

45. • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, it's marked private. If I find a second (or somebody else who can see it) we should just make a note of some of the actual technical statements given there in the nLab entry.

    Yes, it’s marked private. If I find a second (or somebody else who can see it) we should just make a note of some of the actual technical statements given there in the nLab entry.

46. • CommentRowNumber46.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 12th 2013
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexPerhaps Andrej or Mike can at least cut and paste/summarise some of the discussion to somewhere more readable?

    Perhaps Andrej or Mike can at least cut and paste/summarise some of the discussion to somewhere more readable?

47. • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWith [this firefox add-on](https://addons.mozilla.org/en-US/firefox/addon/google-search-link-fix/) you can right-click on a google search result and copy the URL. I'll see if I can find time to summarize the points.

    With this firefox add-on you can right-click on a google search result and copy the URL.

    I’ll see if I can find time to summarize the points.

48. • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOkay, I tried to explain a bit more at [[univalence]].

    Okay, I tried to explain a bit more at univalence.

49. • CommentRowNumber49.
    • CommentAuthorUrs
    • CommentTimeNov 13th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks!!

    Thanks!!

50. • CommentRowNumber50.
    • CommentAuthorRodMcGuire
    • CommentTimeNov 13th 2013
    • PermaLink
    Author: RodMcGuire
    Format: MarkdownItexin [[univalence]] these links are broken: >The [[HoTT]]-[[Coq]] code is at >* _[HoTT/Coq/Univalence.v](https://github.com/HoTT/HoTT/blob/master/Coq/Univalence.v)_ >* _[HoTT/Coq/UnivalenceAxiom.v](https://github.com/HoTT/HoTT/blob/master/Coq/UnivalenceAxiom.v)_

    in univalence these links are broken:

    The HoTT-Coq code is at

    • HoTT/Coq/Univalence.v

    • HoTT/Coq/UnivalenceAxiom.v

51. • CommentRowNumber51.
    • CommentAuthorspitters
    • CommentTimeNov 13th 2013
    • PermaLink
    Author: spitters
    Format: TextWhat is the status of this line? " Univalence is claimed to be established in all (infinity,1)-toposes, their presentations by type-theoretic model categories as well as further cases of locally cartesian closed (infinity,1)-categories in David Gepner, Joachim Kock, Univalence in locally cartesian closed infinity-categories (arXiv:1208.1749) " I know some people think it is not the final word on the topic.

    What is the status of this line?
    "
    Univalence is claimed to be established in all (infinity,1)-toposes, their presentations by type-theoretic model categories as well as further cases of locally cartesian closed (infinity,1)-categories in
    David Gepner, Joachim Kock, Univalence in locally cartesian closed infinity-categories (arXiv:1208.1749)
    "
    
    I know some people think it is not the final word on the topic.
52. • CommentRowNumber52.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexThanks, Mike.

    Thanks, Mike.

53. • CommentRowNumber53.
    • CommentAuthorMike Shulman
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex@spitters, I think the issue is with the universes rather than the univalence -- we don't know how to get strict universes in type theory out of object classifiers in general. Is that what you mean? We should probably clarify the sentence.

    @spitters, I think the issue is with the universes rather than the univalence – we don’t know how to get strict universes in type theory out of object classifiers in general. Is that what you mean? We should probably clarify the sentence.

54. • CommentRowNumber54.
    • CommentAuthorspitters
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: spitters
    Format: TextYes, that's what I meant. There was quite a bit of discussion about this in Barcelona. Maybe this part should be merged with: http://ncatlab.org/nlab/show/type-theoretic+model+category

    Yes, that's what I meant. There was quite a bit of discussion about this in Barcelona.
    Maybe this part should be merged with:
    http://ncatlab.org/nlab/show/type-theoretic+model+category
55. • CommentRowNumber55.
    • CommentAuthorMike Shulman
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYou can make links to the nLab from here by typing `[[type-theoretic model category]]`, just as on the nLab itself. I don't see why or what to merge though.

    You can make links to the nLab from here by typing [[type-theoretic model category]], just as on the nLab itself. I don’t see why or what to merge though.

56. • CommentRowNumber56.
    • CommentAuthorspitters
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: spitters
    Format: TextSure. That would be another option.

    Sure. That would be another option.
57. • CommentRowNumber57.
    • CommentAuthorMike Shulman
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat?

    What?

58. • CommentRowNumber58.
    • CommentAuthorMike Shulman
    • CommentTimeNov 17th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI tried to clarify this reference. I also added a remark that univalence essentially occurs in the 1996 Hofmann-Streicher paper under the name "universe extensionality" (although "type extensionality" would be a better analogon to "function extensionality").

    I tried to clarify this reference. I also added a remark that univalence essentially occurs in the 1996 Hofmann-Streicher paper under the name “universe extensionality” (although “type extensionality” would be a better analogon to “function extensionality”).

59. • CommentRowNumber59.
    • CommentAuthorColin Zwanziger
    • CommentTimeDec 25th 2014
    • PermaLink
    Author: Colin Zwanziger
    Format: MarkdownItex[[univalence]] contains the assertion: "The univalence axiom says that [equality and equivalence] are the same. Morally, this says that Type behaves like an object classifier." I would like to make this less cryptic, but first I have to decode it--I would be grateful if someone would explain the intuition behind this. [I've understood the proof that the universe is an object classifier in the HoTT book, and I see that it employs univalence. But I don't see the conceptual relation.]

    univalence contains the assertion: “The univalence axiom says that [equality and equivalence] are the same. Morally, this says that Type behaves like an object classifier.” I would like to make this less cryptic, but first I have to decode it–I would be grateful if someone would explain the intuition behind this.

    [I’ve understood the proof that the universe is an object classifier in the HoTT book, and I see that it employs univalence. But I don’t see the conceptual relation.]

60. • CommentRowNumber60.
    • CommentAuthorMike Shulman
    • CommentTimeDec 28th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexFor $U$ to be an object classifier, the pullback map $Hom(X,U) \to Core(\mathbf{H}/X)$ should be fully faithful. The morphisms in $Hom(X,U)$ are equalities of types, while those in $Core(\mathbf{H}/X)$ are equivalences of types. So univalence, which says that equality and equivalence of types are the same, says that this map is an equivalence on morphisms, i.e. fully faithful. Is that the sort of thing you're looking for?

    For $U$ to be an object classifier, the pullback map $Hom(X,U) \to Core(\mathbf{H}/X)$ should be fully faithful. The morphisms in $Hom(X,U)$ are equalities of types, while those in $Core(\mathbf{H}/X)$ are equivalences of types. So univalence, which says that equality and equivalence of types are the same, says that this map is an equivalence on morphisms, i.e. fully faithful. Is that the sort of thing you’re looking for?

61. • CommentRowNumber61.
    • CommentAuthorNikolajK
    • CommentTimeFeb 16th 2016
    • (edited Feb 16th 2016)
    • PermaLink
    Author: NikolajK
    Format: MarkdownItexCan someone specify what the often phrase that is often discussed means, "make univalence compute". Does it mean to find a realization (in programming language) of the term $f : (A {\cong} B) \to (A = B)$ that is inverse to the function running in the other direction? I.e. code up that idea - and idea that is maybe simpler to realize in normal/less formalized mathematics of $\infty$-groupoids?

    Can someone specify what the often phrase that is often discussed means, “make univalence compute”.

    Does it mean to find a realization (in programming language) of the term

    $f : (A {\cong} B) \to (A = B)$

    that is inverse to the function running in the other direction? I.e. code up that idea - and idea that is maybe simpler to realize in normal/less formalized mathematics of $\infty$-groupoids?

62. • CommentRowNumber62.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 16th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRoughly, it means to find a type theory satisfying a normalization/canonicity theorem and in which univalence is true. This doesn't involve just realizing the single term "univalence" as a program, but designing the entire type theory so that all terms can be evaluated.

    Roughly, it means to find a type theory satisfying a normalization/canonicity theorem and in which univalence is true. This doesn’t involve just realizing the single term “univalence” as a program, but designing the entire type theory so that all terms can be evaluated.

63. • CommentRowNumber63.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI added to [[univalence axiom]] some mention of the weaker statements that are known to be sufficient to imply the full UA.

    I added to univalence axiom some mention of the weaker statements that are known to be sufficient to imply the full UA.

64. • CommentRowNumber64.
    • CommentAuthorHarry Gindi
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Harry Gindi
    Format: MarkdownItexThe impression I always got as a non-expert was that univalence is basically designed to be a weaker form of the axiom of extensionality, and as soon as you require this, you're going to have things become uncomputable. Do people think there are real prospects for UA to hold in a completely computable/evaluable type theory?

    The impression I always got as a non-expert was that univalence is basically designed to be a weaker form of the axiom of extensionality, and as soon as you require this, you’re going to have things become uncomputable. Do people think there are real prospects for UA to hold in a completely computable/evaluable type theory?

65. • CommentRowNumber65.
    • CommentAuthorUrs
    • CommentTimeAug 9th 2017
    • (edited Aug 9th 2017)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThe approach called _cubical type theory_ claims to achieve this, though I never quite know what precisely the claim is regarding "book-HoTT": Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, _Cubical Type Theory: a constructive interpretation of the univalence axiom_ ([arXiv:1611.02108](https://arxiv.org/abs/1611.02108)) Of course Mike will know more.

    The approach called cubical type theory claims to achieve this, though I never quite know what precisely the claim is regarding “book-HoTT”:

    Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom (arXiv:1611.02108)

    Of course Mike will know more.

66. • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> univalence is basically designed to be a weaker form of the axiom of extensionality What does that mean? Usually when people say "the axiom of extensionality" they're referring to membership-based set theory, which is a totally different context from type theory in which the univalence axiom makes sense. They're totally incomparable. > as soon as you require this, you’re going to have things become uncomputable Why? > Do people think there are real prospects for UA to hold in a completely computable/evaluable type theory? Yep; cubical type theory appears to basically solve the problem. What's written at [[univalence axiom]] is a bit out of date. Homotopy canonicity for UA as an axiom in Book HoTT is still open, but cubical type theory is a different theory that enjoys both canonicity and univalence.

    univalence is basically designed to be a weaker form of the axiom of extensionality

    What does that mean? Usually when people say “the axiom of extensionality” they’re referring to membership-based set theory, which is a totally different context from type theory in which the univalence axiom makes sense. They’re totally incomparable.

    as soon as you require this, you’re going to have things become uncomputable

    Why?

    Do people think there are real prospects for UA to hold in a completely computable/evaluable type theory?

    Yep; cubical type theory appears to basically solve the problem. What’s written at univalence axiom is a bit out of date. Homotopy canonicity for UA as an axiom in Book HoTT is still open, but cubical type theory is a different theory that enjoys both canonicity and univalence.

67. • CommentRowNumber67.
    • CommentAuthorHarry Gindi
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Harry Gindi
    Format: MarkdownItexSorry, Mike, whatever the axiom you take in addition to the usual Intensional Type Theory to get Extensional Type Theory. "The extensional axiom". It looks remarkably similar to the univalence axiom.

    Sorry, Mike, whatever the axiom you take in addition to the usual Intensional Type Theory to get Extensional Type Theory. “The extensional axiom”. It looks remarkably similar to the univalence axiom.

68. • CommentRowNumber68.
    • CommentAuthorUrs
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItex> but cubical type theory is a different theory It would be good to know how it relates to book-HoTT. Do you know?

    but cubical type theory is a different theory

    It would be good to know how it relates to book-HoTT. Do you know?

69. • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexTo get [[extensional type theory]] one adds [[axiom K]] or [[axiom UIP]]. They look very different from univalence to me; in addition to the fact that they contradict it, they seem to be saying totally different kinds of things. Can you explain what relationship you see?

    To get extensional type theory one adds axiom K or axiom UIP. They look very different from univalence to me; in addition to the fact that they contradict it, they seem to be saying totally different kinds of things. Can you explain what relationship you see?

70. • CommentRowNumber70.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI *believe* that Book HoTT can be interpreted into cubical type theory. I'm still a little fuzzy on the details, but I think the situation is that the "natural" identity types of cubical type theory only satisfy the Id-elimination rule of Book HoTT (and MLTT) with a typal computation rule, but you can define a different family of identity types that satisfy it strictly.

    I believe that Book HoTT can be interpreted into cubical type theory. I’m still a little fuzzy on the details, but I think the situation is that the “natural” identity types of cubical type theory only satisfy the Id-elimination rule of Book HoTT (and MLTT) with a typal computation rule, but you can define a different family of identity types that satisfy it strictly.

71. • CommentRowNumber71.
    • CommentAuthorHarry Gindi
    • CommentTimeAug 9th 2017
    • (edited Aug 9th 2017)
    • PermaLink
    Author: Harry Gindi
    Format: MarkdownItex@Mike "Any two terms of the same identity type are propositionally equal" vs "Any two terms of the same identity type are homotopic" sound pretty similar to me, just that the homotopic one sounds like a weakening, so you have homotopy-extensionality instead of propositional extensionality. I would have thought that univalence is trivially satisfied, not traduced by extensionality. If it is computable, which you indicate that it is, I find it surprising and encouraging!

    @Mike “Any two terms of the same identity type are propositionally equal” vs “Any two terms of the same identity type are homotopic” sound pretty similar to me, just that the homotopic one sounds like a weakening, so you have homotopy-extensionality instead of propositional extensionality. I would have thought that univalence is trivially satisfied, not traduced by extensionality.

    If it is computable, which you indicate that it is, I find it surprising and encouraging!

72. • CommentRowNumber72.
    • CommentAuthorUrs
    • CommentTimeAug 9th 2017
    • (edited Aug 9th 2017)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> the “natural” identity types of cubical type theory only satisfy the Id-elimination rule of Book HoTT (and MLTT) with a typal computation rule, but you can define a different family of identity types that satisfy it strictly. Interesting. And you are saying that univalence computes does not actually depend on the identity types having this extra weakening? It should be exciting to translate book-HoTT proofs, like that of the generalized Blakers-Massey-theorem, to cubical HoTT and see them become programs that run.

    the “natural” identity types of cubical type theory only satisfy the Id-elimination rule of Book HoTT (and MLTT) with a typal computation rule, but you can define a different family of identity types that satisfy it strictly.

    Interesting. And you are saying that univalence computes does not actually depend on the identity types having this extra weakening?

    It should be exciting to translate book-HoTT proofs, like that of the generalized Blakers-Massey-theorem, to cubical HoTT and see them become programs that run.

73. • CommentRowNumber73.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI'm having trouble relating "Any two terms of the same identity type are homotopic" to anything resembling univalence. What is the connection there? Also, there's nothing intrinsically uncomputable about extensional type theory either. Axiom K can be made to compute by defining in terms of Agda-style generalized pattern matching, while [[observational type theory]] is a sort of 0-truncated version of homotopy/cubical type theory.

    I’m having trouble relating “Any two terms of the same identity type are homotopic” to anything resembling univalence. What is the connection there?

    Also, there’s nothing intrinsically uncomputable about extensional type theory either. Axiom K can be made to compute by defining in terms of Agda-style generalized pattern matching, while observational type theory is a sort of 0-truncated version of homotopy/cubical type theory.

74. • CommentRowNumber74.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> univalence computes does not actually depend on the identity types having this extra weakening? Well, the Id-elimination rules in cubical type theory are not primitive, but *defined* in terms of the cubical Kan compositions. If you define them in the straightforward way for the natural identity types, it's just a fact that what you get only satisfies a typal computation rule. But I think I've been told that if you are clever you can define a type that's equivalent (hence, by univalence, typally equal) but not judgmentally equal to the natural identity types, and define an Id-elimination operation for it that does happen to satisfy the judgmental computation rule. > It should be exciting to translate book-HoTT proofs, like that of the generalized Blakers-Massey-theorem, to cubical HoTT and see them become programs that run. Yes, there was a group at Snowbird working on this. I think they made some good progress. For a long time I was resistant to cubical type theory on philosophical and semantic grounds, but I'm gradually coming around.

    univalence computes does not actually depend on the identity types having this extra weakening?

    Well, the Id-elimination rules in cubical type theory are not primitive, but defined in terms of the cubical Kan compositions. If you define them in the straightforward way for the natural identity types, it’s just a fact that what you get only satisfies a typal computation rule. But I think I’ve been told that if you are clever you can define a type that’s equivalent (hence, by univalence, typally equal) but not judgmentally equal to the natural identity types, and define an Id-elimination operation for it that does happen to satisfy the judgmental computation rule.

    It should be exciting to translate book-HoTT proofs, like that of the generalized Blakers-Massey-theorem, to cubical HoTT and see them become programs that run.

    Yes, there was a group at Snowbird working on this. I think they made some good progress.

    For a long time I was resistant to cubical type theory on philosophical and semantic grounds, but I’m gradually coming around.

75. • CommentRowNumber75.
    • CommentAuthorUrs
    • CommentTimeAug 11th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Mike. That's very interesting. Assuming that book-HoTT does have an interpretation into cubical-HoTT, would this imply univalent models for book-HoTT in categories of cubical objects in a given sheaf topos?

    Thanks, Mike. That’s very interesting.

    Assuming that book-HoTT does have an interpretation into cubical-HoTT, would this imply univalent models for book-HoTT in categories of cubical objects in a given sheaf topos?

76. • CommentRowNumber76.
    • CommentAuthorMike Shulman
    • CommentTimeAug 11th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, I think so.

    Yes, I think so.

77. • CommentRowNumber77.
    • CommentAuthorspitters
    • CommentTimeAug 12th 2017
    • PermaLink
    Author: spitters
    Format: MarkdownItexAbout the judgemental J-rule; see section 9.1 of the [cubical paper](https://arxiv.org/abs/1611.02108). A confirmation of what Mike is saying. Re 75. No, we don't know yet whether this holds in general sheaf toposes. We know how to do the cubical model internal to some presheaf toposes. We have precise conditions in our paper on [guarded cubical type theory](https://arxiv.org/abs/1611.09263). [Orton and Pitts](http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf) provide axioms in the internal language of a topos sufficient for constructing the cubical model, but the main examples are presheaf models.

    About the judgemental J-rule; see section 9.1 of the cubical paper. A confirmation of what Mike is saying.

    Re 75. No, we don’t know yet whether this holds in general sheaf toposes. We know how to do the cubical model internal to some presheaf toposes. We have precise conditions in our paper on guarded cubical type theory. Orton and Pitts provide axioms in the internal language of a topos sufficient for constructing the cubical model, but the main examples are presheaf models.

78. • CommentRowNumber78.
    • CommentAuthorMike Shulman
    • CommentTimeAug 13th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI'm confused; I thought the original whole point of the cubical model was to be constructive, and if it is constructive then why can't you do it internally in any topos? (I think Orton and Pitts are doing something different, talking about presheaf topos that could replace the topos of cubical sets; here we're talking about starting from an arbitrary topos and taking cubical diagrams *in* that topos.)

    I’m confused; I thought the original whole point of the cubical model was to be constructive, and if it is constructive then why can’t you do it internally in any topos? (I think Orton and Pitts are doing something different, talking about presheaf topos that could replace the topos of cubical sets; here we’re talking about starting from an arbitrary topos and taking cubical diagrams in that topos.)

79. • CommentRowNumber79.
    • CommentAuthorspitters
    • CommentTimeAug 13th 2017
    • PermaLink
    Author: spitters
    Format: MarkdownItexSorry, you are right. What OP and we were doing is slightly different. About the cubical model, it's constructive in that it can be formalized in NuPrl, in CZF+universe, and possibly in other systems. The problem with toposes is that they do not have universes, and that the Hoffman-Streicher construction starts from a Grothendieck topos in Set. It is expected should not be a problem, but I am not sure whether anyone has worked out the details.

    Sorry, you are right. What OP and we were doing is slightly different.

    About the cubical model, it’s constructive in that it can be formalized in NuPrl, in CZF+universe, and possibly in other systems. The problem with toposes is that they do not have universes, and that the Hoffman-Streicher construction starts from a Grothendieck topos in Set. It is expected should not be a problem, but I am not sure whether anyone has worked out the details.

80. • CommentRowNumber80.
    • CommentAuthorMike Shulman
    • CommentTimeAug 14th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGrothendieck toposes all have universes, though, don't they? #75 was about "sheaf toposes", i.e. Grothendieck ones.

    Grothendieck toposes all have universes, though, don’t they? #75 was about “sheaf toposes”, i.e. Grothendieck ones.

81. • CommentRowNumber81.
    • CommentAuthorUrs
    • CommentTimeAug 14th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Grothendieck toposes all have universes That's a surprising statement to me. Could you elaborate? They have universes for propositions, but a universe for 0-truncated objects would have to be non-0-truncated, no?

    Grothendieck toposes all have universes

    That’s a surprising statement to me. Could you elaborate? They have universes for propositions, but a universe for 0-truncated objects would have to be non-0-truncated, no?

82. • CommentRowNumber82.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 14th 2017
    • (edited Aug 14th 2017)
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexPresumably as long as there are enough universes in the base category of sets? And I take the statement to mean the ordinary kind of Grothendieck universe.

    Presumably as long as there are enough universes in the base category of sets? And I take the statement to mean the ordinary kind of Grothendieck universe.

83. • CommentRowNumber83.
    • CommentAuthorspitters
    • CommentTimeAug 14th 2017
    • PermaLink
    Author: spitters
    Format: MarkdownItexMike, the construction of the universe in cubical sets depends on the Hoffman-Streicher construction, which depends on a Grothendieck universe in (classical) set. There does not seem to be a published account of iterating the Hoffman-Streicher construction. I.e. starting from a Grothendieck universe in Set, make a universe in the sheaf topos, and use that to make another Hoffman-Streicher universe for the internal cubical sets. It's likely that this can indeed be iterated. (In fact, I seem to recall a discussion with Thierry in which he checked that it actually works.)

    Mike, the construction of the universe in cubical sets depends on the Hoffman-Streicher construction, which depends on a Grothendieck universe in (classical) set. There does not seem to be a published account of iterating the Hoffman-Streicher construction. I.e. starting from a Grothendieck universe in Set, make a universe in the sheaf topos, and use that to make another Hoffman-Streicher universe for the internal cubical sets. It’s likely that this can indeed be iterated. (In fact, I seem to recall a discussion with Thierry in which he checked that it actually works.)

84. • CommentRowNumber84.
    • CommentAuthorUrs
    • CommentTimeAug 14th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexOh, I see, universes in that sense. Never mind #81

    Oh, I see, universes in that sense. Never mind #81

85. • CommentRowNumber85.
    • CommentAuthorMike Shulman
    • CommentTimeAug 14th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe Hoffmann-Streicher universe is just defined by Yoneda, right? Surely it should be perfectly constructive.

    The Hoffmann-Streicher universe is just defined by Yoneda, right? Surely it should be perfectly constructive.

86. • CommentRowNumber86.
    • CommentAuthorspitters
    • CommentTimeAug 14th 2017
    • PermaLink
    Author: spitters
    Format: MarkdownItexI believe I was looking at p9 of [this note](http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/UniTop.pdf) by Thomas Streicher. If there was a trivial internal version for sheaf toposes, I would have expected Thomas to state it. In any case, I you have a complete argument in mind, it might be worth recording it, as it seems to be lacking from the literature at the moment. I might try to do it myself later, but I am on holiday now.

    I believe I was looking at p9 of this note by Thomas Streicher. If there was a trivial internal version for sheaf toposes, I would have expected Thomas to state it. In any case, I you have a complete argument in mind, it might be worth recording it, as it seems to be lacking from the literature at the moment. I might try to do it myself later, but I am on holiday now.

87. • CommentRowNumber87.
    • CommentAuthorMike Shulman
    • CommentTimeAug 15th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWell, I don't have a surplus of time right now, and I'm not hugely motivated to put a lot of thought into this because internal cubical objects in sheaf 1-toposes are not a very interesting class of models for me. I suppose there might be some choicey issues regarding whether one wants the universe to classify things by actual pullbacks or only after passage to a cover. But couldn't one also note that cubical objects in a Grothendieck topos (over a classical base $Set$) are themselves again a Grothendieck topos over the same $Set$ and apply Streicher's construction directly?

    Well, I don’t have a surplus of time right now, and I’m not hugely motivated to put a lot of thought into this because internal cubical objects in sheaf 1-toposes are not a very interesting class of models for me. I suppose there might be some choicey issues regarding whether one wants the universe to classify things by actual pullbacks or only after passage to a cover. But couldn’t one also note that cubical objects in a Grothendieck topos (over a classical base $Set$) are themselves again a Grothendieck topos over the same $Set$ and apply Streicher’s construction directly?

88. • CommentRowNumber88.
    • CommentAuthorspitters
    • CommentTimeAug 30th 2017
    • PermaLink
    Author: spitters
    Format: MarkdownItexMike, re 87, > But couldn’t one also note that cubical objects in a Grothendieck topos (over a classical base Set) are themselves again a Grothendieck topos over the same Set and apply Streicher’s construction directly? Yes, we used a similar construction in our paper. I just want to point out that the theory of HS-universes is not as polished as one might like it to be.

    Mike, re 87,

    But couldn’t one also note that cubical objects in a Grothendieck topos (over a classical base Set) are themselves again a Grothendieck topos over the same Set and apply Streicher’s construction directly?

    Yes, we used a similar construction in our paper. I just want to point out that the theory of HS-universes is not as polished as one might like it to be.