Martin Hofmann’s contributions to type theory: Groupoids and univalence

DOI10.1017/S0960129520000316MaRDI QIDQ5084306zbMATH OpenOpenAlexFDO

Authors Thorsten Altenkirch

Publication date 24 June 2022

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129520000316

zbMATH Keywords

groupoidstype theoryunivalence

Mathematics Subject Classification ID

Biographies, obituaries, personalia, bibliographies (01A70) History of mathematical logic and foundations (03-03) Type theory (03B38)

Recommendations

• scientific article; zbMATH DE number 1302059
• scientific article; zbMATH DE number 3853066
• Homotopy type theory and Voevodsky's univalent foundations
• Categorical and algebraic aspects of Martin-Löf type theory
• Remarks on Martin-Löf's partial type theory
• Mathesis Universalis and Homotopy Type Theory
• Homotopy type theory. Univalent foundations of mathematics
• The strict \(\omega\)-groupoid interpretation of type theory
• Introduction -- from type theory and homotopy theory to univalent foundations
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY

Cites work

• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)

Cited in

(3)

• The strict \(\omega\)-groupoid interpretation of type theory
• Homotopy theoretic models of identity types
• Generalizations of Hedberg's theorem

Describes a project that uses

Uses Software

• LEGO
• Cubical Agda

This page was built for publication: Martin Hofmann’s contributions to type theory: Groupoids and univalence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5084306)