Injective types in univalent mathematics

DOI10.1017/S0960129520000225zbMath1478.18025arXiv1903.01211OpenAlexW3120571129WikidataQ114116581 ScholiaQ114116581MaRDI QIDQ5156770

Martín Hötzel Escardó

Publication date: 11 October 2021

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

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

zbMATH Keywords

univalence axiomKan extensionunivalent mathematicsflabby typeinjective typepartial-map classifier

Mathematics Subject Classification ID

Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (1)

InjectiveTypes

Uses Software

• Coq
• Agda
• GitHub

Cites Work

• Unnamed Item
• Injective power objects and the axiom of choice
• Equipping weak equivalences with algebraic structure
• Idempotents in intensional type theory
• Interacting with Modal Logics in the Coq Proof Assistant
• Partial Elements and Recursion via Dominances in Univalent Type Theory.
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalence for inverse diagrams and homotopy canonicity
• An experimental library of formalized Mathematics based on the univalent foundations

This page was built for publication: Injective types in univalent mathematics