Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core Truncations.SeparatedTrunc.
Require Import Modalities.Modality Modalities.Identity.
Require Import Limits.Pullback.

(** * Projective types *)

(** To quantify over all truncation levels including infinity, we parametrize [IsOProjective] by a [Modality]. When specializing to [IsOProjective purely] we get an (oo,-1)-projectivity predicate, [IsProjective]. When specializing to [IsOProjective (Tr n)] we get an (n,-1)-projectivity predicate, [IsTrProjective]. *)

Definition IsOProjective (O : Modality) (X : Type) : Type
  := forall A, In O A -> forall B, In O B ->
     forall f : X -> B, forall p : A -> B,
     IsSurjection p -> merely (exists s : X -> A, p o s == f).

(** (oo,-1)-projectivity. *)

Notation IsProjective := (IsOProjective purely).

(** (n,-1)-projectivity. *)

Notation IsTrProjective n := (IsOProjective (Tr n)).

(** A type X is projective if and only if surjections into X merely split. *)
Proposition iff_isoprojective_surjections_split
  (O : Modality) (X : Type) `{In O X}
  : IsOProjective O X <->
    (forall (Y : Type), In O Y -> forall (p : Y -> X),
          IsSurjection p -> merely (exists s : X -> Y, p o s == idmap)).
O: Modality
X: Type
H: In O X
IsOProjective O X <->
(forall Y : Type,
 In O Y ->
 forall p : Y -> X,
 IsConnMap (Tr (-1)) p ->
 merely {s : X -> Y & p o s == idmap})
Proof.
O: Modality
X: Type
H: In O X
IsOProjective O X <->
(forall Y : Type,
 In O Y ->
 forall p : Y -> X,
 IsConnMap (Tr (-1)) p ->
 merely {s : X -> Y & p o s == idmap})
  split.
O: Modality
X: Type
H: In O X
IsOProjective O X ->
forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely {s : X -> Y & (fun x : X => p (s x)) == idmap}
O: Modality
X: Type
H: In O X
(forall Y : Type,
 In O Y ->
 forall p : Y -> X,
 IsConnMap (Tr (-1)) p ->
 merely {s : X -> Y & (fun x : X => p (s x)) == idmap}) ->
IsOProjective O X
  -
O: Modality
X: Type
H: In O X
IsOProjective O X ->
forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely {s : X -> Y & (fun x : X => p (s x)) == idmap} intros isprojX Y oY p S; unfold IsOProjective in isprojX.
O: Modality
X: Type
H: In O X
isprojX: forall A : Type,
In O A ->
forall B : Type,
In O B ->
forall (f : X -> B) (p : A -> B),
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> A & (fun x : X => p (s x)) == f}
Y: Type
oY: In O Y
p: Y -> X
S: IsConnMap (Tr (-1)) p
merely {s : X -> Y & (fun x : X => p (s x)) == idmap}
    exact (isprojX Y _ X _ idmap p S).
  -
O: Modality
X: Type
H: In O X
(forall Y : Type,
 In O Y ->
 forall p : Y -> X,
 IsConnMap (Tr (-1)) p ->
 merely {s : X -> Y & (fun x : X => p (s x)) == idmap}) ->
IsOProjective O X intro splits.
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
IsOProjective O X unfold IsOProjective.
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
forall A : Type,
In O A ->
forall B : Type,
In O B ->
forall (f : X -> B) (p : A -> B),
IsConnMap (Tr (-1)) p ->
merely {s : X -> A & (fun x : X => p (s x)) == f}
    intros A oA B oB f p S.
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
merely {s : X -> A & (fun x : X => p (s x)) == f}
    pose proof (splits (Pullback p f) _ pullback_pr2 _) as s'.
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
s': merely
  {s : X -> Pullback p f &
  (fun x : X => pullback_pr2 (s x)) == idmap}
merely {s : X -> A & (fun x : X => p (s x)) == f}
    strip_truncations.
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
s': {s : X -> Pullback p f &
(fun x : X => pullback_pr2 (s x)) == idmap}
merely {s : X -> A & (fun x : X => p (s x)) == f}
    destruct s' as [s E].
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
s: X -> Pullback p f
E: (fun x : X => pullback_pr2 (s x)) == idmap
merely {s : X -> A & (fun x : X => p (s x)) == f}
    refine (tr (pullback_pr1 o s; _)).
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
s: X -> Pullback p f
E: (fun x : X => pullback_pr2 (s x)) == idmap
(fun x : X => p (pullback_pr1 (s x))) == f
    intro x.
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
s: X -> Pullback p f
E: (fun x : X => pullback_pr2 (s x)) == idmap
x: X
p (pullback_pr1 (s x)) = f x
    refine (pullback_commsq p f (s x) @ _).
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
s: X -> Pullback p f
E: (fun x : X => pullback_pr2 (s x)) == idmap
x: X
f (pullback_pr2 (s x)) = f x
    apply (ap f).
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
A: Type
oA: In O A
B: Type
oB: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
s: X -> Pullback p f
E: (fun x : X => pullback_pr2 (s x)) == idmap
x: X
pullback_pr2 (s x) = x
    apply E.
Defined.

Corollary equiv_isoprojective_surjections_split
  `{Funext} (O : Modality) (X : Type) `{In O X}
  : IsOProjective O X <~>
    (forall (Y : Type), In O Y -> forall (p : Y -> X),
          IsSurjection p -> merely (exists s : X -> Y, p o s == idmap)).
H: Funext
O: Modality
X: Type
H0: In O X
IsOProjective O X <~>
(forall Y : Type,
 In O Y ->
 forall p : Y -> X,
 IsConnMap (Tr (-1)) p ->
 merely {s : X -> Y & p o s == idmap})
Proof.
H: Funext
O: Modality
X: Type
H0: In O X
IsOProjective O X <~>
(forall Y : Type,
 In O Y ->
 forall p : Y -> X,
 IsConnMap (Tr (-1)) p ->
 merely {s : X -> Y & p o s == idmap})
  exact (equiv_iff_hprop_uncurried (iff_isoprojective_surjections_split O 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. We will refer to this as [HasOChoice], to avoid confusion with [IsOProjective] above. In similarity with [IsOProjective], we parametrize it by a [Modality]. *)

Class HasOChoice (O : Modality) (A : Type) :=
  hasochoice :
    forall (B : A -> Type), (forall x, In O (B x)) ->
    (forall x, merely (B x)) -> merely (forall x, B x).

(** (oo,-1)-choice. *)

Notation HasChoice := (HasOChoice purely).

(** (n,-1)-choice. *)

Notation HasTrChoice n := (HasOChoice (Tr n)).

Instance hasochoice_sigma
  `{Funext} {A : Type} {B : A -> Type} (O : Modality)
  (chA : HasOChoice O A)
  (chB : forall a : A, HasOChoice O (B a))
  : HasOChoice O {a : A | B a}.
