module Data.Set.Projective where

Set-projective types🔗

A type $A$ is set-projective if we can commute propositional truncation past $A -indexed$ families.

is-set-projective : ∀ {ℓ} (A : Type ℓ) → (κ : Level) → Type _
is-set-projective A κ =
  ∀ (P : A → Type κ)
  → (∀ a → is-set (P a))
  → (∀ a → ∥ P a ∥)
  → ∥ (∀ a → P a) ∥

Intuitively, a type $A$ is set-projective if it validates a sort of $A -indexed$ version of the axiom of choice.

If $A$ is a set, then $A$ is set-projective if and only if every surjection $E \to A$ from a set $E$ splits.

surjections-split→set-projective
  : ∀ {ℓ ℓ'} {A : Type ℓ}
  → is-set A
  → (∀ (E : Type (ℓ ⊔ ℓ')) → is-set E
     → (f : E → A) → is-surjective f
     → ∥ (∀ a → fibre f a) ∥)
  → is-set-projective A (ℓ ⊔ ℓ')

sets-projective→surjections-split
  : ∀ {ℓ ℓ'} {A : Type ℓ}
  → is-set A
  → is-set-projective A (ℓ ⊔ ℓ')
  → ∀ {E : Type ℓ'} → is-set E
  → (f : E → A) → is-surjective f
  → ∥ (∀ a → fibre f a) ∥

This is essentially a specialization of the of the proof that the axiom of choice is equivalent to every surjection splitting, so we will not dwell on the details.

surjections-split→set-projective {A = A} A-set surj-split P P-set ∥P∥ =
  ∥-∥-map
    (Equiv.to (Π-cod≃ (Fibre-equiv P)))
    (surj-split (Σ[ x ∈ A ] (P x)) (Σ-is-hlevel 2 A-set P-set) fst λ x →
      ∥-∥-map (Equiv.from (Fibre-equiv P x)) (∥P∥ x))

sets-projective→surjections-split A-set A-pro E-set f =
  A-pro (fibre f) (λ x → fibre-is-hlevel 2 E-set A-set f x)

Closure of set-projectivity🔗

Set-projective types are closed under Σ-types. Suppose that $A : Type$ is a set-projective type, and that $B : A \to Type$ is a family of set-projective types, and let $P : Σ A B \to Set$ be a family of merely inhabited sets. Note that $(b : B (a)) \to P (a, b)$ is a $B (a) -indexed$ family of merely inhabited sets for every $a,$ so its product must also be inhabited by projectivity of $B (a) .$ Moreover, $A$ is also projective, so $(a : A) \to (b : B (a)) \to P (a, b)$ is also merely inhabited, as $(b : B (a)) \to P (a, b)$ is an $A -indexed$ family of merely inhabited sets. We can then uncurry this family to finish the proof.

Σ-set-projective
  : ∀ {A : Type ℓ} {B : A → Type ℓ'}
  → is-set-projective A (ℓ' ⊔ ℓ'')
  → (∀ a → is-set-projective (B a) ℓ'')
  → is-set-projective (Σ[ a ∈ A ] B a) ℓ''
Σ-set-projective {A = A} {B = B} A-pro B-pro P P-set ∥P∥ = do
  ∥-∥-map uncurry $
    A-pro (λ a → ((b : B a) → P (a , b))) (λ a → Π-is-hlevel 2 λ b → P-set (a , b)) λ a →
    B-pro a (λ b → P (a , b)) (λ b → P-set (a , b)) λ b → ∥P∥ (a , b)

Moreover, set-projective types are stable under retracts. Suppose that we have $f : A \to B, g : B \to A$ with $f \circ g = i d$ with $A$ set-projective, and let $P : B \to Set$ be a family of merely inhabited sets. We can precompose $P$ with $f$ to obtain an $A -indexed$ family of sets whose product $Π (a : A) \to P (f (a))$ must be inhabited via projectivity of $A .$ Moreover, we can precompose again with $g$ to see that $Π (b : B) \to P (f (g (b)))$ is merely inhabited. Finally, $f (g (b)) = b,$ so $Π (b : B) \to P (b)$ is merely inhabited.

retract→set-projective
  : ∀ {A : Type ℓ} {B : Type ℓ'}
  → (f : A → B) (g : B → A)
  → is-left-inverse f g
  → is-set-projective A ℓ''
  → is-set-projective B ℓ''
retract→set-projective {A = A} {B = B} f g retract A-pro P P-set ∥P∥ =
  ∥-∥-map (λ k b → subst P (retract b) (k (g b)))
    (A-pro (P ∘ f) (P-set ∘ f) (∥P∥ ∘ f))

This gives us a nice proof that set-projectivity is stable under equivalence.

Equiv→set-projective
  : ∀ {A : Type ℓ} {B : Type ℓ'}
  → A ≃ B
  → is-set-projective A ℓ''
  → is-set-projective B ℓ''
Equiv→set-projective f A-pro =
  retract→set-projective (Equiv.to f) (Equiv.from f) (Equiv.ε f) A-pro

By the theorem of finite choice, finite sets are projective.

Fin-set-projective : ∀ {n} → is-set-projective (Fin n) ℓ
Fin-set-projective {n = n} P P-set ∥P∥ = finite-choice n ∥P∥

finite→set-projective
  : {A : Type ℓ}
  → Finite A
  → is-set-projective A ℓ'
finite→set-projective finite =
  rec! (λ enum → Equiv→set-projective (enum e⁻¹) Fin-set-projective)
    (Finite.enumeration finite)

Taboos🔗

As it turns out, the finite types are the only types that are projective constructively! The general sketch of the taboo is that it is consistent that:

Propositions are projective.
Every infinite set admits an injection from Nat. In other words, every infinite set is Dedekind-infinite.
Countable choice fails (IE: the natural numbers are not set-projective).

The existence of such a model is out of scope for this page, so we will focus our attention on the internal portion of the argument. In particular, we will prove that if propositions are set-projective, then the existence of an Dedekind-infinite set-projective type implies countable choice.

First, note that if propositions are set-projective, then the image of every function into a set-projective type is itself set-projective. This follows directly from the definition of images, along with closure of projectives under Σ.

module _
  (props-projective : ∀ {ℓ ℓ'} → (A : Type ℓ) → is-prop A → is-set-projective A ℓ')
  where

  props-projective→image-projective
    : ∀ {A : Type ℓ} {B : Type ℓ'}
    → (f : A → B)
    → is-set-projective B (ℓ ⊔ ℓ' ⊔ ℓ'')
    → is-set-projective (image f) ℓ''
  props-projective→image-projective f B-pro =
    Σ-set-projective B-pro λ b → props-projective _ (hlevel 1)

This in turn implies that set-projective types are stable under embeddings, as the image of an embedding $f : A ↪ B$ is equivalent to $A .$

  props-projective+is-embedding→set-projective
    : ∀ {A : Type ℓ} {B : Type ℓ'} {f : A → B}
    → is-embedding f
    → is-set-projective B (ℓ ⊔ ℓ' ⊔ ℓ'')
    → is-set-projective A ℓ''
  props-projective+is-embedding→set-projective {f = f} f-emb B-pro =
    Equiv→set-projective
      (is-embedding→image-equiv f-emb e⁻¹)
      (props-projective→image-projective f B-pro)

If we specialise this result to embeddings $N a t ↪ A,$ then we obtain countable choice from the existence of a Dedekind-infinite type.

  props-projective+dedekind-infinite-projective→countable-choice
    : ∀ {A : Type ℓ} {f : Nat → A}
    → is-embedding f
    → is-set-projective A (ℓ ⊔ ℓ')
    → is-set-projective Nat ℓ'
  props-projective+dedekind-infinite-projective→countable-choice =
    props-projective+is-embedding→set-projective

Note that the set-projectivity of propositions is itself a taboo: in particular, every proposition is set-projective if and only if every set has split support. The following proof is adapted from (Kraus et al. 2016).

We will start with the reverse direction. Suppose that every proposition is set projective, and let $A$ be a set. The truncation of $A$ is a propositon, and the constant family $∥ A ∥ \to A$ is a set-indexed family, so projectivity of $∥ A ∥$ directly gives us split support.

props-projective→split-support
  : ∀ {ℓ}
  → ((A : Type ℓ) → is-prop A → is-set-projective A ℓ)
  → ∀ (A : Type ℓ) → is-set A → ∥ (∥ A ∥ → A) ∥
props-projective→split-support props-projective A A-set =
  props-projective ∥ A ∥ (hlevel 1) (λ _ → A) (λ _ → A-set) id

For the forward direction, suppose that every set has split support, let $A$ be a proposition, and $P : A \to Set$ a family of merely inhabited sets. Note that the type $Σ A P$ is a set, so it must have split support $s : ∥∥Σ A P ∥ \to Σ A P ∥ .$ Moreover, $P (a)$ is always merely inhabited, so we can readily show that $∥ A \to Σ A P ∥ .$ Finally, $A$ is a proposition, so we can obtain a $P (a)$ from $Σ A P$ for any $a : A;$ if we combine this with our previous observation, we immediately get $∥ (a : A) \to P (a) ∥ .$

split-support→props-projective
  : ∀ {ℓ}
  → (∀ (A : Type ℓ) → is-set A → ∥ (∥ A ∥ → A) ∥)
  → (A : Type ℓ) → is-prop A → is-set-projective A ℓ
split-support→props-projective split-support A A-prop P P-set ∥P∥ = do
  s ← split-support (Σ[ a ∈ A ] P a) (Σ-is-hlevel 2 (is-prop→is-set A-prop) P-set)
  pure λ a → subst P (A-prop _ _) (snd (s (∥-∥-map (λ p → (a , p)) (∥P∥ a))))

References

Kraus, Nicolai, M. Escardó, T. Coquand, and Thorsten Altenkirch. 2016. “Notions of Anonymous Existence in Martin-Löf Type Theory.” Log. Methods Comput. Sci.