Abstract: We investigate the injective types and the algebraically injective types in univalent mathematics, both in the absence and in the presence of propositional resizing. Injectivity is defined by the surjectivity of the restriction map along any embedding, and algebraic injectivity is defined by a given section of the restriction map along any embedding. Under propositional resizing axioms, the main results are easy to state: (1) Injectivity is equivalent to the propositional truncation of algebraic injectivity. (2) The algebraically injective types are precisely the retracts of exponential powers of universes. (2a) The algebraically injective sets are precisely the retracts of powersets. (2b) The algebraically injective -types are precisely the retracts of exponential powers of universes of -types. (3) The algebraically injective types are also precisely the retracts of algebras of the partial-map classifier. From (2) it follows that any universe is embedded as a retract of any larger universe. In the absence of propositional resizing, we have similar results which have subtler statements that need to keep track of universe levels rather explicitly, and are applied to get the results that require resizing.
Recommendations
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
- Univalent semantics of constructive type theories
- Inductive types in homotopy type theory
- scientific article; zbMATH DE number 1424016
- Theory of dependent types and axiom of univalence
- Mathesis Universalis and Homotopy Type Theory
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 7204300
- Categorical structures for type theory in univalent foundations
- A general theory of types for nonsingular injective modules
Cites work
- An experimental library of formalized mathematics based on the univalent foundations
- Equipping weak equivalences with algebraic structure
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 19494 (Why is no real title available?)
- Idempotents in intensional type theory
- Injective power objects and the axiom of choice
- Interacting with Modal Logics in the Coq Proof Assistant
- Partial elements and recursion via dominances in univalent type theory
- Univalence for inverse diagrams and homotopy canonicity
This page was built for publication: Injective types in univalent mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5156770)
