Injective types in univalent mathematics
From MaRDI portal
Publication:5156770
DOI10.1017/S0960129520000225zbMath1478.18025arXiv1903.01211OpenAlexW3120571129WikidataQ114116581 ScholiaQ114116581MaRDI QIDQ5156770
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
Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)
Related Items (1)
Uses Software
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