H: Funext
A: Type
B: A -> Type
O: Modality
chA: HasOChoice O A
chB: forall a : A, HasOChoice O (B a)
HasOChoice O {a : A & B a}
Proof.
H: Funext
A: Type
B: A -> Type
O: Modality
chA: HasOChoice O A
chB: forall a : A, HasOChoice O (B a)
HasOChoice O {a : A & B a}
  intros C sC f.
H: Funext
A: Type
B: A -> Type
O: Modality
chA: HasOChoice O A
chB: forall a : A, HasOChoice O (B a)
C: {a : A & B a} -> Type
sC: forall x : {a : A & B a}, In O (C x)
f: forall x : {a : A & B a}, merely (C x)
merely (forall x : {a : A & B a}, C x)
  set (f' := fun a => chB a (fun b => C (a; b)) _ (fun b => f (a; b))).
H: Funext
A: Type
B: A -> Type
O: Modality
chA: HasOChoice O A
chB: forall a : A, HasOChoice O (B a)
C: {a : A & B a} -> Type
sC: forall x : {a : A & B a}, In O (C x)
f: forall x : {a : A & B a}, merely (C x)
f':= fun a : A =>
chB a (fun b : B a => C (a; b))
  (fun x : B a => sC (a; x))
  (fun b : B a => f (a; b)): forall a : A,
merely
  (forall x : B a, (fun b : B a => C (a; b)) x)
merely (forall x : {a : A & B a}, C x)
  specialize (chA (fun a => forall b, C (a; b)) _ f').
H: Funext
A: Type
B: A -> Type
O: Modality
C: {a : A & B a} -> Type
chA: merely
(forall x : A, (fun a : A => forall b : (fun a0 : A => B a0) a, C (a; b)) x)
chB: forall a : A, HasOChoice O (B a)
sC: forall x : {a : A & B a}, In O (C x)
f: forall x : {a : A & B a}, merely (C x)
f':= fun a : A =>
chB a (fun b : B a => C (a; b))
  (fun x : B a => sC (a; x))
  (fun b : B a => f (a; b)): forall a : A,
merely
  (forall x : B a, (fun b : B a => C (a; b)) x)
merely (forall x : {a : A & B a}, C x)
  strip_truncations.
H: Funext
A: Type
B: A -> Type
O: Modality
C: {a : A & B a} -> Type
chB: forall a : A, HasOChoice O (B a)
sC: forall x : {a : A & B a}, In O (C x)
f: forall x : {a : A & B a}, merely (C x)
f':= fun a : A =>
chB a (fun b : B a => C (a; b))
  (fun x : B a => sC (a; x))
  (fun b : B a => f (a; b)): forall a : A,
merely
  (forall x : B a, (fun b : B a => C (a; b)) x)
chA: forall (x : A) (b : B x), C (x; b)
merely (forall x : {a : A & B a}, C x)
  apply tr.
H: Funext
A: Type
B: A -> Type
O: Modality
C: {a : A & B a} -> Type
chB: forall a : A, HasOChoice O (B a)
sC: forall x : {a : A & B a}, In O (C x)
f: forall x : {a : A & B a}, merely (C x)
f':= fun a : A =>
chB a (fun b : B a => C (a; b))
  (fun x : B a => sC (a; x))
  (fun b : B a => f (a; b)): forall a : A,
merely
  (forall x : B a, (fun b : B a => C (a; b)) x)
chA: forall (x : A) (b : B x), C (x; b)
forall x : {a : A & B a}, C x
  intro.
H: Funext
A: Type
B: A -> Type
O: Modality
C: {a : A & B a} -> Type
chB: forall a : A, HasOChoice O (B a)
sC: forall x : {a : A & B a}, In O (C x)
f: forall x : {a : A & B a}, merely (C x)
f':= fun a : A =>
chB a (fun b : B a => C (a; b))
  (fun x : B a => sC (a; x))
  (fun b : B a => f (a; b)): forall a : A,
merely
  (forall x : B a, (fun b : B a => C (a; b)) x)
chA: forall (x : A) (b : B x), C (x; b)
x: {a : A & B a}
C x
  apply chA.
Defined.

Proposition isoprojective_ochoice (O : Modality) (X : Type)
  : HasOChoice O X -> IsOProjective O X.
O: Modality
X: Type
HasOChoice O X -> IsOProjective O X
Proof.
O: Modality
X: Type
HasOChoice O X -> IsOProjective O X
  intros chX A ? B ? f p S.
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
merely {s : X -> A & (fun x : X => p (s x)) == f}
  assert (g : merely (forall x:X, hfiber p (f x))).
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
merely (forall x : X, hfiber p (f x))
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
g: merely (forall x : X, hfiber p (f x))
merely {s : X -> A & (fun x : X => p (s x)) == f}
  -
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
merely (forall x : X, hfiber p (f x)) rapply chX.
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
forall x : X, merely (hfiber p (f x))
    intro x.
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
x: X
merely (hfiber p (f x))
    exact (center _).
  -
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
g: merely (forall x : X, hfiber p (f x))
merely {s : X -> A & (fun x : X => p (s x)) == f} strip_truncations; apply tr.
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
g: forall x : X, hfiber p (f x)
{s : X -> A & (fun x : X => p (s x)) == f}
    exists (fun x:X => pr1 (g x)).
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
g: forall x : X, hfiber p (f x)
(fun x : X => p (g x).1) == f
    intro x.
O: Modality
X: Type
chX: HasOChoice O X
A: Type
X0: In O A
B: Type
X1: In O B
f: X -> B
p: A -> B
S: IsConnMap (Tr (-1)) p
g: forall x : X, hfiber p (f x)
x: X
p (g x).1 = f x
    exact (g x).2.
Defined.

Proposition hasochoice_oprojective (O : Modality) (X : Type) `{In O X}
  : IsOProjective O X -> HasOChoice O X.
O: Modality
X: Type
H: In O X
IsOProjective O X -> HasOChoice O X
Proof.
O: Modality
X: Type
H: In O X
IsOProjective O X -> HasOChoice O X
  refine (_ o fst (iff_isoprojective_surjections_split O X)).
O: Modality
X: Type
H: In O X
(forall Y : Type,
 In O Y ->
 forall p : Y -> X,
 IsConnMap (Tr (-1)) p ->
 merely {s : X -> Y & (fun x : X => p (s x)) == idmap}) ->
HasOChoice O X
  intros splits P oP S.
O: Modality
X: Type
H: In O X
splits: forall Y : Type,
In O Y ->
forall p : Y -> X,
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> Y &
  (fun x : X => p (s x)) == idmap}
P: X -> Type
oP: forall x : X, In O (P x)
S: forall x : X, merely (P x)
merely (forall x : X, P x)
  specialize splits with {x : X & P x} pr1.
O: Modality
X: Type
H: In O X
P: X -> Type
splits: In O {x : X & P x} ->
IsConnMap (Tr (-1)) pr1 ->
merely
  {s : X -> {x : X & P x} &
  (fun x : X => (s x).1) == idmap}
oP: forall x : X, In O (P x)
S: forall x : X, merely (P x)
merely (forall x : X, P x)
  pose proof (splits _ (fst (iff_merely_issurjection P) S)) as M.
O: Modality
X: Type
H: In O X
P: X -> Type
splits: In O {x : X & P x} ->
IsConnMap (Tr (-1)) pr1 ->
merely
  {s : X -> {x : X & P x} &
  (fun x : X => (s x).1) == idmap}
oP: forall x : X, In O (P x)
S: forall x : X, merely (P x)
M: merely
  {s : X -> {x : X & P x} &
  (fun x : X => (s x).1) == idmap}
merely (forall x : X, P x)
  clear S splits.
O: Modality
X: Type
H: In O X
P: X -> Type
oP: forall x : X, In O (P x)
M: merely
  {s : X -> {x : X & P x} &
  (fun x : X => (s x).1) == idmap}
merely (forall x : X, P x)
  strip_truncations; apply tr.
O: Modality
X: Type
H: In O X
P: X -> Type
oP: forall x : X, In O (P x)
M: {s : X -> {x : X & P x} &
(fun x : X => (s x).1) == idmap}
forall x : X, P x
  destruct M as [s p].
O: Modality
X: Type
H: In O X
P: X -> Type
oP: forall x : X, In O (P x)
s: X -> {x : X & P x}
p: (fun x : X => (s x).1) == idmap
forall x : X, P x
  intro x.
O: Modality
X: Type
H: In O X
P: X -> Type
oP: forall x : X, In O (P x)
s: X -> {x : X & P x}
p: (fun x : X => (s x).1) == idmap
x: X
P x
  exact (transport _ (p x) (s x).2).
Defined.

Proposition iff_isoprojective_hasochoice (O : Modality) (X : Type) `{In O X}
  : IsOProjective O X <-> HasOChoice O X.
O: Modality
X: Type
H: In O X
IsOProjective O X <-> HasOChoice O X
Proof.
O: Modality
X: Type
H: In O X
IsOProjective O X <-> HasOChoice O X
  split.
O: Modality
X: Type
H: In O X
IsOProjective O X -> HasOChoice O X
O: Modality
X: Type
H: In O X
HasOChoice O X -> IsOProjective O X
  -
O: Modality
X: Type
H: In O X
IsOProjective O X -> HasOChoice O X apply hasochoice_oprojective.
O: Modality
X: Type
H: In O X
In O X exact _.
  -
O: Modality
X: Type
H: In O X
HasOChoice O X -> IsOProjective O X apply isoprojective_ochoice.
Defined.

Proposition equiv_isoprojective_hasochoice
  `{Funext} (O : Modality) (X : Type) `{In O X}
  : IsOProjective O X <~> HasOChoice O X.
H: Funext
O: Modality
X: Type
H0: In O X
IsOProjective O X <~> HasOChoice O X
Proof.
H: Funext
O: Modality
X: Type
H0: In O X
IsOProjective O X <~> HasOChoice O X
  refine (equiv_iff_hprop_uncurried (iff_isoprojective_hasochoice O X)).
H: Funext
O: Modality
X: Type
H0: In O X
IsHProp (HasOChoice O X)
  exact istrunc_forall.
Defined.

Proposition isprojective_unit : IsProjective Unit.
IsProjective Unit
Proof.
IsProjective Unit
  apply (isoprojective_ochoice purely Unit).
HasChoice Unit
  intros P trP S.
P: Unit -> Type
trP: forall x : Unit, In purely (P x)
S: forall x : Unit, merely (P x)
merely (forall x : Unit, P x)
  specialize S with tt.
P: Unit -> Type
trP: forall x : Unit, In purely (P x)
S: merely (P tt)
merely (forall x : Unit, P x)
  strip_truncations; apply tr.
P: Unit -> Type
trP: forall x : Unit, In purely (P x)
S: P tt
forall x : Unit, P x
  apply Unit_ind.
P: Unit -> Type
trP: forall x : Unit, In purely (P x)
S: P tt
P tt
  exact S.
Defined.

Section AC_oo_neg1.
  (** ** Projectivity and AC_(oo,-1) (defined in HoTT book, Exercise 7.8) *)
  (* TODO: Generalize to n, m. *)

  Context {AC : forall X : HSet, HasChoice X}.

  (** (Exercise 7.9) Assuming AC_(oo,-1) every type merely has a projective cover. *)
  Proposition projective_cover_AC `{Univalence} (A : Type)
    : merely (exists X:HSet, exists p : X -> A, IsSurjection p).
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
merely
  {X : HSet & {p : X -> A & IsConnMap (Tr (-1)) p}}
  Proof.
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
merely
  {X : HSet & {p : X -> A & IsConnMap (Tr (-1)) p}}
    pose (X := Build_HSet (Tr 0 A)).
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
merely
  {X : HSet & {p : X -> A & IsConnMap (Tr (-1)) p}}
    pose proof ((equiv_isoprojective_hasochoice _ X)^-1 (AC X)) as P.
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
P: IsProjective X
merely
  {X : HSet & {p : X -> A & IsConnMap (Tr (-1)) p}}
    pose proof (P A _ X _ idmap tr _) as F; clear P.
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
F: merely {s : X -> A & tr o s == idmap}
merely
  {X : HSet & {p : X -> A & IsConnMap (Tr (-1)) p}}
    strip_truncations.
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
F: {s : X -> A & (fun x : X => tr (s x)) == idmap}
merely
  {X : HSet & {p : X -> A & IsConnMap (Tr (-1)) p}}
    destruct F as [f p].
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
f: X -> A
p: (fun x : X => tr (f x)) == idmap
merely
  {X : HSet & {p : X -> A & IsConnMap (Tr (-1)) p}}
    refine (tr (X; (f; BuildIsSurjection f _))).
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
f: X -> A
p: (fun x : X => tr (f x)) == idmap
forall b : A, merely (hfiber f b)
    intro a; unfold hfiber.
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
f: X -> A
p: (fun x : X => tr (f x)) == idmap
a: A
merely {x : X & f x = a}
    apply equiv_O_sigma_O.
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
f: X -> A
p: (fun x : X => tr (f x)) == idmap
a: A
Tr (-1) {x : X & Tr (-1) (f x = a)}
    refine (tr (tr a; _)).
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
f: X -> A
p: (fun x : X => tr (f x)) == idmap
a: A
Tr (-1) (f (tr a) = a)
    rapply (equiv_path_Tr _ _)^-1%equiv.  (* Uses Univalence. *)
AC: forall X : HSet, HasChoice X
H: Univalence
A: Type
X:= Build_HSet (Tr 0 A): HSet
f: X -> A
p: (fun x : X => tr (f x)) == idmap
a: A
tr (f (tr a)) = tr a
    apply p.
  Defined.

  (** Assuming AC_(oo,-1), projective types are exactly sets. *)
  Theorem equiv_isprojective_ishset_AC `{Univalence} (X : Type)
    : IsProjective X <~> IsHSet X.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
IsProjective X <~> IsHSet X
  Proof.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
IsProjective X <~> IsHSet X
    apply equiv_iff_hprop.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
IsProjective X -> IsHSet X
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
IsHSet X -> IsProjective X
    -
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
IsProjective X -> IsHSet X intro isprojX.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
isprojX: IsProjective X
IsHSet X unfold IsOProjective in isprojX.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
isprojX: forall A : Type,
In purely A ->
forall B : Type,
In purely B ->
forall (f : X -> B) (p : A -> B),
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> A & (fun x : X => p (s x)) == f}
IsHSet X
      pose proof (projective_cover_AC X) as P; strip_truncations.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
isprojX: forall A : Type,
In purely A ->
forall B : Type,
In purely B ->
forall (f : X -> B) (p : A -> B),
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> A & (fun x : X => p (s x)) == f}
P: {X0 : HSet &
{p : X0 -> X & IsConnMap (Tr (-1)) p}}
IsHSet X
      destruct P as [P [p issurj_p]].
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
isprojX: forall A : Type,
In purely A ->
forall B : Type,
In purely B ->
forall (f : X -> B) (p : A -> B),
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> A & (fun x : X => p (s x)) == f}
P: HSet
p: P -> X
issurj_p: IsConnMap (Tr (-1)) p
IsHSet X
      pose proof (isprojX P _ X _ idmap p issurj_p) as S; strip_truncations.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
isprojX: forall A : Type,
In purely A ->
forall B : Type,
In purely B ->
forall (f : X -> B) (p : A -> B),
IsConnMap (Tr (-1)) p ->
merely
  {s : X -> A & (fun x : X => p (s x)) == f}
P: HSet
p: P -> X
issurj_p: IsConnMap (Tr (-1)) p
S: {s : X -> P & (fun x : X => p (s x)) == idmap}
IsHSet X
      exact (inO_retract_inO (Tr 0) X P S.1 p S.2).
    -
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
IsHSet X -> IsProjective X intro ishsetX.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
ishsetX: IsHSet X
IsProjective X
      apply (equiv_isoprojective_hasochoice purely X)^-1.
AC: forall X : HSet, HasChoice X
H: Univalence
X: Type
ishsetX: IsHSet X
HasChoice X
      rapply AC.
  Defined.

End AC_oo_neg1.