The groupoid interpretation of type theory

By M. Hofmann, T. Streicher. 1998

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

1. Benedikt Ahrens
2. Ralph Matthes
3. David A. McAllester
4. Richard Garner
5. Benno van den Berg
6. Behnam Neyshabur
7. Olivier Catoni
8. Yevgeny Seldin

Citations in the corpus

• Heterogeneous substitution systems revisited (2016, positive): “The next lemma is originally due to Hofmann and Streicher [19]; and is also proved in Thm. 4.5 of [7]: The category of hss contains all the isomorphisms of the category of ( Id + H ) - algebras, for which source and target are substitution systems.”
• Types are weak ω‐groupoids (2008, background): “Whilst attempts to make this link precise have only borne fruit in the past few years [1, 7, 9, 19], the basic idea dates back to an observation made by Hofmann and Streicher in [11].”
• Constructing categories and setoids of setoids in type theory (2014, unknown): “The root of the problem is that the intensional identity type of MLTT induces a non-trivial groupoid structure on types [8].”
• MathZero, The Classification Problem, and Set-Theoretic Type Theory (2020, methodology): “Isomorphism was handled at an abstract level in the groupoid model of type theory [3].”
• The simplicial model of Univalent Foundations (after Voevodsky) (2012, unknown): “Other methods exist for certain specific categories ([HS98], [War08]), but are not applicable to the present case.”