Idempotents in intensional type theory

DOI10.2168/LMCS-12(3:9)2016zbMath1445.03011arXiv1507.03634MaRDI QIDQ2974780

Michael Shulman

Publication date: 11 April 2017

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1507.03634

zbMATH Keywords

idempotentMartin-Löf type theoryunivalence axiomdependent type theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40) Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60)

Related Items (4)

Strange new universes: Proof assistants and synthetic foundations ⋮ On Small Types in Univalent Foundations ⋮ Indexed type theories ⋮ Injective types in univalent mathematics

Uses Software

• Coq
• HoTT
• GitHub
• MathOverflow

Cites Work

• Homotopy type theory and Voevodsky’s univalent foundations
• Voevodsky’s Univalence Axiom in Homotopy Type Theory
• Eilenberg-MacLane spaces in homotopy type theory
• Type Theory and Homotopy
• Higher Topos Theory (AM-170)

This page was built for publication: Idempotents in intensional type theory