<story><title>Introduction to Homotopy Type Theory</title><url>https://arxiv.org/abs/2212.11082</url></story><parent_chain><item><author>spekcular</author><text>I realize it&amp;#x27;s Christmas Eve, but this post tempts my inner curmudgeon.&lt;p&gt;I do not understand why homotopy type theory posts are so popular on this website. My view is that all the &amp;quot;philosophical&amp;quot; arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play. Further, the &amp;quot;practical&amp;quot; arguments in terms of facilitating formalization are not so compelling given the HoTT people haven&amp;#x27;t actually (as far as I know) formalized much mathematics - whereas (seemingly) less ideological communities like users of Lean have made great progress.&lt;p&gt;To expand on the comment about the philosophical arguments: take for example the abstract of this article. It states:&lt;p&gt;&amp;gt; It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal.&lt;p&gt;It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.&lt;p&gt;Also, more to the point: ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.</text></item></parent_chain><comment><author>ebingdom</author><text>&amp;gt; I do not understand why homotopy type theory posts are so popular on this website.&lt;p&gt;Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming language that is capable of expressing both programs and proofs, such that you can prove your code correct in the same language. Hacker News is a mostly technical community that often likes to geek out on programming languages.&lt;p&gt;Homotopy type theory is an especially cool flavor of type theory that finally gives a satisfying answer to the question of when two types should be considered propositionally equal.</text></comment>
<story><title>Introduction to Homotopy Type Theory</title><url>https://arxiv.org/abs/2212.11082</url></story><parent_chain><item><author>spekcular</author><text>I realize it&amp;#x27;s Christmas Eve, but this post tempts my inner curmudgeon.&lt;p&gt;I do not understand why homotopy type theory posts are so popular on this website. My view is that all the &amp;quot;philosophical&amp;quot; arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play. Further, the &amp;quot;practical&amp;quot; arguments in terms of facilitating formalization are not so compelling given the HoTT people haven&amp;#x27;t actually (as far as I know) formalized much mathematics - whereas (seemingly) less ideological communities like users of Lean have made great progress.&lt;p&gt;To expand on the comment about the philosophical arguments: take for example the abstract of this article. It states:&lt;p&gt;&amp;gt; It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal.&lt;p&gt;It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.&lt;p&gt;Also, more to the point: ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.</text></item></parent_chain><comment><author>zmgsabst</author><text>&amp;gt; So I am skeptical of any approach that wants to blur those distinctions.&lt;p&gt;HoTT doesn’t blur those distinctions — it formalizes the distinction.&lt;p&gt;The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.&lt;p&gt;The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)&lt;p&gt;&amp;gt; ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.&lt;p&gt;Counterpoint: no it doesn’t, because almost every working mathematician uses a higher level type theory in their work that “compiles” to ZFC and will run away screaming if you try to make them compile their work down to formal ZFC statements because set theory is a garbage foundation — the worst of the three options.&lt;p&gt;“My axioms do everything but formalize proofs!” is the equivalent of “my car does everything but drive!”</text></comment>