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β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βType$ is a family of set-projective types, and let $P:Ξ£ΒAΒBβSet$ be a family of merely inhabited sets. Note that $(b:B(a))β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)β(b:B(a))βP(a,b)$ is also merely inhabited, as $(b:B(a))β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βB,g:BβA$ with $fβg=id$ with $A$ set-projective, and let $P:Bβ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)βP(f(a))$ must be inhabited via projectivity of $A.$ Moreover, we can precompose again with $g$ to see that $Ξ(b:B)βP(f(g(b)))$ is merely inhabited. Finally, $f(g(b))=b,$ so $Ξ(b:B)β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 $Natβͺ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β₯β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βSet$ a family of merely inhabited sets. Note that the type $Ξ£AP$ is a set, so it must have split support $s:β₯β₯Ξ£APβ₯βΞ£APβ₯.$ Moreover, $P(a)$ is always merely inhabited, so we can readily show that $β₯AβΞ£APβ₯.$ Finally, $A$ is a proposition, so we can obtain a $P(a)$ from $Ξ£AP$ for any $a:A;$ if we combine this with our previous observation, we immediately get $β₯(a:A)β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.*