Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
stub for homotopy type theory
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.
I linked the Coq wiki.
uploaded a pdf with the basic HoTT-Coq code documentation, linked to now from homotopy type theory.
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).
I have further brushed up and expanded the dictionary, now with more comments on identity types.
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.
Thanks!
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.
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”?
I mean the google group. You can configure google groups to act like mailing lists.
Ah, okay, thanks. Yes, I am subscribed to the HoTT google list by email, so I know that one. Thanks.
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.
The reason it’s missing is that I don’t know the answer!
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…”?
While many statements from ordinary category theory generalize essentially verbatim to $(\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 : A \to B$ is a (-1)-truncated object in the slice over $B$. Similarly an $\infty$-truncated object in the slice is just any old morphism. So the $n$-truncated objects in the slice are close to being monomorphisms (“$n$ steps close”!) but are not quite monomorphisms.
What does generalize is the following characterization of monos: in ordinary category theory a morphism $f : A \to B$ is a mono precisely if its diagonal $A \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 $n$-truncated precisely if its diagonal is (n-1)-truncated.
[edit: for the discussion of the recursion principle see here]
Ah, I forgot state the punchline:
so if $X$ is an $n$-truncated object, then $X \to *$ is $n$-truncated, and so the diagonal $X \to X \times X$ is (n-1)-truncated.
So the diagonal on an object $X$ is a mono precisely if the object is 0-truncated (is an h-set)!
I have added that remark at n-truncated object of an (infinity,1)-category at Examples-Diagonals
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!
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.
(Incidentally, there are separate articles fully faithful (infinity,1)-functor and full and faithful (infinity,1)-functor, both describing, I believe, the same concept…)
Thanks for noticing that! Discuss here.
So how truncated is a split mono in an $(\infty,1)$-category, and why don’t we call that a mono instead?
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 $(\infty,1)$-category. $(-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.
A split monomorphism is an $(n,1)$-category will be $(n-2)$-truncated, so in an $(\infty,1)$-category, that tells us nothing, is that right?
@Toby: that seems right.
In particular, a split mono in a $(0,1)$-category (a poset) is $(-2)$-truncated (an iso). Good, that makes me feel happy about it.
I’ve added a remark along these lines to split monomorphism.
Cool. Can I proselytise that a $(0,1)$-category is a poset while a proset is a strict $(0,1)$-category?
Sure.
added a pointer to the recent
to the list of references at homotopy type theory.
Added to the list of References at homotopy type theory a pointer to the new
Earlier I had added more pointers at univalence on univalence in the cubical set model by Coquand and Huber.
Added to the references a pointer to Voevodsky’s latest talk (pdf)
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)
have added pointer to Shulman 16
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.
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.
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.
Hey anqurvanillapy – thanks for your attention to blemishes and for repairing them. Just a friendly note to say that small typo corrections really don’t need to be announced at the nForum. You can leave the description box blank when you make such corrections at the nLab.
What is Axiom R? The link to Shulman 15 doesn’t work. It seems to link to some subsection in cohesive homotopy type theory.
Someone typed a slash instead of a #
, I’ve fixed it.
That last comment mystified me. It means to refer to What I Wish I Knew When Learning HoTT
added pointer to
1 to 54 of 54