(** * Injective Types *)

(** Formalization of the paper: Injective Types in Univalent Mathematics by Martín Escardó (with some extra results). *)

From HoTT Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core Truncations.Constant.
Require Import Modalities.Modality.
Require Import HFiber.
Require Import Universes.HProp.
Require Import ExcludedMiddle.
Require Import InjectiveTypes.TypeFamKanExt.

(** ** Definitions of injectivity and first examples *)

(** Since the universe levels are important to many of the results here, we keep track of them explicitly as much as possible. Due to our inability to use the max and successor operations within proofs, we instead construct these universes and their associated posetal relations in the arguments of the functions.

In universe declarations, we use [u], [v], [w], etc. as our typical universe variables. Our convention for the max of two universes [u] and [v] is [uv], and the successor of a universe [u] is [su]. Occasionally we write [T] for a top universe which is strictly larger than all other provided universes.

We hope that later versions of Coq will allow us access to the max and successor operations and much of the cumbersome universe handling here can be greatly reduced. *)

Section UniverseStructure.
  Universes u v w uv uw vw.
  Constraint u <= uv, v <= uv, u <= uw, w <= uw, v <= vw, w <= vw.

  (** A type [D] is said to be injective if for every embedding [j : X -> Y] and every function [f : X -> D], there merely exists a [f' : Y -> D] such that [f' o j == f]. *)
  Definition IsInjectiveType@{uvw | uv <= uvw, uw <= uvw, vw <= uvw} (D : Type@{w})
    := forall (X : Type@{u}) (Y : Type@{v}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j)
      (f : X -> D), merely@{uvw} (sig@{vw uw} (fun f' => f' o j == f)).

  (** A type is then algebraically injective if the same is true, but without the propositional truncation. We use a class here instead of just a sigma type to make proofs more readable. *)
  Class IsAlgebraicInjectiveType@{} (D : Type@{w}) := {
    lift_ai {X : Type@{u}} {Y : Type@{v}} (j : X -> Y) {isem : IsEmbedding@{u v uv} j} (f : X -> D)
      : Y -> D;
    is_ext_ai {X : Type@{u}} {Y : Type@{v}} (j : X -> Y) {isem} f
      : lift_ai j f o j == f;
  }.

  (** Contractible types are algebraically injective. *)
  #[export] Instance alg_inj_contr@{} (D : Type@{w}) (cD : Contr D)
    : IsAlgebraicInjectiveType@{} D.
D: Type
cD: Contr D
IsAlgebraicInjectiveType D
  Proof.
D: Type
cD: Contr D
IsAlgebraicInjectiveType D
    snapply Build_IsAlgebraicInjectiveType; intros X Y j isem f.
D: Type
cD: Contr D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D
Y -> D
D: Type
cD: Contr D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D
(fun (X Y : Type) (j : X -> Y) 
   (isem : IsEmbedding j) 
   (f : X -> D) => ?Goal) X Y j
  (istruncmap_mapinO_tr j) f o j == f
    -
D: Type
cD: Contr D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D
Y -> D exact (const (center D)).
    -
D: Type
cD: Contr D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D
(fun (X Y : Type) (j : X -> Y) (_ : IsEmbedding j)
   (_ : X -> D) => const (center D)) X Y j
  (istruncmap_mapinO_tr j) f o j == f intros x.
D: Type
cD: Contr D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D
x: X
const (center D) (j x) = f x
      exact (contr _).
  Defined.

  (** [Empty] is not algebraically injective. *)
  Definition not_alg_inj_empty@{}
    : IsAlgebraicInjectiveType@{} Empty -> Empty.
IsAlgebraicInjectiveType Empty -> Empty
  Proof.
IsAlgebraicInjectiveType Empty -> Empty
    intros Eai.
Eai: IsAlgebraicInjectiveType Empty
Empty
    refine (lift_ai (Empty_rec@{v}) idmap tt).
Eai: IsAlgebraicInjectiveType Empty
IsEmbedding Empty_rec
    apply istruncmap_mapinO_tr.
Eai: IsAlgebraicInjectiveType Empty
MapIn (Tr (-1)) Empty_rec
    rapply mapinO_between_inO@{uv u v uv}.
  Defined.

End UniverseStructure.

(** [Type@{uv}] is algebraically [u],[v]-injective in at least two ways. *)
Definition alg_inj_Type_sigma@{u v uv suv | u <= uv, v <= uv, uv < suv} `{Univalence}
  : IsAlgebraicInjectiveType@{u v suv uv suv suv} Type@{uv}.
H: Univalence
IsAlgebraicInjectiveType Type
Proof.
H: Univalence
IsAlgebraicInjectiveType Type
  snapply Build_IsAlgebraicInjectiveType; intros X Y j isem f.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> Type
Y -> Type
H: Univalence
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> Type
(fun (X Y : Type) (j : X -> Y) 
   (isem : IsEmbedding j) 
   (f : X -> Type) => ?Goal) X Y j
  (istruncmap_mapinO_tr j) f o j == f
  -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> Type
Y -> Type exact (f <| j).
  -
H: Univalence
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> Type
(fun (X Y : Type) (j : X -> Y) (_ : IsEmbedding j)
   (f : X -> Type) => f <| j) X Y j
  (istruncmap_mapinO_tr j) f o j == f intros x.
H: Univalence
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> Type
x: X
(f <| j) (j x) = f x
    rapply isext_leftkanfam.
Defined.

Instance alg_inj_Type_forall@{u v uv suv | u <= uv, v <= uv, uv < suv} `{Univalence}
  : IsAlgebraicInjectiveType@{u v suv uv suv suv} Type@{uv}.
H: Univalence
IsAlgebraicInjectiveType Type
Proof.
H: Univalence
IsAlgebraicInjectiveType Type
  snapply Build_IsAlgebraicInjectiveType; intros X Y j isem f.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> Type
