Projective types
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2023-02-06.
Last modified on 2023-11-24.
module foundation.projective-types where
Imports
open import elementary-number-theory.natural-numbers open import foundation.connected-maps open import foundation.postcomposition-functions open import foundation.surjective-maps open import foundation.truncation-levels open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.sets open import foundation-core.truncated-types
Idea
A type X
is said to be set-projective if for every surjective map
f : A → B
into a set B
the postcomposition function
(X → A) → (X → B)
is surjective. This is equivalent to the condition that for every equivalence
relation R
on a type A
the natural map
(X → A)/~ → (X → A/R)
is an equivalence. The latter map is always an embedding, and it is an
equivalence for every X
, A
, and R
if and only if the axiom of choice
holds.
The notion of set-projectiveness generalizes to n
-projectiveness, for n : ℕ
.
A type X
is said to be k
-projective if the postcomposition function
(X → A) → (X → B)
is surjective for every k-1
-connected map f : A → B
into
a k
-truncated type B
.
Definitions
Set-projective types
is-set-projective : {l1 : Level} (l2 l3 : Level) → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) is-set-projective l2 l3 X = (A : UU l2) (B : Set l3) (f : A ↠ type-Set B) → is-surjective (postcomp X (map-surjection f))
k
-projective types
is-projective : {l1 : Level} (l2 l3 : Level) (k : ℕ) → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) is-projective l2 l3 k X = ( A : UU l2) (B : Truncated-Type l3 (truncation-level-ℕ k)) ( f : connected-map ( truncation-level-minus-one-ℕ k) ( A) ( type-Truncated-Type B)) → is-surjective (postcomp X (map-connected-map f))
See also
- The natural map
(X → A)/~ → (X → A/R)
was studied in foundation.exponents-set-quotients
Recent changes
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622). - 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).