HackerPapers

arXiv:1601.05035math.LO

Homotopy Type Theory: A synthetic approach to higher equalities

Michael Shulman

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

This is an introduction to Homotopy Type Theory and Univalent Foundations for philosophers, written as a chapter for the book "Categories for the Working Philosopher" (ed. Elaine Landry)

arXiv comments
16 pages. v2: fixed internal cross-references. v3: added sentence introducing refl
Journal reference
DOI
Subjects
math.LOLogic math.CTCategory Theory

On Hacker News

Linked by 1 identifiable commenter in 2 comments across 2 threads, from Oct 2021 to Oct 2021.

Comments linking this paper, per year.

Discussed in comments2 threads

  1. Adventures in Category Theory – The algebra of types (2018) 1 comment

    • I would recommend this introduction to type theory: https://arxiv.org/abs/1601.05035. While it's about HoTT, it starts with a very clear general-audience explanation on why and how type theory is different from set theory.

      4adView on HNParent context

  2. Where do type systems come from? (2017) 1 comment

    • At the risk of more confusion https://ncatlab.org/nlab/show/intensional+type+theory. As a gentle introduction to modern type theory I would recommend https://arxiv.org/abs/1601.05035.

      4adView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.