Y -> Type
H: Univalence
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> Type
(fun (X Y : Type) (j : X -> Y) 
   (isem : IsEmbedding j) 
   (f : X -> Type) => ?Goal) X Y j
  (istruncmap_mapinO_tr j) f o j == f
  -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> Type
Y -> Type exact (f |> j).
  -
H: Univalence
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> Type
(fun (X Y : Type) (j : X -> Y) (_ : IsEmbedding j)
   (f : X -> Type) => f |> j) X Y j
  (istruncmap_mapinO_tr j) f o j == f intros x.
H: Univalence
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> Type
x: X
(f |> j) (j x) = f x 
    rapply isext_rightkanfam.
Defined.

(** ** Constructions with algebraically injective types *)

(** Retracts of algebraically injective types are algebraically injective. *)
Definition alg_inj_retract
  @{u v w w' uv uw vw uw' vw'
  | u <= uv, v <= uv, u <= uw, w <= uw, v <= vw, w <= vw, u <= uw', v <= vw', w' <= uw', w' <= vw'}
  {D' : Type@{w'}} {D : Type@{w}} (r : D -> D') {s : D' -> D}
  (retr : r o s == idmap) (Dai : IsAlgebraicInjectiveType@{u v w uv uw vw} D)
  : IsAlgebraicInjectiveType@{u v w' uv uw' vw'} D'.
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D'
Proof.
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D'
  snapply Build_IsAlgebraicInjectiveType; intros X Y j isem f.
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D'
Y -> D'
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D'
(fun (X Y : Type) (j : X -> Y) 
   (isem : IsEmbedding j) 
   (f : X -> D') => ?Goal) X Y j
  (istruncmap_mapinO_tr j) f o j == f
  -
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D'
Y -> D' exact (r o lift_ai _ (s o f)).
  -
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D'
(fun (X Y : Type) (j : X -> Y) (isem : IsEmbedding j)
   (f : X -> D') => r o lift_ai j (s o f)) X Y j
  (istruncmap_mapinO_tr j) f o j == f intros x.
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D'
x: X
r (lift_ai j (fun x : X => s (f x)) (j x)) = f x rhs_V apply (retr (f x)).
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D'
x: X
r (lift_ai j (fun x : X => s (f x)) (j x)) =
r (s (f x))
    exact (ap r (is_ext_ai _ (s o f) x)).
Defined.

Section UniverseStructure.
  Universes u v w t uv uw vw tw utw vtw.
  Constraint u <= uv, u <= uw, v <= vw, v <= uv, w <= uw, w <= vw, w <= tw, t <= tw,
    uw <= utw, vw <= vtw, tw <= utw, tw <= vtw.

  (** Dependent products are algebraically injective when all their factors are. *)
  #[export] Instance alg_inj_forall@{}
    `{Funext} {A : Type@{t}} (D : A -> Type@{w})
    (Dai : forall a, IsAlgebraicInjectiveType@{u v w uv uw vw} (D a))
    : IsAlgebraicInjectiveType@{u v tw uv utw vtw} (forall a, D a).
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
IsAlgebraicInjectiveType (forall a : A, D a)
  Proof.
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
IsAlgebraicInjectiveType (forall a : A, D a)
    snapply Build_IsAlgebraicInjectiveType; intros X Y j isem f.
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> forall a : A, D a
Y -> forall a : A, D a
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> forall a : A, D a
(fun (X Y : Type) (j : X -> Y) 
   (isem : IsEmbedding j) 
   (f : X -> forall a : A, D a) => 
 ?Goal) X Y j (istruncmap_mapinO_tr j) f o j == f
    -
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> forall a : A, D a
Y -> forall a : A, D a exact (fun y a => lift_ai _ (fun x => f x a) y).
    -
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> forall a : A, D a
(fun (X Y : Type) (j : X -> Y) (isem : IsEmbedding j)
   (f : X -> forall a : A, D a) (y : Y) (a : A) =>
 lift_ai j (fun x : X => f x a) y) X Y j
  (istruncmap_mapinO_tr j) f o j == f intros x.
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> forall a : A, D a
x: X
(fun a : A => lift_ai j (fun x : X => f x a) (j x)) =
f x funext a.
H: Funext
A: Type
D: A -> Type
Dai: forall a : A, IsAlgebraicInjectiveType (D a)
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> forall a : A, D a
x: X
a: A
lift_ai j (fun x : X => f x a) (j x) = f x a
      exact (is_ext_ai _ (fun x => f x a) x).
  Defined.

  (** In particular, exponentials of algebraically injective types are algebraically injective. *)
  Definition alg_inj_arrow@{}
    `{Funext} {A : Type@{t}} {D : Type@{w}}
    (Dai : IsAlgebraicInjectiveType@{u v w uv uw vw} D)
    : IsAlgebraicInjectiveType@{u v tw uv utw vtw} (A -> D)
    := _.

End UniverseStructure.

(** Algebraically injective types are retracts of any type that they embed into. *)
Definition retract_alg_inj_embedding@{v w vw | v <= vw, w <= vw}
  (D : Type@{w}) {Y : Type@{v}} (j : D -> Y) (isem : IsEmbedding j)
  (Dai : IsAlgebraicInjectiveType@{w v w vw w vw} D)
  : { r : Y -> D & r o j == idmap }
  := (lift_ai _ idmap; is_ext_ai _ idmap).

(** Any algebraically [u],[su]-injective type [X : Type@{u}], is a retract of [X -> Type@{u}]. *)
Definition retract_power_universe_alg_usuinj@{u su | u < su} `{Univalence}
  (D : Type@{u}) (Dai : IsAlgebraicInjectiveType@{u su u su u su} D)
  : { r : (D -> Type@{u}) -> D & r o (@paths D) == idmap }
  := retract_alg_inj_embedding D (@paths D) isembedding_paths Dai.

(** ** Algebraic flabbiness and resizing constructions *)
(** If [D : Type@{u}] is algebraically [u],[su]-injective, then it is algebraically [u],[u]-injective. *)
Definition alg_uuinj_alg_usu_inj
  @{u w su uw suw
  | u < su, u <= uw, w <= uw, su <= suw, w <= suw}
  (D : Type@{w}) (Dai : IsAlgebraicInjectiveType@{u su w su uw suw} D)
  : IsAlgebraicInjectiveType@{u u w u uw uw} D.
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D
Proof.
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D
  snapply Build_IsAlgebraicInjectiveType.
D: Type
Dai: IsAlgebraicInjectiveType D
forall (X Y : Type) (j : X -> Y),
IsEmbedding j -> (X -> D) -> Y -> D
D: Type
Dai: IsAlgebraicInjectiveType D
forall (X Y : Type) (j : X -> Y)
(isem : MapIn (Tr (-1)) j) (f : X -> D),
?lift_ai X Y j (istruncmap_mapinO_tr j) f o j == f
  -
D: Type
Dai: IsAlgebraicInjectiveType D
forall (X Y : Type) (j : X -> Y),
IsEmbedding j -> (X -> D) -> Y -> D exact (@lift_ai D Dai).
  -
D: Type
Dai: IsAlgebraicInjectiveType D
forall (X Y : Type) (j : X -> Y)
(isem : MapIn (Tr (-1)) j) (f : X -> D),
(fun X0 Y0 : Type => lift_ai) X Y j
  (istruncmap_mapinO_tr j) f o j == f exact (@is_ext_ai D Dai).
Defined.
(** Note that this proof is easy because of cumulativity of [Type] (which is not assumed in the original paper). *)

(** Algebraic flabbiness is a variant of algebraic injectivity, but only ranging over embeddings of propositions into the unit type. *)
Class IsAlgebraicFlabbyType@{u w} (D : Type@{w}) := {
  center_af {P : HProp@{u}} (f : P -> D) : D;
  contr_af {P : HProp@{u}} (f : P -> D) (p : P) : center_af f = f p;
}.

(** Algebraic flabbiness of a type [D] is equivalent to the statement that all conditionally constant functions [X -> D] are constant. First we give the condition, and then the two implications. *)
Definition cconst_is_const_cond@{u w uw | u <= uw, w <= uw}
  (D : Type@{w})
  := forall (X : Type@{u}) (f : X -> D),
    ConditionallyConstant@{u w uw} f -> sig@{uw uw} (fun d => forall x, d = f x).

Definition alg_flab_cconst_is_const@{u w uw | u <= uw, w <= uw}
  (D : Type@{w}) (ccond : cconst_is_const_cond@{u w uw} D)
  : IsAlgebraicFlabbyType@{u w} D.
D: Type
ccond: cconst_is_const_cond D
IsAlgebraicFlabbyType D
Proof.
D: Type
ccond: cconst_is_const_cond D
IsAlgebraicFlabbyType D
  snapply Build_IsAlgebraicFlabbyType; intros P f.
D: Type
ccond: cconst_is_const_cond D
P: HProp
f: P -> D
D
D: Type
ccond: cconst_is_const_cond D
P: HProp
f: P -> D
forall p : P,
(fun (P : HProp) (f : P -> D) => ?Goal) P f = f p
  -
D: Type
ccond: cconst_is_const_cond D
P: HProp
f: P -> D
D apply (ccond P f).
D: Type
ccond: cconst_is_const_cond D
P: HProp
f: P -> D
ConditionallyConstant f
    apply (cconst_factors_hprop _ _ idmap f).
D: Type
ccond: cconst_is_const_cond D
P: HProp
f: P -> D
(fun x : P => f x) == f
    reflexivity.
  -
D: Type
ccond: cconst_is_const_cond D
P: HProp
f: P -> D
forall p : P,
(fun (P : HProp) (f : P -> D) =>
 let X :=
   fun H : ConditionallyConstant f => (ccond P f H).1
   in
 X
   (cconst_factors_hprop f P idmap f (fun x0 : P => 1)))
  P f = f p apply (ccond P f).
Defined.

Definition cconst_is_const_alg_flab@{u w uw | u <= uw, w <= uw}
  (D : Type@{w}) (Daf : IsAlgebraicFlabbyType@{u w} D)
  : cconst_is_const_cond@{u w uw} D.
D: Type
Daf: IsAlgebraicFlabbyType D
cconst_is_const_cond D
Proof.
D: Type
Daf: IsAlgebraicFlabbyType D
cconst_is_const_cond D
  intros X f [f' e].
D: Type
Daf: IsAlgebraicFlabbyType D
X: Type
f: X -> D
f': Trunc (-1) X -> D
e: forall x : X, f' (tr x) = f x
{d : D & forall x : X, d = f x}
  srefine (center_af f'; _).
D: Type
Daf: IsAlgebraicFlabbyType D
X: Type
f: X -> D
f': Trunc (-1) X -> D
e: forall x : X, f' (tr x) = f x
(fun d : D => forall x : X, d = f x) (center_af f')
  intros x.
D: Type
Daf: IsAlgebraicFlabbyType D
X: Type
f: X -> D
f': Trunc (-1) X -> D
e: forall x : X, f' (tr x) = f x
x: X
center_af f' = f x
  exact (contr_af f' (tr x) @ e x).
Defined.

(** Algebraic flabbiness is equivalent to algebraic injectivity, with appropriate choices of universes. *)
Section UniverseStructure.
  Universes u v w uv uw vw.
  Constraint u <= uv, v <= uv, u <= uw, w <= uw, v <= vw, w <= vw.

  (** Algebraically [u],[v]-injective types are algebraically [u]-flabby. *)
  Definition alg_flab_alg_inj@{}
    {D : Type@{w}} (Dai : IsAlgebraicInjectiveType@{u v w uv uw vw} D)
    : IsAlgebraicFlabbyType@{u w} D.
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicFlabbyType D
  Proof.
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicFlabbyType D
    snapply Build_IsAlgebraicFlabbyType; intros P f.
D: Type
Dai: IsAlgebraicInjectiveType D
P: HProp
f: P -> D
D
D: Type
Dai: IsAlgebraicInjectiveType D
P: HProp
f: P -> D
forall p : P,
(fun (P : HProp) (f : P -> D) => ?Goal) P f = f p
    -
D: Type
Dai: IsAlgebraicInjectiveType D
P: HProp
f: P -> D
D srapply (lift_ai _ f tt).
    -
D: Type
Dai: IsAlgebraicInjectiveType D
P: HProp
f: P -> D
forall p : P,
(fun (P : HProp) (f : P -> D) =>
 lift_ai (fun _ : P => ?y) f tt) P f = f p apply is_ext_ai.
  Defined.

  (** Algebraically [uv]-flabby types are algebraically [u],[v]-injective. *)
  Definition alg_inj_alg_flab@{}
    {D : Type@{w}} (Daf : IsAlgebraicFlabbyType@{uv w} D)
    : IsAlgebraicInjectiveType@{u v w uv uw vw} D.
D: Type
Daf: IsAlgebraicFlabbyType D
IsAlgebraicInjectiveType D
  Proof.
D: Type
Daf: IsAlgebraicFlabbyType D
IsAlgebraicInjectiveType D
    snapply Build_IsAlgebraicInjectiveType; intros X Y j isem f.
D: Type
Daf: IsAlgebraicFlabbyType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D
Y -> D
D: Type
Daf: IsAlgebraicFlabbyType D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D
(fun (X Y : Type) (j : X -> Y) 
   (isem : IsEmbedding j) 
   (f : X -> D) => ?Goal) X Y j
  (istruncmap_mapinO_tr j) f o j == f
    -
D: Type
Daf: IsAlgebraicFlabbyType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D
Y -> D intros y.
D: Type
Daf: IsAlgebraicFlabbyType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D
y: Y
D exact (center_af (fun x : Build_HProp (hfiber j y) => f x.1)).
    -
D: Type
Daf: IsAlgebraicFlabbyType D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D
(fun (X Y : Type) (j : X -> Y) (isem : IsEmbedding j)
   (f : X -> D) (y : Y) =>
 center_af (fun x : Build_HProp (hfiber j y) => f x.1))
  X Y j (istruncmap_mapinO_tr j) f o j == f intros x.
D: Type
Daf: IsAlgebraicFlabbyType D
X, Y: Type
j: X -> Y
isem: MapIn (Tr (-1)) j
f: X -> D
x: X
center_af
  (fun x : Build_HProp (hfiber j (j x)) => f x.1) =
f x exact (contr_af _ (x; idpath (j x))).
  Defined.

End UniverseStructure.

(** By combining the above, we see that if [D] is algebraically [ut],[v]-injective, then it is algebraically [u],[t]-injective. *)
Definition resize_alg_inj
  @{u v w t ut uw vw tw uvt utw
  | u <= ut, u <= uw, v <= vw, v <= uvt, w <= uw, w <= vw, w <= tw,
    t <= ut, t <= tw, ut <= uvt, ut <= utw, uw <= utw, tw <= utw}
  {D : Type@{w}} (Dai : IsAlgebraicInjectiveType@{ut v w uvt utw vw} D)
  : IsAlgebraicInjectiveType@{u t w ut uw tw} D.
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D
Proof.
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D
  apply alg_inj_alg_flab.
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicFlabbyType D
  exact (alg_flab_alg_inj Dai).
Defined.

(** We include two direct proofs of the algebraic flabbiness of [Type], instead of combining [alg_inj_alg_flab] with the previous proofs of algebraic injectivity, for better computations later. *)
Definition alg_flab_Type_sigma@{u su | u < su} `{Univalence}
  : IsAlgebraicFlabbyType@{u su} Type@{u}.
H: Univalence
IsAlgebraicFlabbyType Type
Proof.
H: Univalence
IsAlgebraicFlabbyType Type
  snapply Build_IsAlgebraicFlabbyType; intros P A.
H: Univalence
P: HProp
A: P -> Type
Type
H: Univalence
P: HProp
A: P -> Type
forall p : P,
(fun (P : HProp) (A : P -> Type) => ?Goal) P A = A p
  -
H: Univalence
P: HProp
A: P -> Type
Type exact (sig@{u u} (fun p => A p)).
  -
H: Univalence
P: HProp
A: P -> Type
forall p : P,
(fun (P : HProp) (A : P -> Type) => {p0 : P & A p0}) P
  A = A p intros p.
H: Univalence
P: HProp
A: P -> Type
p: P
(fun (P : HProp) (A : P -> Type) => {p : P & A p}) P A =
A p
    apply path_universe_uncurried.
H: Univalence
P: HProp
A: P -> Type
p: P
{p : P & A p} <~> A p
    exact (@equiv_contr_sigma _ _ (contr_inhabited_hprop _ _)).
Defined.

Instance alg_flab_Type_forall@{u su | u < su} `{Univalence}
  : IsAlgebraicFlabbyType@{u su} Type@{u}.
H: Univalence
IsAlgebraicFlabbyType Type
Proof.
H: Univalence
IsAlgebraicFlabbyType Type
  snapply Build_IsAlgebraicFlabbyType; intros P A.
H: Univalence
P: HProp
A: P -> Type
Type
H: Univalence
P: HProp
A: P -> Type
forall p : P,
(fun (P : HProp) (A : P -> Type) => ?Goal) P A = A p
  -
H: Univalence
P: HProp
A: P -> Type
Type exact (forall p : P, A p).
  -
H: Univalence
P: HProp
A: P -> Type
forall p : P,
(fun (P : HProp) (A : P -> Type) =>
 forall p0 : P, A p0) P A = A p intros p.
H: Univalence
P: HProp
A: P -> Type
p: P
(fun (P : HProp) (A : P -> Type) => forall p : P, A p)
  P A = A p
    apply path_universe_uncurried.
H: Univalence
P: HProp
A: P -> Type
p: P
(forall p : P, A p) <~> A p
    exact (@equiv_contr_forall _ _ (contr_inhabited_hprop _ _) _).
Defined.

(** ** Algebraic flabbiness with resizing axioms *)

Section AssumePropResizing.
  Context `{PropResizing}.

  (** Algebraic flabbiness is independent of universes under propositional resizing. *)
  Definition universe_independent_alg_flab@{v u w}
    {D : Type@{w}} (Daf : IsAlgebraicFlabbyType@{v w} D)
    : IsAlgebraicFlabbyType@{u w} D.
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
IsAlgebraicFlabbyType D
  Proof.
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
IsAlgebraicFlabbyType D
    snapply Build_IsAlgebraicFlabbyType; intros P f;
    pose (e := (equiv_smalltype@{v u} P));
    pose (PropQ := (@istrunc_equiv_istrunc _ _ e^-1 (-1) _)).
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
P: HProp
f: P -> D
e:= equiv_smalltype P: smalltype P <~> P
PropQ:= istrunc_equiv_istrunc P e^-1: IsHProp (smalltype P)
D
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
P: HProp
f: P -> D
e:= equiv_smalltype P: smalltype P <~> P
PropQ:= istrunc_equiv_istrunc P e^-1: IsHProp (smalltype P)
forall p : P,
(fun (P : HProp) (f : P -> D) =>
 let e := equiv_smalltype P in
 let PropQ := istrunc_equiv_istrunc P e^-1 in ?Goal) P
  f = f p
    -
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
P: HProp
f: P -> D
e:= equiv_smalltype P: smalltype P <~> P
PropQ:= istrunc_equiv_istrunc P e^-1: IsHProp (smalltype P)
D exact (center_af (f o e)).
    -
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
P: HProp
f: P -> D
e:= equiv_smalltype P: smalltype P <~> P
PropQ:= istrunc_equiv_istrunc P e^-1: IsHProp (smalltype P)
forall p : P,
(fun (P : HProp) (f : P -> D) =>
 let e := equiv_smalltype P in
 let PropQ := istrunc_equiv_istrunc P e^-1 in
 center_af (f o e)) P f = f p intros p.
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
P: HProp
f: P -> D
e:= equiv_smalltype P: smalltype P <~> P
PropQ:= istrunc_equiv_istrunc P e^-1: IsHProp (smalltype P)
p: P
(fun (P : HProp) (f : P -> D) =>
 let e := equiv_smalltype P in
 let PropQ := istrunc_equiv_istrunc P e^-1 in
 center_af (f o e)) P f = f p
      lhs apply (contr_af (f o e) (e^-1 p)).
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
P: HProp
f: P -> D
e:= equiv_smalltype P: smalltype P <~> P
PropQ:= istrunc_equiv_istrunc P e^-1: IsHProp (smalltype P)
p: P
f (e (e^-1 p)) = f p
      apply ap.
H: PropResizing
D: Type
Daf: IsAlgebraicFlabbyType D
P: HProp
f: P -> D
e:= equiv_smalltype P: smalltype P <~> P
PropQ:= istrunc_equiv_istrunc P e^-1: IsHProp (smalltype P)
p: P
e (e^-1 p) = p
      apply eisretr.
  Defined.

  (** Algebraic injectivity is independent of universes under propositional resizing. *)
  Definition universe_independent_alg_inj
    @{u v w u' v' uv uw vw u'v' u'w v'w
    | u <= uv, v <= uv, u <= uw, w <= uw, v <= vw, w <= vw,
      u' <= u'v', v' <= u'v', u' <= u'w, w <= u'w, v' <= v'w, w <= v'w}
    {D : Type@{w}} (Dai : IsAlgebraicInjectiveType@{u v w uv uw vw} D)
    : IsAlgebraicInjectiveType@{u' v' w u'v' u'w v'w} D.
H: PropResizing
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D
  Proof.
H: PropResizing
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D
    apply alg_inj_alg_flab.
H: PropResizing
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicFlabbyType D
    apply universe_independent_alg_flab@{u u'v' w}.
H: PropResizing
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicFlabbyType D
    exact (alg_flab_alg_inj Dai).
  Defined.

  (** Any algebraically injective type [D : Type@{u}] is a retract of [X -> Type@{u}] with [X : Type@{u}]. This is a universe independent version of [retract_power_universe_alg_usuinj]. *)
  Definition retract_power_universe_alg_inj@{u su | u < su} `{Univalence}
    {D : Type@{u}} (Dai : IsAlgebraicInjectiveType@{u u u u u u} D)
    : exists (X : Type@{u}) (s : D -> (X -> Type@{u})) (r : (X -> Type@{u}) -> D), r o s == idmap.
H: PropResizing
H0: Univalence
D: Type
Dai: IsAlgebraicInjectiveType D
{X : Type &
{s : D -> X -> Type &
{r : (X -> Type) -> D & r o s == idmap}}}
  Proof.
H: PropResizing
H0: Univalence
D: Type
Dai: IsAlgebraicInjectiveType D
{X : Type &
{s : D -> X -> Type &
{r : (X -> Type) -> D & r o s == idmap}}}
    refine (D; _).
H: PropResizing
H0: Univalence
D: Type
Dai: IsAlgebraicInjectiveType D
{s : D -> D -> Type &
{r : (D -> Type) -> D &
(fun x : D => r (s x)) == idmap}}
    refine (@paths D; _).
H: PropResizing
H0: Univalence
D: Type
Dai: IsAlgebraicInjectiveType D
{r : (D -> Type) -> D &
(fun x : D => r (paths x)) == idmap}
    apply (retract_power_universe_alg_usuinj D).
H: PropResizing
H0: Univalence
D: Type
Dai: IsAlgebraicInjectiveType D
IsAlgebraicInjectiveType D
    exact (universe_independent_alg_inj@{u u u u su u u u su u su} Dai).
  Defined.

End AssumePropResizing.

(** Any retract of a type family [X -> Type@{u}] is algebraically injective. This is the opposite result as above, classifying algebraically injective types, independent of universes. It should be noted that this direction of the if and only if does not depend on propositional resizing. *)
Definition alg_inj_retract_power_universe@{u su | u < su}
  `{Univalence} (D : Type@{u}) {X : Type@{u}} {s : D -> (X -> Type@{u})}
  (r : (X -> Type@{u}) -> D) (retr : r o s == idmap)
  : IsAlgebraicInjectiveType@{u u u u u u} D.
H: Univalence
D, X: Type
s: D -> X -> Type
r: (X -> Type) -> D
retr: r o s == idmap
IsAlgebraicInjectiveType D
Proof.
H: Univalence
D, X: Type
s: D -> X -> Type
r: (X -> Type) -> D
retr: r o s == idmap
IsAlgebraicInjectiveType D
  apply (alg_inj_retract r retr).
H: Univalence
D, X: Type
s: D -> X -> Type
r: (X -> Type) -> D
retr: r o s == idmap
IsAlgebraicInjectiveType (X -> Type)
  rapply alg_inj_arrow.
Defined.

(** ** Injectivity in terms of algebraic injectivity in the absence of resizing *)

Section UniverseStructure.
  Universes u v w uv uw vw uvw.
  Constraint u <= uv, v <= uv, u <= uw, w <= uw, v <= vw, w <= vw,
    uv <= uvw, uw <= uvw, vw <= uvw.

  (** Algebraically injective types are injective. *)
  Definition inj_alg_inj@{}
    (D : Type@{w}) (Dai : IsAlgebraicInjectiveType@{u v w uv uw vw} D)
    : IsInjectiveType@{u v w uv uw vw uvw} D.
D: Type
Dai: IsAlgebraicInjectiveType D
IsInjectiveType D
  Proof.
D: Type
Dai: IsAlgebraicInjectiveType D
IsInjectiveType D
    intros X Y j isem f.
D: Type
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D
merely {f' : Y -> D & (fun x : X => f' (j x)) == f}
    apply tr.
D: Type
Dai: IsAlgebraicInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D
{f' : Y -> D & (fun x : X => f' (j x)) == f}
    exact (lift_ai _ _; is_ext_ai _ f).
  Defined.

  (** The propositional truncation of algebraic injectivity implies injectivity. *)
  Definition inj_merely_alg_inj@{T | uvw < T}
    `{Funext} {D : Type@{w}}
    (mDai : merely@{T} (IsAlgebraicInjectiveType@{u v w uv uw vw} D))
    : ((IsInjectiveType@{u v w uv uw vw uvw} D) : Type@{T}).
H: Funext
D: Type
mDai: merely (IsAlgebraicInjectiveType D)
IsInjectiveType D : Type
  Proof.
H: Funext
D: Type
mDai: merely (IsAlgebraicInjectiveType D)
IsInjectiveType D : Type
    revert mDai.
H: Funext
D: Type
merely (IsAlgebraicInjectiveType D) ->
IsInjectiveType D : Type
    napply Trunc_rec@{T T}. (* Manually stripping truncations so as to control universe variables. *)
H: Funext
D: Type
IsHProp (IsInjectiveType D)
H: Funext
D: Type
IsAlgebraicInjectiveType D -> IsInjectiveType D
    -
H: Funext
D: Type
IsHProp (IsInjectiveType D) repeat (napply istrunc_forall@{T T T}; intro).
H: Funext
D, a, a0: Type
a1: a -> a0
a2: IsEmbedding a1
a3: a -> D
IsHProp
  (merely
     {f' : a0 -> D & (fun x : a => f' (a1 x)) == a3})
      apply istrunc_truncation.
    -
H: Funext
D: Type
IsAlgebraicInjectiveType D -> IsInjectiveType D intro Dai.
H: Funext
D: Type
Dai: IsAlgebraicInjectiveType D
IsInjectiveType D
      exact (inj_alg_inj@{} D Dai).
  Defined.

  (** A retract of an injective type is injective. *)
  Definition inj_retract
    @{w' uw' vw' uvw' T
    | u <= uw', v <= vw', w' <= uw', w' <= vw', 
    uv <= uvw', uw' <= uvw', vw' <= uvw', uvw < T, uvw' < T}
    `{Funext} {D' : Type@{w'}} {D : Type@{w}} (r : D -> D') {s : D' -> D}
    (retr : r o s == idmap) (Di : IsInjectiveType@{u v w uv uw vw uvw} D)
    : IsInjectiveType@{u v w' uv uw' vw' uvw'} D'.
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Di: IsInjectiveType D
IsInjectiveType D'
  Proof.
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Di: IsInjectiveType D
IsInjectiveType D'
    intros X Y j isem f.
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> D'
merely {f' : Y -> D' & (fun x : X => f' (j x)) == f}
    specialize (Di X Y j isem (s o f)).
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
Di: merely {f' : Y -> D & f' o j == s o f}
isem: IsEmbedding j
merely {f' : Y -> D' & (fun x : X => f' (j x)) == f}
    revert Di.
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
isem: IsEmbedding j
merely {f' : Y -> D & f' o j == s o f} ->
merely {f' : Y -> D' & (fun x : X => f' (j x)) == f}
    rapply Trunc_rec@{T T}.
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
isem: IsEmbedding j
{f' : Y -> D &
(fun x : X => f' (j x)) == (fun x : X => s (f x))} ->
merely {f' : Y -> D' & (fun x : X => f' (j x)) == f}
    intros [g e].
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
isem: IsEmbedding j
g: Y -> D
e: (fun x : X => g (j x)) == (fun x : X => s (f x))
merely {f' : Y -> D' & (fun x : X => f' (j x)) == f}
    apply tr.
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
isem: IsEmbedding j
g: Y -> D
e: (fun x : X => g (j x)) == (fun x : X => s (f x))
{f' : Y -> D' & (fun x : X => f' (j x)) == f}
    snrefine (r o g; _).
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
isem: IsEmbedding j
g: Y -> D
e: (fun x : X => g (j x)) == (fun x : X => s (f x))
(fun f' : Y -> D' => (fun x : X => f' (j x)) == f)
  (r o g)
    intros x.
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
isem: IsEmbedding j
g: Y -> D
e: (fun x : X => g (j x)) == (fun x : X => s (f x))
x: X
r (g (j x)) = f x
    rhs_V apply (retr (f x)).
H: Funext
D', D: Type
r: D -> D'
s: D' -> D
retr: r o s == idmap
X, Y: Type
j: X -> Y
f: X -> D'
isem: IsEmbedding j
g: Y -> D
e: (fun x : X => g (j x)) == (fun x : X => s (f x))
x: X
r (g (j x)) = r (s (f x))
    exact (ap r (e x)).
  Defined.

End UniverseStructure.

(** Injective types are retracts of any type that they embed into, in an unspecified way. *)
Definition merely_retract_inj_embedding@{v w vw svw | v <= vw, w <= vw, vw < svw}
  (D : Type@{w}) {Y : Type@{v}} (j : D -> Y) (isem : IsEmbedding j)
  (Di : IsInjectiveType@{w v w vw w vw vw} D)
  : merely@{svw} { r : Y -> D & r o j == idmap }
  := Di _ _ _ _ idmap.

(** The power of an injective type is injective. *)
Definition inj_arrow
  @{u v w t uv ut vt tw uvt utw vtw utvw
  | u <= uv, v <= uv, u <= ut, t <= ut, v <= vt, t <= vt, t <= tw, w <= tw, uv <= uvt, ut <= uvt,
    vt <= uvt, ut <= utw, tw <= utw, vt <= vtw, tw <= vtw, uvt <= utvw, utw <= utvw, vtw <= utvw}
  `{Funext} {A : Type@{t}} (D : Type@{w})
  (Di : IsInjectiveType@{ut vt w uvt utw vtw utvw} D)
  : IsInjectiveType@{u v tw uv utw vtw utvw} (A -> D).
H: Funext
A, D: Type
Di: IsInjectiveType D
IsInjectiveType (A -> D)
Proof.
H: Funext
A, D: Type
Di: IsInjectiveType D
IsInjectiveType (A -> D)
  intros X Y j isem f.
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
merely
  {f' : Y -> A -> D & (fun x : X => f' (j x)) == f}
  assert (embId : IsEmbedding (fun a : A => a)) by rapply istruncmap_mapinO_tr.
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
merely
  {f' : Y -> A -> D & (fun x : X => f' (j x)) == f}
  pose proof (mD := Di (X * A) (Y * A) (functor_prod j equiv_idmap)
    (istruncmap_functor_prod@{u v t t ut vt uvt uvt uv t} _ _ _) (uncurry f)).
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
mD: merely
  {f' : Y * A -> D &
  f' o functor_prod j 1%equiv == uncurry f}
merely
  {f' : Y -> A -> D & (fun x : X => f' (j x)) == f}
  revert mD.
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
merely
  {f' : Y * A -> D &
  f' o functor_prod j 1%equiv == uncurry f} ->
merely
  {f' : Y -> A -> D & (fun x : X => f' (j x)) == f}
  rapply Trunc_rec@{utvw utvw}.
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
{f' : Y * A -> D &
(fun x : X * A => f' (functor_prod j 1%equiv x)) ==
uncurry f} ->
merely
  {f' : Y -> A -> D & (fun x : X => f' (j x)) == f}
  intros [g e].
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
g: Y * A -> D
e: (fun x : X * A => g (functor_prod j 1%equiv x)) ==
uncurry f
merely
  {f' : Y -> A -> D & (fun x : X => f' (j x)) == f}
  apply tr.
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
g: Y * A -> D
e: (fun x : X * A => g (functor_prod j 1%equiv x)) ==
uncurry f
{f' : Y -> A -> D & (fun x : X => f' (j x)) == f}
  refine (fun y a => g (y, a); _).
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
g: Y * A -> D
e: (fun x : X * A => g (functor_prod j 1%equiv x)) ==
uncurry f
(fun (x : X) (a : A) => g (j x, a)) == f
  intros x.
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
g: Y * A -> D
e: (fun x : X * A => g (functor_prod j 1%equiv x)) ==
uncurry f
x: X
(fun a : A => g (j x, a)) = f x funext a.
H: Funext
A, D: Type
Di: IsInjectiveType D
X, Y: Type
j: X -> Y
isem: IsEmbedding j
f: X -> A -> D
embId: IsEmbedding idmap
g: Y * A -> D
e: (fun x : X * A => g (functor_prod j 1%equiv x)) ==
uncurry f
x: X
a: A
g (j x, a) = f x a
  exact (e (x, a)).
Defined.

(** Any [u],[su]-injective type [X : Type@{u}], is a retract of [X -> Type@{u}] in an unspecified way. *)
Definition merely_retract_power_universe_inj@{u su ssu | u < su, su < ssu}
  `{Univalence} (D : Type@{u}) (Di : IsInjectiveType@{u su u su u su su} D)
  : merely@{su} (sig@{su su} (fun r => r o (@paths D) == idmap))
  := merely_retract_inj_embedding D (@paths D) isembedding_paths Di.

(** Inverse of [inj_merely_alg_inj] modulo universes. *)
Definition merely_alg_inj_inj@{u su ssu | u < su, su < ssu} `{Univalence}
  (D : Type@{u}) (Di : IsInjectiveType@{u su u su u su su} D)
  : merely@{su} (IsAlgebraicInjectiveType@{u u u u u u} D).
H: Univalence
D: Type
Di: IsInjectiveType D
merely (IsAlgebraicInjectiveType D)
Proof.
H: Univalence
D: Type
Di: IsInjectiveType D
merely (IsAlgebraicInjectiveType D)
  srefine (Trunc_functor (-1) _ (merely_retract_power_universe_inj D Di)).
H: Univalence
D: Type
Di: IsInjectiveType D
{r : (D -> Type) -> D & r o paths == idmap} ->
IsAlgebraicInjectiveType D
  intros [r retr].
H: Univalence
D: Type
Di: IsInjectiveType D
r: (D -> Type) -> D
retr: (fun x : D => r (paths x)) == idmap
IsAlgebraicInjectiveType D
  exact (alg_inj_retract_power_universe D r retr).
Defined.

(** ** The equivalence of excluded middle with the (algebraic) injectivity of pointed types *)

(** Assuming excluded middle, all pointed types are algebraically flabby (and thus algebraically injective). *)
Definition alg_flab_pointed_lem@{u w}
  `{ExcludedMiddle} {D : Type@{w}} (d : D)
  : IsAlgebraicFlabbyType@{u w} D.
H: ExcludedMiddle
D: Type
d: D
IsAlgebraicFlabbyType D
Proof.
H: ExcludedMiddle
D: Type
d: D
IsAlgebraicFlabbyType D
  snapply Build_IsAlgebraicFlabbyType; intros P f.
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
D
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
forall p : P,
(fun (P : HProp) (f : P -> D) => ?Goal) P f = f p
  -
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
D destruct (LEM P _) as [p | np].
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
p: P
D
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
np: ~ P
D
    +
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
p: P
D exact (f p).
    +
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
np: ~ P
D exact d.
  -
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
forall p : P,
(fun (P : HProp) (f : P -> D) =>
 let s := LEM P (trunctype_istrunc P) in
 match s with
 | inl t => (fun p0 : P => f p0) t
 | inr n => (fun _ : ~ P => d) n
 end) P f = f p cbn.
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
forall p : P,
match LEM P (trunctype_istrunc P) with
| inl t => f t
| inr _ => d
end = f p  intros q.
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
q: P
match LEM P (trunctype_istrunc P) with
| inl t => f t
| inr _ => d
end = f q
    destruct (LEM P _) as [p | np].
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
q, p: P
f p = f q
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
q: P
np: ~ P
d = f q
    +
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
q, p: P
f p = f q exact (ap f (path_ishprop _ _)).
    +
H: ExcludedMiddle
D: Type
d: D
P: HProp
f: P -> D
q: P
np: ~ P
d = f q exact (Empty_rec (np q)).
Defined.

(** If the type [P + ~P + Unit] is algebraically flabby for [P] a proposition, then [P] is decidable. *)
Definition decidable_alg_flab_hprop@{w} `{Funext} (P : HProp@{w})
  (Paf : IsAlgebraicFlabbyType@{w w} ((P + ~P) + (Unit : Type@{w})))
  : Decidable P.
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
Decidable P
Proof.
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
Decidable P
  pose (inl' := inl : P + ~P -> (P + ~P) + (Unit : Type@{w})).
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
Decidable P
  assert (l : {d : (P + ~P) + (Unit : Type@{w}) & forall z, d = inl' z}).
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
{d : P + ~ P + Unit & forall z : P + ~ P, d = inl' z}
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
l: {d : P + ~ P + (Unit : Type) &
forall z : P + ~ P, d = inl' z}
Decidable P
  {
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
{d : P + ~ P + Unit & forall z : P + ~ P, d = inl' z} refine (center_af _; contr_af inl').
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
IsHProp (P + ~ P) rapply ishprop_decidable_hprop@{w w}. }
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
l: {d : P + ~ P + (Unit : Type) &
forall z : P + ~ P, d = inl' z}
Decidable P
  destruct l as [[s | u] l2].
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
s: P + ~ P
l2: forall z : P + ~ P, inl s = inl' z
Decidable P
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
u: Unit
l2: forall z : P + ~ P, inr u = inl' z
Decidable P
  -
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
s: P + ~ P
l2: forall z : P + ~ P, inl s = inl' z
Decidable P exact s.
  -
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
u: Unit
l2: forall z : P + ~ P, inr u = inl' z
Decidable P assert (np := fun p => inl_ne_inr _ _ (l2 (inl p))^).
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
u: Unit
l2: forall z : P + ~ P, inr u = inl' z
np: P -> Empty
Decidable P
    assert (nnp := fun np' => inl_ne_inr _ _ (l2 (inr np'))^).
H: Funext
P: HProp
Paf: IsAlgebraicFlabbyType (P + ~ P + (Unit : Type))
inl':= inl : P + ~ P -> P + ~ P + (Unit : Type): P + ~ P -> P + ~ P + (Unit : Type)
u: Unit
l2: forall z : P + ~ P, inr u = inl' z
np: P -> Empty
nnp: ~ P -> Empty
Decidable P
    exact (Empty_rec (nnp np)).
Defined.

(** If all pointed types are algebraically flabby, then excluded middle holds. *)
Definition lem_pointed_types_alg_flab@{w} `{Funext}
  (ptaf: forall (D : Type@{w}), D -> IsAlgebraicFlabbyType@{w w} D)
  : ExcludedMiddle_type@{w}.
H: Funext
ptaf: forall D : Type, D -> IsAlgebraicFlabbyType D
ExcludedMiddle_type
Proof.
H: Funext
ptaf: forall D : Type, D -> IsAlgebraicFlabbyType D
ExcludedMiddle_type
  intros P PropP.
H: Funext
ptaf: forall D : Type, D -> IsAlgebraicFlabbyType D
P: Type
PropP: IsHProp P
P + ~ P
  apply (decidable_alg_flab_hprop (Build_HProp P)).
H: Funext
ptaf: forall D : Type, D -> IsAlgebraicFlabbyType D
P: Type
PropP: IsHProp P
IsAlgebraicFlabbyType
  (Build_HProp P + ~ Build_HProp P + Unit)
  apply ptaf.
H: Funext
ptaf: forall D : Type, D -> IsAlgebraicFlabbyType D
P: Type
PropP: IsHProp P
Build_HProp P + ~ Build_HProp P + Unit
  exact (inr tt).
Defined.