(** * Injectivity of Sigma types *)

(** Here we characterize the condition for which a sigma type over an injective type is itself injective, and we also provide some examples.

Many proofs guided by original Agda formalization in the Type Topology Library which can be found at: https://martinescardo.github.io/TypeTopology/InjectiveTypes.Sigma and InjectiveTypes.MathematicalStructuresMoreGeneral. *)

Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Forall Types.Sigma Types.Universe.
Require Import Modalities.ReflectiveSubuniverse.
Require Import Truncations.Core.
Require Import InjectiveTypes.InjectiveTypes InjectiveTypes.TypeFamKanExt.

Section AlgFlabSigma.
  Context {X : Type} (A : X -> Type) (Xaf : IsAlgebraicFlabbyType X).

  (** The condition for a sigma type over an algebraically flabby type to be algebraically flabby can be described as the existence of a section to the following map for every [P] and [f]. *)
  Definition alg_flab_map (P : HProp) (f : P -> X)
    : (A (center_af f)) -> (forall h, A (f h))
    := fun a h => contr_af f h # a.

  (** Here is the condition.  (It would in fact be enough to assume that [s] is section up to homotopies in its domain.) *)
  Definition alg_flab_sigma_condition
    := forall P f, {s : _ & alg_flab_map P f o s == idmap}.

  (** A sigma type over an algebraically flabby type is also algebraically flabby, and thus algebraically injective, when the above condition holds. *)
  Definition alg_flab_sigma (cond : alg_flab_sigma_condition)
    : IsAlgebraicFlabbyType {x : X & A x}.
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
IsAlgebraicFlabbyType {x : X & A x}
  Proof.
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
IsAlgebraicFlabbyType {x : X & A x}
    snapply Build_IsAlgebraicFlabbyType; intros P f.
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
{x : X & A x}
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
forall p : P,
(fun (P : HProp) (f : P -> {x : X & A x}) => ?Goal) P
  f = f p
    all: pose (C := cond P (pr1 o f)).
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
{x : X & A x}
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
forall p : P,
(fun (P : HProp) (f : P -> {x : X & A x}) =>
 let C := cond P (pr1 o f) in ?Goal) P f = 
f p
    - (* We need to give a point in [{x : X * A x}].  Since [X] is algebraically flabby, we get a point in [X]: *)
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
{x : X & A x}
      exists (center_af (pr1 o f)).
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
A (center_af (fun x : P => (f x).1))
      (* For the point in [A (above)], we use the section component of [cond P (pr1 o f)]: *)
      exact (C.1 (pr2 o f)).
    -
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
forall p : P,
(fun (P : HProp) (f : P -> {x : X & A x}) =>
 let C := cond P (pr1 o f) in
 (center_af (fun x : P => (f x).1); C.1 (pr2 o f))) P
  f = f p intros h; cbn.
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
h: P
(center_af (fun x : P => (f x).1);
(cond P (fun x : P => (f x).1)).1
  (fun x : P => (f x).2)) = f h
      change (cond P (fun x : P => (f x).1)) with C.
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
h: P
(center_af (fun x : P => (f x).1);
C.1 (fun x : P => (f x).2)) = f h
      (* We need to show that the point we gave is equal to [f h]. *)
      snapply path_sigma; cbn.
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
h: P
center_af (fun x : P => (f x).1) = (f h).1
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
h: P
transport (fun x : X => A x) 
  ?Goal (C.1 (fun x : P => (f x).2)) = 
(f h).2
      +
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
h: P
center_af (fun x : P => (f x).1) = (f h).1 napply contr_af.
      +
X: Type
A: X -> Type
Xaf: IsAlgebraicFlabbyType X
cond: alg_flab_sigma_condition
P: HProp
f: P -> {x : X & A x}
C:= cond P (pr1 o f): {s
: (forall h : P, A ((pr1 o f) h)) ->
  A (center_af (pr1 o f)) &
alg_flab_map P (pr1 o f) o s == idmap}
h: P
transport (fun x : X => A x)
  (contr_af (fun x : P => (f x).1) h)
  (C.1 (fun x : P => (f x).2)) = (f h).2 exact (apD10 (C.2 (pr2 o f)) h).
  Defined.

  Definition alg_inj_sigma (cond : alg_flab_sigma_condition)
    : IsAlgebraicInjectiveType {x : X & A x}
    := alg_inj_alg_flab (alg_flab_sigma cond).

End AlgFlabSigma.

(** Taking our algebraically flabby type [X] to be [Type], we introduce our primary examples (the types of pointed types, monoids, etc.), and give a few simplifying lemmas. *)
Section AlgFlabUniverse.
  (** [T] is a version of transport in the type family [A].  It could be defined to be transport combined with univalence, but we allow the user to choose different "implementations" of transport that might be more convenient. *)
  Context (A : Type -> Type) (T : forall {X Y}, X <~> Y -> A X -> A Y)
    (Trefl : forall X, (T (equiv_idmap X) == idmap)).
  Arguments T {X Y} _ _. (* This is needed, despite the braces above. *)

  (** When studying the sigma type [{X : Type & A X}], the map [alg_flab_map] can be exchanged for either of these simpler maps.  This first one will turn out to be homotopic to [alg_flab_map] when [Type] is given its "forall" flabbiness structure. *)
  Definition alg_flab_map_forall `{Funext}
    (P : HProp) (f : P -> Type)
    : A (forall h, f h) -> (forall h, A (f h)).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Funext
P: HProp
f: P -> Type
A (forall h : P, f h) -> forall h : P, A (f h)
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Funext
P: HProp
f: P -> Type
A (forall h : P, f h) -> forall h : P, A (f h)
    intros a h.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Funext
P: HProp
f: P -> Type
a: A (forall h : P, f h)
h: P
A (f h)
    srefine (T _ a).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Funext
P: HProp
f: P -> Type
a: A (forall h : P, f h)
h: P
(forall h : P, f h) <~> f h
    apply (@equiv_contr_forall _ _ (contr_inhabited_hprop _ _)).
  Defined.

  (** And this one is homotopic to [alg_flab_map] when [Type] is given its "sigma" flabbiness structure. *)
  Definition alg_flab_map_sigma
    (P : HProp) (f : P -> Type)
    : A {h : P & f h} -> (forall h, A (f h)).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
P: HProp
f: P -> Type
A {h : P & f h} -> forall h : P, A (f h)
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
P: HProp
f: P -> Type
A {h : P & f h} -> forall h : P, A (f h)
    intros a h.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
P: HProp
f: P -> Type
a: A {h : P & f h}
h: P
A (f h)
    srefine (T _ a).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
P: HProp
f: P -> Type
a: A {h : P & f h}
h: P
{h : P & f h} <~> f h
    apply (@equiv_contr_sigma _ _ (contr_inhabited_hprop _ _)).
  Defined.

  (** The following conditions can be thought of as closure conditions under pi or sigma types for the type family [A]. *)
  Definition alg_flab_sigma_condition_forall `{Funext}
    := forall P f, {s : _ & alg_flab_map_forall P f o s == idmap}.

  Definition alg_flab_sigma_condition_sigma
    := forall P f, {s : _ & alg_flab_map_sigma P f o s == idmap}.

  Definition homotopic_alg_flab_map_alg_flab_map_forall `{Univalence}
    (P : HProp) (f : P -> Type)
    : alg_flab_map_forall P f == alg_flab_map A alg_flab_Type_forall P f.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
alg_flab_map_forall P f ==
alg_flab_map A alg_flab_Type_forall P f
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
alg_flab_map_forall P f ==
alg_flab_map A alg_flab_Type_forall P f
    intros a.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
a: A (forall h : P, f h)
alg_flab_map_forall P f a =
alg_flab_map A alg_flab_Type_forall P f a funext h.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
a: A (forall h : P, f h)
h: P
alg_flab_map_forall P f a h =
alg_flab_map A alg_flab_Type_forall P f a h
    srefine (homotopic_trequiv A (@T) (@univalent_transport H A) Trefl _ _ a).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
a: A (forall h : P, f h)
h: P
forall X : Type, univalent_transport A 1 == idmap
    apply univalent_transport_idequiv.
  Defined.

  Definition homotopic_alg_flab_map_alg_flab_map_sigma `{Univalence}
    (P : HProp) (f : P -> Type)
    : alg_flab_map_sigma P f == alg_flab_map A alg_flab_Type_sigma P f.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
alg_flab_map_sigma P f ==
alg_flab_map A alg_flab_Type_sigma P f
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
alg_flab_map_sigma P f ==
alg_flab_map A alg_flab_Type_sigma P f
    intros s.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
s: A {h : P & f h}
alg_flab_map_sigma P f s =
alg_flab_map A alg_flab_Type_sigma P f s funext h.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
s: A {h : P & f h}
h: P
alg_flab_map_sigma P f s h =
alg_flab_map A alg_flab_Type_sigma P f s h
    srefine (homotopic_trequiv A (@T) (@univalent_transport H A) Trefl _ _ s).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
P: HProp
f: P -> Type
s: A {h : P & f h}
h: P
forall X : Type, univalent_transport A 1 == idmap
    apply univalent_transport_idequiv.
  Defined.

  (** The original [sigma_condition] is implied by our reformulated conditions [alg_flab_sigma_condition_forall] and [alg_flab_sigma_condition_sigma]. *)
  Definition sigma_condition_sigma_condition_forall `{Univalence}
    (condf : alg_flab_sigma_condition_forall)
    : alg_flab_sigma_condition A _.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
alg_flab_sigma_condition A alg_flab_Type_forall
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
alg_flab_sigma_condition A alg_flab_Type_forall
    intros P f.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
P: HProp
f: P -> Type
{s : (forall h : P, A (f h)) -> A (center_af f) &
(fun x : forall h : P, A (f h) =>
 alg_flab_map A alg_flab_Type_forall P f (s x)) ==
idmap}
    destruct (condf _ f) as [s J].
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A (forall h : P, f h)
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_forall P f (s x)) == idmap
{s : (forall h : P, A (f h)) -> A (center_af f) &
(fun x : forall h : P, A (f h) =>
 alg_flab_map A alg_flab_Type_forall P f (s x)) ==
idmap}
    exists s.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A (forall h : P, f h)
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_forall P f (s x)) == idmap
(fun x : forall h : P, A (f h) =>
 alg_flab_map A alg_flab_Type_forall P f (s x)) ==
idmap
    intro g.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A (forall h : P, f h)
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_forall P f (s x)) == idmap
g: forall h : P, A (f h)
alg_flab_map A alg_flab_Type_forall P f (s g) = g
    lhs_V napply (homotopic_alg_flab_map_alg_flab_map_forall P f (s g)).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A (forall h : P, f h)
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_forall P f (s x)) == idmap
g: forall h : P, A (f h)
alg_flab_map_forall P f (s g) = g
    apply J.
  Defined.

  Definition alg_flab_sigma_forall `{Univalence} (condf : alg_flab_sigma_condition_forall)
    : IsAlgebraicFlabbyType {X : Type & A X}.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
IsAlgebraicFlabbyType {X : Type & A X}
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
IsAlgebraicFlabbyType {X : Type & A X}
    napply alg_flab_sigma.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_forall
alg_flab_sigma_condition A ?Goal
    exact (sigma_condition_sigma_condition_forall condf).
  Defined.

  Definition sigma_condition_sigma_condition_sigma `{Univalence}
    (condf : alg_flab_sigma_condition_sigma)
    : alg_flab_sigma_condition A alg_flab_Type_sigma.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_sigma
alg_flab_sigma_condition A alg_flab_Type_sigma
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_sigma
alg_flab_sigma_condition A alg_flab_Type_sigma
    intros P f.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_sigma
P: HProp
f: P -> Type
{s : (forall h : P, A (f h)) -> A (center_af f) &
(fun x : forall h : P, A (f h) =>
 alg_flab_map A alg_flab_Type_sigma P f (s x)) ==
idmap}
    destruct (condf _ f) as [s J].
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_sigma
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A {h : P & f h}
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_sigma P f (s x)) == idmap
{s : (forall h : P, A (f h)) -> A (center_af f) &
(fun x : forall h : P, A (f h) =>
 alg_flab_map A alg_flab_Type_sigma P f (s x)) ==
idmap}
    exists s.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_sigma
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A {h : P & f h}
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_sigma P f (s x)) == idmap
(fun x : forall h : P, A (f h) =>
 alg_flab_map A alg_flab_Type_sigma P f (s x)) ==
idmap
    intro g.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_sigma
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A {h : P & f h}
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_sigma P f (s x)) == idmap
g: forall h : P, A (f h)
alg_flab_map A alg_flab_Type_sigma P f (s g) = g
    lhs_V napply (homotopic_alg_flab_map_alg_flab_map_sigma P f (s g)).
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
condf: alg_flab_sigma_condition_sigma
P: HProp
f: P -> Type
s: (forall h : P, A (f h)) -> A {h : P & f h}
J: (fun x : forall h : P, A (f h) =>
 alg_flab_map_sigma P f (s x)) == idmap
g: forall h : P, A (f h)
alg_flab_map_sigma P f (s g) = g
    apply J.
  Defined.

  Definition alg_flab_sigma_sigma `{Univalence} (conds : alg_flab_sigma_condition_sigma)
    : IsAlgebraicFlabbyType {X : Type & A X}.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
conds: alg_flab_sigma_condition_sigma
IsAlgebraicFlabbyType {X : Type & A X}
  Proof.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
conds: alg_flab_sigma_condition_sigma
IsAlgebraicFlabbyType {X : Type & A X}
    napply alg_flab_sigma.
A: Type -> Type
T: forall X Y : Type, X <~> Y -> A X -> A Y
Trefl: forall X : Type, T 1 == idmap
H: Univalence
conds: alg_flab_sigma_condition_sigma
alg_flab_sigma_condition A ?Goal
    exact (sigma_condition_sigma_condition_sigma conds).
  Defined.

End AlgFlabUniverse.

(** The type of pointed types is algebraically flabby. *)
Definition alg_flab_pType `{Univalence}
  : IsAlgebraicFlabbyType {X : Type & X}.
H: Univalence
IsAlgebraicFlabbyType {X : Type & X}
Proof.
H: Univalence
IsAlgebraicFlabbyType {X : Type & X}
  rapply (alg_flab_sigma_forall _ (@equiv_fun)).
H: Univalence
forall X : Type, 1%equiv == idmap
H: Univalence
alg_flab_sigma_condition_forall idmap (@equiv_fun)
  -
H: Univalence
forall X : Type, 1%equiv == idmap reflexivity.
  -
H: Univalence
alg_flab_sigma_condition_forall idmap (@equiv_fun) intros P f.
H: Univalence
P: HProp
f: P -> Type
{s : (forall h : P, f h) -> forall h : P, f h &
(fun x : forall h : P, f h =>
 alg_flab_map_forall idmap (@equiv_fun) P f (s x)) ==
idmap}
    exists idmap.
H: Univalence
P: HProp
f: P -> Type
(fun x : forall h : P, f h =>
 alg_flab_map_forall idmap (@equiv_fun) P f x) ==
idmap
    reflexivity.
Defined.

(** The following results are adapted from section 7 of Injective Types in Univalent Mathematics by Martín Escardó, using the above results. *)

(** For a subuniverse, the flabbiness condition is equivalent to closure under proposition indexed pi types (or sigma types), so using this we can state a simpler theorem for proving flabbiness of subuniverses. *)
Definition alg_flab_subuniverse_forall `{Univalence} (O : Subuniverse)
  (condForall : forall (P : HProp) A, (forall h : P, In O (A h)) -> In O (forall h : P, A h))
  : IsAlgebraicFlabbyType@{u su} (Type_ O).
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
IsAlgebraicFlabbyType (Type_ O)
Proof.
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
IsAlgebraicFlabbyType (Type_ O)
  rapply (alg_flab_sigma_forall _ (fun X Y f H => @inO_equiv_inO' O X Y H f)).
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
forall X : Type,
(fun H : In O X => inO_equiv_inO' X 1) == idmap
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
alg_flab_sigma_condition_forall 
  (In O)
  (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
   inO_equiv_inO' X f)
  -
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
forall X : Type,
(fun H : In O X => inO_equiv_inO' X 1) == idmap intros X A.
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
X: Type
A: In O X
inO_equiv_inO' X 1 = A apply path_ishprop.
  -
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
alg_flab_sigma_condition_forall 
  (In O)
  (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
   inO_equiv_inO' X f) intros P A.
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
P: HProp
A: P -> Type
{s
: (forall h : P, In O (A h)) ->
  In O (forall h : P, A h) &
(fun x : forall h : P, In O (A h) =>
 alg_flab_map_forall (In O)
   (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
    inO_equiv_inO' X f) P A 
   (s x)) == idmap}
    exists _.
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
P: HProp
A: P -> Type
(fun x : forall h : P, In O (A h) =>
 alg_flab_map_forall (In O)
   (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
    inO_equiv_inO' X f) P A 
   (condForall P A x)) == idmap
    intros s.
H: Univalence
O: Subuniverse
condForall: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O (forall h : P, A h)
P: HProp
A: P -> Type
s: forall h : P, In O (A h)
alg_flab_map_forall (In O)
  (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
   inO_equiv_inO' X f) P A 
  (condForall P A s) = s apply path_ishprop.
Defined.

Definition alg_flab_subuniverse_sigma `{Univalence} (O : Subuniverse)
  (condSigma : forall (P : HProp) A, (forall h : P, In O (A h)) -> In O {h : P & A h})
  : IsAlgebraicFlabbyType@{u su} (Type_ O).
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
IsAlgebraicFlabbyType (Type_ O)
Proof.
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
IsAlgebraicFlabbyType (Type_ O)
  rapply (alg_flab_sigma_sigma _ (fun X Y f H => @inO_equiv_inO' O X Y H f)).
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
forall X : Type,
(fun H : In O X => inO_equiv_inO' X 1) == idmap
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
alg_flab_sigma_condition_sigma 
  (In O)
  (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
   inO_equiv_inO' X f)
  -
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
forall X : Type,
(fun H : In O X => inO_equiv_inO' X 1) == idmap intros X A.
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
X: Type
A: In O X
inO_equiv_inO' X 1 = A apply path_ishprop.
  -
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
alg_flab_sigma_condition_sigma 
  (In O)
  (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
   inO_equiv_inO' X f) intros P A.
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
P: HProp
A: P -> Type
{s : (forall h : P, In O (A h)) -> In O {h : P & A h}
&
(fun x : forall h : P, In O (A h) =>
 alg_flab_map_sigma (In O)
   (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
    inO_equiv_inO' X f) P A 
   (s x)) == idmap}
    exists _.
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
P: HProp
A: P -> Type
(fun x : forall h : P, In O (A h) =>
 alg_flab_map_sigma (In O)
   (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
    inO_equiv_inO' X f) P A 
   (condSigma P A x)) == idmap
    intros s.
H: Univalence
O: Subuniverse
condSigma: forall (P : HProp) (A : P -> Type),
(forall h : P, In O (A h)) ->
In O {h : P & A h}
P: HProp
A: P -> Type
s: forall h : P, In O (A h)
alg_flab_map_sigma (In O)
  (fun (X Y : Type) (f : X <~> Y) (H : In O X) =>
   inO_equiv_inO' X f) P A 
  (condSigma P A s) = s apply path_ishprop.
Defined.

(** As an immediate corollary, we get that reflective subuniverses are algebraically flabby. *)
Definition alg_flab_reflective_subuniverse `{Univalence} (O : ReflectiveSubuniverse)
  : IsAlgebraicFlabbyType@{u su} (Type_ O)
  := alg_flab_subuniverse_forall _ _.