{"id":54,"date":"2024-03-15T03:44:40","date_gmt":"2024-03-15T03:44:40","guid":{"rendered":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/?p=54"},"modified":"2024-03-15T03:44:40","modified_gmt":"2024-03-15T03:44:40","slug":"discussing-a-mechanization-of-the-blakers-massey-connectivity-theorem-in-homotopy-type-theory","status":"publish","type":"post","link":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/03\/15\/discussing-a-mechanization-of-the-blakers-massey-connectivity-theorem-in-homotopy-type-theory\/","title":{"rendered":"Discussing \u201cA Mechanization of the Blakers\u2013Massey Connectivity Theorem in Homotopy Type Theory\u201d"},"content":{"rendered":"\n

(Link)<\/a><\/p>\n\n\n\n

Authors:<\/strong> Kuen-Bang Hou (Favonia) (Carnegie Mellon University), Eric Finster (\u00c9cole Polytechnique), Daniel R. Licata (Wesleyan University), and Peter LeFanu Lumsdaine (Stockholm University)<\/p>\n\n\n\n

Reference:<\/strong> Hou, K. B., Finster, E., Licata, D. R., & Lumsdaine, P. L. (2016). A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory. In Proceedings of the 31st annual ACM\/IEEE symposium on logic in computer science (LICS 2016) (pp. 565-574)<\/p>\n\n\n\n

Why this paper?<\/strong> Cited by Automating Boundary Filling in Cubical Agda<\/a> and Strange new universes: Proof assistants and synthetic foundations<\/a><\/p>\n\n\n\n

I first became aware of this paper from a long and fascinating blog comment thread<\/a> in which mathematicians argued about the utility, or lack thereof, of homotopy type theory<\/a> for homotopy theorists. Urs Schreiber, arguing for team HoTT, held up this paper an exemplar of the value of the type theoretical approach, saying \u201cit was remarkable to see a complete homotopy theory newbie, who had the proof in HoTT, explain it to none less than Charles Rezk, who said he had tried to find it using traditional means but failed\u201d.<\/p>\n\n\n\n

This paper occupies the same genre as the Brunerie thesis<\/a> I read about a year ago, as it re-proves a known homotopy theoretic result (this one from the 1950s) in synthetic style using type theory. Because of the synthetic treatment, the result is transferrable to any \u221e-topos (this generality is what is heralded as \u2018new\u2019 in the Schreiber quote above). Like Brunerie\u2019s work, the proof is \u201cessentially new\u201d rather than merely a translation of existing work to a different language. Unlike Brunerie\u2019s work, which was a tour de force of pen-and-paper type theory, this work is entirely formalised, using the proof assistant Agda.<\/p>\n\n\n\n

I was familiar going into this paper about the notion of truncation<\/em>. In type theory one has identities between elements, but because identities are themselves elements of an identity type, one also has identities between identities, and so forth. A type is n<\/em>-truncated, or simply an n<\/em>-type, if at every level above n<\/em> the identities are trivial. For example a set is a 0<\/em>-type, as while it may be non-trivial at level 0<\/em> (some sets have multiple elements which are not equal) it is trivial above that level (there is only one way for an element to be equal to itself). Connectivity<\/em> is the dual notion to truncation: elements are trivial below a certain level. This extends to connectivity of a map between types; to say that such a map is n<\/em>-connected is to (very roughly) say that it shows the two types to be equivalent up to level n<\/em>.<\/p>\n\n\n\n

The Blakers\u2013Massey theorem is about the connectivity of certain maps used in the definition of a pushout<\/em>, a construction similar to a disjoint union but also featuring some \u2018glue\u2019 that joins some elements together. The canonical example is defining the integers as two copies of the natural numbers glued together at their zeros. The theorem is apparently greatly useful for describing the algebraic structure of the higher levels of some examples in homotopy theory, which in general is an extremely hard problem. \u00a0This paper in fact offers two proofs, one more homotopy theory flavoured version which goes via a detour through a special case of pushout called a wedge, the other a more type theoretically pure version that avoid this detour, which is slightly shorter but more reliant on computations which are hard to explain on paper.<\/p>\n","protected":false},"excerpt":{"rendered":"

I first became aware of this paper from a long and fascinating blog comment thread in which mathematicians argued about the utility, or lack thereof, of homotopy type theory for homotopy theorists. Urs Schreiber, arguing for team HoTT, held up this paper an exemplar of the value of the type theoretical approach, saying \u201cit was remarkable to see a complete homotopy theory newbie, who had the proof in HoTT, explain it to none less than Charles Rezk, who said he had tried to find it using traditional means but failed\u201d.<\/p>\n","protected":false},"author":10,"featured_media":55,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":"","_share_on_mastodon":"0","_share_on_mastodon_status":"My #blog this week is on the Blakers-Massey theorem, whose proof in homotopy type theory #HoTT is one of the key achievements of that community. %permalink% #TypeTheory #HomotopyTheory"},"categories":[5],"tags":[65,61,59,62,58,68,67,57,66,60,64,63],"class_list":["post-54","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-summaries","tag-65","tag-carnegie-mellon-university","tag-daniel-r-licata","tag-ecole-polytechnique","tag-eric-finster","tag-homotopy-theory","tag-homotopy-type-theory","tag-kuen-bang-hou-favonia","tag-lics","tag-peter-lefanu-lumsdaine","tag-stockholm-university","tag-wesleyan-university"],"share_on_mastodon":{"url":"https:\/\/fediscience.org\/@RanaldClouston\/112097642485555589","error":""},"_links":{"self":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/54","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/users\/10"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/comments?post=54"}],"version-history":[{"count":1,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/54\/revisions"}],"predecessor-version":[{"id":56,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/54\/revisions\/56"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/media\/55"}],"wp:attachment":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/media?parent=54"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/categories?post=54"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/tags?post=54"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}