# Projective types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2023-02-06.

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))