HackerPapers

arXiv:0808.2122math.LO

Two-dimensional models of type theory

Richard Garner

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

Abstract

We describe a non-extensional variant of Martin-Löf type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.

arXiv comments
46 pages; v2: final journal version
Journal reference
Mathematical Structures in Computer Science 19 (2009), no. 4, pages 687--736
DOI
doi:10.1017/S0960129509007646
Subjects
math.LOLogic math.CTCategory Theory

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Dec 2021 to Dec 2021.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. The HoTT Game 1 comment

    • I don't know what proof is used here, but the standard proof uses univalence to upgrade the equivalence (_ + 1): Z -> Z to a path Z = Z. Then we use induction for S^1 to define the map S^1 -> U that takes the base point to Z and the loop to the path Z = Z. Having the fundamental…

      scappView on HNParent context

Submitted to Hacker News

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