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

DOI10.1017/S0960129520000316zbMath1496.03003OpenAlexW3174180696MaRDI QIDQ5084306

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

univalencegroupoidstype theory

Mathematics Subject Classification ID

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

Uses Software

• LEGO
• Cubical agda

Cites Work

• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Unnamed Item
• Unnamed Item
• Unnamed Item

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