Library HoTT.Projective

Require Import Basics Types HProp HFiber HSet.
Require Import Truncations.
Require Import Modalities.Descent Modalities.Separated.
Require Import Limits.Pullback.

Projective types


Definition IsProjective (X : Type) : Type
  := A B : Type, f : X B, p : A B,
        IsSurjection p merely ( s : X A, p o s == f).

A type X is projective if and only if surjections into X merely split.
Proposition iff_isprojective_surjections_split (X : Type)
  : IsProjective X
    ( (Y : Type), (p : Y X),
          IsSurjection p merely ( s : X Y, p o s == idmap)).
Proof.
  split.
  - intros isprojX Y p S; unfold IsProjective in isprojX.
    exact (isprojX Y X idmap p S).
  - intro splits. unfold IsProjective.
    intros A B f p S.
    pose proof (splits (Pullback p f) pullback_pr2 _) as s'.
    strip_truncations.
    destruct s' as [s E].
    refine (tr (pullback_pr1 o s; _)).
    intro x.
    refine (pullback_commsq p f (s x) @ _).
    apply (ap f).
    apply E.
Defined.

Corollary equiv_isprojective_surjections_split `{Funext} (X : Type)
  : IsProjective X <~>
    ( (Y : Type), (p : Y X),
          IsSurjection p merely ( s : X Y, p o s == idmap)).
Proof.
  exact (equiv_iff_hprop_uncurried (iff_isprojective_surjections_split X)).
Defined.

Projectivity and the axiom of choice

In topos theory, an object X is said to be projective if the axiom of choice holds when making choices indexed by X.
Definition IsProjective' (X : Type) : Type := P : X Type,
    ( x, merely (P x)) merely ( x, P x).

Proposition iff_isprojective_choice (X : Type)
  : IsProjective X IsProjective' X.
Proof.
  refine (iff_compose (iff_isprojective_surjections_split X) _).
  split.
  - intros splits P S.
    specialize splits with {x : X & P x} pr1.
    pose proof (splits (fst (iff_merely_issurjection P) S)) as M.
    clear S splits.
    strip_truncations; apply tr.
    destruct M as [s p].
    intro x.
    exact (transport _ (p x) (s x).2).
  - intros choiceX Y p S.
    unfold IsConnMap, IsConnected in S.
    pose proof (fun b ⇒ (@center _ (S b))) as S'; clear S.
    pose proof (choiceX (hfiber p) S') as M; clear S'.
    strip_truncations; apply tr.
     (fun x(M x).1).
    exact (fun x(M x).2).
Defined.

Proposition equiv_isprojective_choice `{Funext} (X : Type)
  : IsProjective X <~> IsProjective' X.
Proof.
  exact (equiv_iff_hprop_uncurried (iff_isprojective_choice X)).
Defined.

Proposition isprojective_unit : IsProjective Unit.
Proof.
  apply (iff_isprojective_choice Unit).
  intros P S.
  specialize S with tt.
  strip_truncations; apply tr.
  apply Unit_ind.
  exact S.
Defined.

Section AC_oo_neg1.

Projectivity and AC(oo,-1) (defined in HoTT book, Exercise 7.8)


  Context {AC : X : hSet, IsProjective' X}.

(Exercise 7.9) Assuming AC(oo,-1) every type merely has a projective cover.
  Proposition projective_cover_AC `{Univalence} (A : Type)
    : merely ( X:hSet, p : X A, IsSurjection p).
  Proof.
    pose (X := BuildhSet (Tr 0 A)).
    pose proof ((equiv_isprojective_choice X)^-1 (AC X)) as P.
    pose proof (P A X idmap tr _) as F; clear P.
    strip_truncations.
    destruct F as [f p].
    refine (tr (X; (f; BuildIsSurjection f _))).
    intro a; unfold hfiber.
    apply equiv_O_sigma_O.
    refine (tr (tr a; _)).
    rapply (equiv_path_Tr _ _)^-1%equiv.     apply p.
  Defined.

Assuming AC(oo,-1), projective types are exactly sets.
  Theorem equiv_isprojective_ishset_AC `{Univalence} (X : Type)
    : IsProjective X <~> IsHSet X.
  Proof.
    apply equiv_iff_hprop.
    - intro isprojX. unfold IsProjective in isprojX.
      pose proof (projective_cover_AC X) as P; strip_truncations.
      destruct P as [P [p issurj_p]].
      pose proof (isprojX P X idmap p issurj_p) as S; strip_truncations.
      destruct S as [s h].
      rapply (istrunc_embedding_trunc s).
      apply isembedding_isinj_hset.
      exact (isinj_section h).
    - intro ishsetX.
      apply (equiv_isprojective_choice X)^-1.
      rapply AC.
  Defined.

End AC_oo_neg1.