Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

(0 1)-category-theory 2-category 2-category-theory 2-monad abelian-categories accessible adjoint algebra algebraic algebraic-geometry analysis arithmetic beauty book bug bundle categories category category-theory chern-simons-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics complex-geometry conference connection constructive constructive-mathematics cosmology database deformation-theory descent differential differential-cohomology differential-geometry duality enriched enriched-category-theory enrichment examples factorization-system fiber fibration forms foundation foundations functional-analysis functor galois-theory gauge-theory gebra general topology geometric geometric-quantization geometry gravity group-theory higher higher-algebra higher-category-theory higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory homtopy-type-theory infinity-groupoid integration-theory internal-categories kan lie lie-algebras lie-theory limit limits linear linear-algebra locale localization localization-theory logic manifolds mathematics measure measure-theory mechanics meta modal-logic model model-category-theory monoidal monoidal-category monoidal-category-theory morphism n-groups newpage noncommutative noncommutative-geometry object operator operator-algebra order-theory philosophy physics predicative pretopology pro-object probability-theory quantum quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry set set-theory sheaf simplicial site space stable-homotopy-theory stack string string-theory subobject supergeometry symplectic-geometry tannaka tensor terminology theory topologica-quantum-field-theory topology topos topos-theory torsor tqft type type-theory universal weighted-limit

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

   $$\begin{array}{ccc}B& \stackrel{f}{\to }& X\\ \downarrow & \nearrow & \downarrow \\ 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.]

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 $𝒞$, 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.

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{]}_{𝒞{/}_{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 $\mathrm{sSet}$ (not necessarily universal) are, up to equivalence, precisely the canonical associated infinity-bundles which are associated to $\mathrm{Aut}(F)$-principal $\mathrm{\infty }$-bundles, namely the fibrations

    $$F\hookrightarrow \mathrm{B}(*,\mathrm{Aut}(F),F)\stackrel{p_F}{\to }\mathrm{B}(*,\mathrm{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(*,\mathrm{Aut}(F),F)\to B(*,\mathrm{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 $\mathrm{\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 $(\mathrm{\infty }\mathrm{,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 $(\mathrm{\infty }\mathrm{,1})$-toposes associated $\mathrm{\infty }$-bundles?

    Do we have an argument for this in the context of $(\mathrm{\infty }\mathrm{,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 \mathrm{Eq}(E)$ is an equivalence if it induces an equivalence on all hom-$\mathrm{\infty }$-groupoids $\mathrm{Hom}(X,B^I)\to \mathrm{Hom}(X,\mathrm{Eq}(E))$, which is a fiberwise map over $\mathrm{Hom}(X,B\times B)$. For a given map $(f,g):X\to B\times 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}(X,B)}(f,g)$, while lifts to $\mathrm{Eq}(E)$ form the space $\mathrm{Core}(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 \mathrm{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 $\mathrm{\infty }$-topos theoretic sense.

    In $\mathrm{\infty }\mathrm{Grpd}$ I know how to prove that the $\kappa$-small object classifier is $\mathrm{Core}(\mathrm{\infty }{\mathrm{Grpd}}_{\kappa })\simeq {\coprod }_{\mathrm{homotopy}\mathrm{types}[F]}B\mathrm{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 $\mathrm{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](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.