Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeApr 7th 2011
    • (edited Oct 30th 2012)
    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2011

    Have added to homotopy type theory a paragraph on machine implementation and some more links in the References-section. Also started a page Coq, but more than stubby for the moment.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeOct 31st 2011

    I linked the Coq wiki.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2011

    uploaded a pdf with the basic HoTT-Coq code documentation, linked to now from homotopy type theory.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2011
    • (edited Nov 10th 2011)

    Added to the References/Code section at homotopy type theory a pointer to the Proviola-HoTT archive which offers HTML-functionality that displays the proofs in the code (which otherwise is only visible when loading the code into Coq itself).

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2011

    I have further brushed up and expanded the dictionary, now with more comments on identity types.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2011

    I edited the Idea section at homotopy type theory some.

    By the way, Urs, I’m really grateful for all the stuff you’ve been writing on the nLab about HoTT! I’ve just been too caught up with figuring stuff out to read it carefully. But I’m going to try to find some time to look it over and make tweaks.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2011

    Thanks!

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2011

    I’ve edited homotopy type theory some more, clarifying the dictionary a bit and adding a section “Advantages” after a discussion on the HoTT mailing list.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2011

    discussion on the HoTT mailing list.

    Is this a public list? I once tried to find it, but all I ended up finding was a Coq mailing list and the HoTT Google-group. If you don’t mean one of these two, could you tell me if there is a way for me to subscribe to “the HoTT mailing list”?

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2011

    I mean the google group. You can configure google groups to act like mailing lists.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2011

    Ah, okay, thanks. Yes, I am subscribed to the HoTT google list by email, so I know that one. Thanks.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    Mike,

    a question out of curiosity, concerning the triple of correspondences on slide 4, part I of your Swansea notes:

    evidently there is one item missing to complete the picture: what would be the text in red to go in item 1?

    What is the homotopy-version of “A programming language”?

    I did ask somebody else this question. He wasn’t entirely sure but did make an educated guess that sounded interesting. But I have entirely forgotten now what that answer was, unfortunately.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2012

    The reason it’s missing is that I don’t know the answer!

    • CommentRowNumber15.
    • CommentAuthorSridharRamesh
    • CommentTimeMay 10th 2012

    Another question: In the same set of slides, you say at one point “Diagonals in higher categories are not monic!”. How do I square this with my naive, 1-categorical style of thought “But, diagonals followed by projections are identity, and thus diagonals must surely be (split) monic…”?

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    While many statements from ordinary category theory generalize essentially verbatim to (,1)(\infty,1)-category theory, the notions of monomorphisms and epimorphisms form the big exception. Instead of generalizing straightforwardly, these notions split up each into a tower of notions: a monomorphism f:ABf : A \to B is a (-1)-truncated object in the slice over BB. Similarly an \infty-truncated object in the slice is just any old morphism. So the nn-truncated objects in the slice are close to being monomorphisms (“nn steps close”!) but are not quite monomorphisms.

    What does generalize is the following characterization of monos: in ordinary category theory a morphism f:ABf : A \to B is a mono precisely if its diagonal AA× BAA \to A \times_B A is an isomorphism. Now, isomorphisms are the (-2)-truncated morphisms. So this says that a morphism is (-1)-truncated if its diagonal is (-2)-truncated.

    This does generalize to a recursive characterization: a morphisms is nn-truncated precisely if its diagonal is (n-1)-truncated.

    [edit: for the discussion of the recursion principle see here]

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    Ah, I forgot state the punchline:

    so if XX is an nn-truncated object, then X*X \to * is nn-truncated, and so the diagonal XX×XX \to X \times X is (n-1)-truncated.

    So the diagonal on an object XX is a mono precisely if the object is 0-truncated (is an h-set)!

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2012

    Also to address Sridhar’s last question directly: in a higher category, a “split monic” (a morphism admitting a retraction) is not necessarily a monic!

    • CommentRowNumber20.
    • CommentAuthorSridharRamesh
    • CommentTimeMay 11th 2012
    • (edited May 11th 2012)

    Ah, I see now. Between sets, a functor admitting a retraction must be full and faithful, but between nontrivial groupoids, this needn’t be the case (e.g., the map from 1 into the delooping of Z). So in a 1-category, “split monics” are monics, but in a higher category, they needn’t be.

    • CommentRowNumber21.
    • CommentAuthorSridharRamesh
    • CommentTimeMay 11th 2012
    • (edited May 11th 2012)

    (Incidentally, there are separate articles fully faithful (infinity,1)-functor and full and faithful (infinity,1)-functor, both describing, I believe, the same concept…)

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2012

    Thanks for noticing that! Discuss here.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeMay 13th 2012

    So how truncated is a split mono in an (,1)(\infty,1)-category, and why don’t we call that a mono instead?

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2012

    In general, I don’t see any reason for it to be at all truncated, although I can’t think of a counterexample off the top of my head.

    Of course there’s a choice for what we want to call a “mono” in an (,1)(\infty,1)-category. (1)(-1)-truncated morphisms have many of the usual properties of monomorphisms, and are the natural way to interpret propositions as some types in HoTT, so that’s some justification for giving them the unadorned name.

    • CommentRowNumber25.
    • CommentAuthorTobyBartels
    • CommentTimeMay 13th 2012

    A split monomorphism is an (n,1)(n,1)-category will be (n2)(n-2)-truncated, so in an (,1)(\infty,1)-category, that tells us nothing, is that right?

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2012

    @Toby: that seems right.

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeMay 13th 2012

    In particular, a split mono in a (0,1)(0,1)-category (a poset) is (2)(-2)-truncated (an iso). Good, that makes me feel happy about it.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2012

    I’ve added a remark along these lines to split monomorphism.

    • CommentRowNumber29.
    • CommentAuthorTobyBartels
    • CommentTimeMay 14th 2012

    Cool. Can I proselytise that a (0,1)(0,1)-category is a poset while a proset is a strict (0,1)(0,1)-category?

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2012

    Sure.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeOct 30th 2012

    added a pointer to the recent

    to the list of references at homotopy type theory.

    • CommentRowNumber32.
    • CommentAuthorTobias Fritz
    • CommentTimeFeb 5th 2013
    I fixed a broken link pointing to Mike's old webpage.
    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2014
    • (edited Jan 3rd 2014)

    Added to the list of References at homotopy type theory a pointer to the new

    • Vladimir Voevodsky, Experimental library of univalent formalization of mathematics (arXiv:1401.0053)

    Earlier I had added more pointers at univalence on univalence in the cubical set model by Coquand and Huber.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2014
    • (edited Mar 27th 2014)

    Added to the references a pointer to Voevodsky’s latest talk (pdf)

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2014

    Of course I have added

    to a bunch of related entries (including homotopy type theory, cubical set, univalence, relation between category theory and type theory)

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2016

    have added pointer to Shulman 16

    • CommentRowNumber37.
    • CommentAuthorAnthony Bordg
    • CommentTimeDec 16th 2017
    I added Dan Grayson's preprint "An introduction to univalent foundations for mathematicians" in the References section.
    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2018

    Added pointer to Mike’s “Homotopy type theory: the logic of space”.

    diff, v98, current

    • CommentRowNumber39.
    • CommentAuthorErnesto
    • CommentTimeMay 8th 2018
    I don't know if this is the right place to ask questions I have about HoTT book. Any way, here I go:
    In chapter 9, Category theory, page 314, Lemma 9.2.9. states that composition of functors is associative. Why do we need the coherence of this lemma? I am not sure what is the meaning of 'coherence' here and why the pentagon of equalities that follows should commutes.
    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeMay 8th 2018

    Welcome Ernesto! Coherence here is meant in the same sense as coherence in a monoidal category or bicategory: associativity doesn’t hold on the nose, but coherence of the isomorphisms/paths witnessing associativity means that we don’t usually need to worry about applying them explicitly. MacLane’s coherence theorem for monoidal categories (there is a similar theorem for bicategories etc.) says that once that pentagon and triangle commute, then “all diagrams” of associativity and unit isomorphisms also commute. Thus, whenever we have two composites that differ from each other by some reassociations, we don’t need to worry about how we do the reassociation to get from one to the other; there is an essentially unique way to do it.

    In general, a good place to ask questions about the HoTT book is the hott-cafe mailing list.

    • CommentRowNumber41.
    • CommentAuthorErnesto
    • CommentTimeMay 9th 2018
    Thank you Mike, sorry to bother you in this forum. I'll keep asking question about the same subject in hott-cafe mailing list.
    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeMay 9th 2018

    I didn’t mean that the nForum was a bad place to ask questions; I’m sorry if it sounded that way. This particular thread is mainly for discussion about the nLab page homotopy type theory, but the nForum as a whole is for talking about all kinds of “Math, physics, and philosophy” and this sort of question is fine here. I just mentioned hott-cafe because it’s more focused on the particular subject and on exactly this sort of question, so you may find more people there than here who have helpful things to say.

    • CommentRowNumber43.
    • CommentAuthorErnesto
    • CommentTimeMay 9th 2018
    Thank you very much, I am very grateful for your answer.. I begun asking questions in hott cafe about composition of functors but I rephrased it here;

    I want to know if this is neccesary (coherence) because of the way functors and their composition were defined, or if there is a way to define functors and their composition in homotopy type theory in such a way that we do not have to worry about coherence. For instance, if functors were simple functions with an additional condition we have associativity automatically without going into coherence once we check that the composition satisfies the additiional condition, or not? ( Composition of functions is associative and therefore composition of linear functions is associative because composition of linear functions is a linear function).
    • CommentRowNumber44.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2018

    Composition of functions is associative and therefore composition of linear functions is associative because composition of linear functions is a linear function

    Right, but it’s not associative up to definitional equality, because the proof of linearity is carried along as part of the notion of “linear function”. Any two proofs of linearity are equal, because being linear is a proposition, but not necessarily definitionally equal. The situation is the same for functors: the function on objects and the function on morphisms have definitionally associative composition, but the proofs of functoriality don’t. The reason coherence doesn’t arise for linear functions is that vector spaces are sets (0-types), so coherence holds automatically: any diagram of equalities in a vector space commutes.