open import 1Lab.Classical
open import 1Lab.Prelude

open import Data.Dec
open import Data.Fin

open import Meta.Invariant

module Data.Set.Projective where

Set-projective typesπŸ”—

private variable
  β„“ β„“' β„“'' : Level

A type is set-projective if we can commute propositional truncation past 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 is set-projective if it validates a sort of version of the axiom of choice.

If is a set, then is set-projective if and only if every surjection from a set 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 is a set-projective type, and that is a family of set-projective types, and let be a family of merely inhabited sets. Note that is a family of merely inhabited sets for every so its product must also be inhabited by projectivity of Moreover, is also projective, so is also merely inhabited, as is an 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 with with set-projective, and let be a family of merely inhabited sets. We can precompose with to obtain an family of sets whose product must be inhabited via projectivity of Moreover, we can precompose again with to see that is merely inhabited. Finally, so 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:

  1. Propositions are projective.
  2. Every infinite set admits an injection from Nat. In other words, every infinite set is Dedekind-infinite.
  3. 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 is equivalent to 

  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 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 be a set. The truncation of is a propositon, and the constant family is a set-indexed family, so projectivity of 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 be a proposition, and a family of merely inhabited sets. Note that the type is a set, so it must have split support Moreover, is always merely inhabited, so we can readily show that Finally, is a proposition, so we can obtain a from for any if we combine this with our previous observation, we immediately get 

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.