Projective types

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

Created on 2023-02-06.
Last modified on 2025-08-14.

module foundation.projective-types where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.connected-maps
open import foundation.inhabited-types
open import foundation.postcomposition-functions
open import foundation.surjective-maps
open import foundation.truncation-levels
open import foundation.universe-levels

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 onto a set B the [postcomposition function[(foundation-core.postcomposition-functions.md)

  (X → A) → (X → B)

is surjective. This is equivalent to the condition that for every [equivalence relation[(foundation-core.equivalence-relations.md) 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 every natural number 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-Level :
  {l1 : Level} (l2 l3 : Level) → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
is-set-projective-Level l2 l3 X =
  (A : UU l2) (B : Set l3) (f : A ↠ type-Set B) →
  is-surjective (postcomp X (map-surjection f))

is-set-projective : {l1 : Level} → UU l1 → UUω
is-set-projective X = {l2 l3 : Level} → is-set-projective-Level l2 l3 X

k-projective types

is-trunc-projective-Level :
  {l1 : Level} (l2 l3 : Level) → ℕ → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
is-trunc-projective-Level 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))

is-trunc-projective : {l1 : Level} → ℕ → UU l1 → UUω
is-trunc-projective k X = {l2 l3 : Level} → is-trunc-projective-Level l2 l3 k X

Alternative statement of set-projectivity

is-projective-Level' : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
is-projective-Level' l2 X =
  (P : X → UU l2) →
  ((x : X) → is-inhabited (P x)) →
  is-inhabited ((x : X) → (P x))

is-projective' : {l1 : Level} → UU l1 → UUω
is-projective' X = {l2 : Level} → is-projective-Level' l2 X

See also

Recent changes