(* -*- mode: coq; mode: visual-line -*-  *)
Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.

(** * H-Sets *)

Local Open Scope path_scope.

(** A type is a set if and only if it satisfies Axiom K. *)

Definition axiomK A := forall (x : A) (p : x = x), p = idpath x.

Definition axiomK_hset {A} : IsHSet A -> axiomK A.
A: Type
IsHSet A -> axiomK A
Proof.
A: Type
IsHSet A -> axiomK A
  intros H x p.
A: Type
H: IsHSet A
x: A
p: x = x
p = 1
  nrapply path_ishprop.
A: Type
H: IsHSet A
x: A
p: x = x
IsHProp (x = x)
  exact (H x x).
Defined.

Definition hset_axiomK {A} `{axiomK A} : IsHSet A.
A: Type
axiomK0: axiomK A
IsHSet A
Proof.
A: Type
axiomK0: axiomK A
IsHSet A
  apply istrunc_S; intros x y.
A: Type
axiomK0: axiomK A
x, y: A
IsHProp (x = y)
  apply @hprop_allpath.
A: Type
axiomK0: axiomK A
x, y: A
forall x0 y0 : x = y, x0 = y0
  intros p q.
A: Type
axiomK0: axiomK A
x, y: A
p, q: x = y
p = q
  by induction p.
Defined.

Section AssumeFunext.
Context `{Funext}.

Theorem equiv_hset_axiomK {A} : IsHSet A <~> axiomK A.
H: Funext
A: Type
IsHSet A <~> axiomK A
Proof.
H: Funext
A: Type
IsHSet A <~> axiomK A
  apply (equiv_adjointify (@axiomK_hset A) (@hset_axiomK A)).
H: Funext
A: Type
(fun x : axiomK A => axiomK_hset hset_axiomK) == idmap
H: Funext
A: Type
(fun x : IsHSet A => hset_axiomK) == idmap
  -
H: Funext
A: Type
(fun x : axiomK A => axiomK_hset hset_axiomK) == idmap intros K.
H: Funext
A: Type
K: axiomK A
axiomK_hset hset_axiomK = K by_extensionality x.
H: Funext
A: Type
K: axiomK A
x: A
axiomK_hset hset_axiomK x = K x by_extensionality x'.
H: Funext
A: Type
K: axiomK A
x: A
x': x = x
axiomK_hset hset_axiomK x x' = K x x'
    cut (Contr (x=x)).
H: Funext
A: Type
K: axiomK A
x: A
x': x = x
Contr (x = x) -> axiomK_hset hset_axiomK x x' = K x x'
H: Funext
A: Type
K: axiomK A
x: A
x': x = x
Contr (x = x)
    +
H: Funext
A: Type
K: axiomK A
x: A
x': x = x
Contr (x = x) -> axiomK_hset hset_axiomK x x' = K x x' intro.
H: Funext
A: Type
K: axiomK A
x: A
x': x = x
X: Contr (x = x)
axiomK_hset hset_axiomK x x' = K x x' eapply path_contr.
    +
H: Funext
A: Type
K: axiomK A
x: A
x': x = x
Contr (x = x) apply (Build_Contr _ 1).
H: Funext
A: Type
K: axiomK A
x: A
x': x = x
forall y : x = x, 1 = y intros.
H: Funext
A: Type
K: axiomK A
x: A
x', y: x = x
1 = y symmetry; apply K.
  -
H: Funext
A: Type
(fun x : IsHSet A => hset_axiomK) == idmap intro K.
H: Funext
A: Type
K: IsHSet A
hset_axiomK = K
    eapply path_ishprop.
Defined.

Global Instance axiomK_isprop A : IsHProp (axiomK A) | 0.
H: Funext
A: Type
IsHProp (axiomK A)
Proof.
H: Funext
A: Type
IsHProp (axiomK A)
  apply (istrunc_equiv_istrunc _ equiv_hset_axiomK).
Defined.

Theorem hset_path2 {A} `{IsHSet A} {x y : A} (p q : x = y):
  p = q.
H: Funext
A: Type
IsHSet0: IsHSet A
x, y: A
p, q: x = y
p = q
Proof.
H: Funext
A: Type
IsHSet0: IsHSet A
x, y: A
p, q: x = y
p = q
  induction q.
H: Funext
A: Type
IsHSet0: IsHSet A
x: A
p: x = x
p = 1
  apply axiomK_hset; assumption.
Defined.

(** Recall that axiom K says that any self-path is homotopic to the
   identity path.  In particular, the identity path is homotopic to
   itself.  The following lemma says that the endo-homotopy of the
   identity path thus specified is in fact (homotopic to) its identity
   homotopy (whew!).  *)
(* TODO: What was the purpose of this lemma?  Do we need it at all?  It's actually fairly trivial. *)
Lemma axiomK_idpath {A} (x : A) (K : axiomK A) :
  K x (idpath x) = idpath (idpath x).
H: Funext
A: Type
x: A
K: axiomK A
K x 1 = 1
Proof.
H: Funext
A: Type
x: A
K: axiomK A
K x 1 = 1
  pose (T1A := @istrunc_succ _ A (@hset_axiomK A K)).
H: Funext
A: Type
x: A
K: axiomK A
T1A:= istrunc_succ: IsTrunc 1 A
K x 1 = 1
  exact (@hset_path2 (x=x) (T1A x x) _ _ _ _).
Defined.

End AssumeFunext.

(** We prove that if [R] is a reflexive mere relation on [X] implying identity, then [X] is an hSet, and hence [R x y] is equivalent to [x = y]. *)
Lemma ishset_hrel_subpaths
      {X R}
      `{Reflexive X R}
      `{forall x y, IsHProp (R x y)}
      (f : forall x y, R x y -> x = y)
: IsHSet X.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
IsHSet X
Proof.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
IsHSet X
  apply @hset_axiomK.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
axiomK X
  intros x p.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x: X
p: x = x
p = 1
  refine (_ @ concat_Vp (f x x (transport (R x) p^ (reflexivity _)))).
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x: X
p: x = x
p =
(f x x (transport (R x) p^ (reflexivity x)))^ @
f x x (transport (R x) p^ (reflexivity x))
  apply moveL_Vp.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x: X
p: x = x
f x x (transport (R x) p^ (reflexivity x)) @ p =
f x x (transport (R x) p^ (reflexivity x))
  refine ((transport_paths_r _ _)^ @ _).
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x: X
p: x = x
transport (fun y : X => x = y) p
  (f x x (transport (R x) p^ (reflexivity x))) =
f x x (transport (R x) p^ (reflexivity x))
  refine ((transport_arrow _ _ _)^ @ _).
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x: X
p: x = x
transport (fun x0 : X => R x x0 -> x = x0) p (f x x)
  (reflexivity x) =
f x x (transport (R x) p^ (reflexivity x))
  refine ((ap10 (apD (f x) p) (@reflexivity X R _ x)) @ _).
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x: X
p: x = x
f x x (reflexivity x) =
f x x (transport (R x) p^ (reflexivity x))
  apply ap.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x: X
p: x = x
reflexivity x = transport (R x) p^ (reflexivity x)
  apply path_ishprop.
Defined.

Global Instance isequiv_hrel_subpaths
       X R
       `{Reflexive X R}
       `{forall x y, IsHProp (R x y)}
       (f : forall x y, R x y -> x = y)
       x y
: IsEquiv (f x y) | 10000.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x, y: X
IsEquiv (f x y)
Proof.
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x, y: X
IsEquiv (f x y)
  pose proof (ishset_hrel_subpaths f).
X: Type
R: Relation X
H: Reflexive R
H0: is_mere_relation X R
f: forall x y : X, R x y -> x = y
x, y: X
X0: IsHSet X
IsEquiv (f x y)
  refine (isequiv_adjointify
            (f x y)
            (fun p => transport (R x) p (reflexivity x))
            _
            _);
  intro;
  apply path_ishprop.
Defined.

(** We will now prove that for sets, monos and injections are equivalent.*)
Definition ismono {X Y} (f : X -> Y)
  := forall (Z : HSet),
     forall g h : Z -> X, f o g = f o h -> g = h.

Definition isinj {X Y} (f : X -> Y)
  := forall x0 x1 : X,
       f x0 = f x1 -> x0 = x1.

Lemma isinj_embedding {A B : Type} (m : A -> B) : IsEmbedding m -> isinj m.
A, B: Type
m: A -> B
IsEmbedding m -> isinj m
Proof.
A, B: Type
m: A -> B
IsEmbedding m -> isinj m
  intros ise x y p.
A, B: Type
m: A -> B
ise: IsEmbedding m
x, y: A
p: m x = m y
x = y
  pose (ise (m y)).
A, B: Type
m: A -> B
ise: IsEmbedding m
x, y: A
p: m x = m y
i:= ise (m y): IsHProp (hfiber m (m y))
x = y
  assert (q : (x;p) = (y;1) :> hfiber m (m y)) by apply path_ishprop.
A, B: Type
m: A -> B
ise: IsEmbedding m
x, y: A
p: m x = m y
i:= ise (m y): IsHProp (hfiber m (m y))
q: (x; p) = (y; 1)
x = y
  exact (ap pr1 q).
Defined.

(** Computation rule for isinj_embedding. *)
Lemma isinj_embedding_beta {X Y : Type} (f : X -> Y) {I : IsEmbedding f} {x : X}
  : (isinj_embedding f I x x idpath) = idpath.
X, Y: Type
f: X -> Y
I: IsEmbedding f
x: X
isinj_embedding f I x x 1 = 1
Proof.
X, Y: Type
f: X -> Y
I: IsEmbedding f
x: X
isinj_embedding f I x x 1 = 1
  exact (ap (ap pr1) (contr (idpath : (x;idpath) = (x;idpath)))).
Defined.

Definition isinj_section {A B : Type} {s : A -> B} {r : B -> A}
      (H : r o s == idmap) : isinj s.
A, B: Type
s: A -> B
r: B -> A
H: r o s == idmap
isinj s
Proof.
A, B: Type
s: A -> B
r: B -> A
H: r o s == idmap
isinj s
  intros a a' alpha.
A, B: Type
s: A -> B
r: B -> A
H: r o s == idmap
a, a': A
alpha: s a = s a'
a = a'
  exact ((H a)^ @ ap r alpha @ H a').
Defined.

Lemma isembedding_isinj_hset {A B : Type} `{IsHSet B} (m : A -> B)
: isinj m -> IsEmbedding m.
A, B: Type
IsHSet0: IsHSet B
m: A -> B
isinj m -> IsEmbedding m
Proof.
A, B: Type
IsHSet0: IsHSet B
m: A -> B
isinj m -> IsEmbedding m
  intros isi b.
A, B: Type
IsHSet0: IsHSet B
m: A -> B
isi: isinj m
b: B
IsHProp (hfiber m b)
  apply hprop_allpath; intros [x p] [y q].
A, B: Type
IsHSet0: IsHSet B
m: A -> B
isi: isinj m
b: B
x: A
p: m x = b
y: A
q: m y = b
(x; p) = (y; q)
  apply path_sigma_hprop; simpl.
A, B: Type
IsHSet0: IsHSet B
m: A -> B
isi: isinj m
b: B
x: A
p: m x = b
y: A
q: m y = b
x = y
  exact (isi x y (p @ q^)).
Defined.

Lemma ismono_isinj `{Funext} {X Y} (f : X -> Y) : isinj f -> ismono f.
H: Funext
X, Y: Type
f: X -> Y
isinj f -> ismono f
Proof.
H: Funext
X, Y: Type
f: X -> Y
isinj f -> ismono f
  intros ? ? ? ? H'.
H: Funext
X, Y: Type
f: X -> Y
X0: isinj f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) = (fun x : Z => f (h x))
g = h
  apply path_forall.
H: Funext
X, Y: Type
f: X -> Y
X0: isinj f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) = (fun x : Z => f (h x))
g == h
  apply ap10 in H'.
H: Funext
X, Y: Type
f: X -> Y
X0: isinj f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
g == h
  hnf in *.
H: Funext
X, Y: Type
f: X -> Y
X0: forall x0 x1 : X, f x0 = f x1 -> x0 = x1
Z: HSet
g, h: Z -> X
H': forall x : Z, f (g x) = f (h x)
forall x : Z, g x = h x
  eauto.
Qed.

Definition isinj_ismono {X Y} (f : X -> Y)
           (H : ismono f)
: isinj f
  := fun x0 x1 H' =>
       ap10 (H (Build_HSet Unit)
               (fun _ => x0)
               (fun _ => x1)
               (ap (fun x => unit_name x) H'))
            tt.

Lemma ismono_isequiv `{Funext} X Y (f : X -> Y) `{IsEquiv _ _ f}
: ismono f.
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
ismono f
Proof.
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
ismono f
  intros ? g h H'.
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) = (fun x : Z => f (h x))
g = h
  apply ap10 in H'.
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
g = h
  apply path_forall.
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
g == h
  intro x.
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
g x = h x
  transitivity (f^-1 (f (g x))).
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
g x = f^-1 (f (g x))
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
f^-1 (f (g x)) = h x
  -
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
g x = f^-1 (f (g x)) by rewrite eissect.
  -
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
f^-1 (f (g x)) = h x transitivity (f^-1 (f (h x))).
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
f^-1 (f (g x)) = f^-1 (f (h x))
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
f^-1 (f (h x)) = h x
    *
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
f^-1 (f (g x)) = f^-1 (f (h x)) apply ap.
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
f (g x) = f (h x) apply H'.
    *
H: Funext
X, Y: Type
f: X -> Y
H0: IsEquiv f
Z: HSet
g, h: Z -> X
H': (fun x : Z => f (g x)) == (fun x : Z => f (h x))
x: Z
f^-1 (f (h x)) = h x by rewrite eissect.
Qed.

Lemma cancelL_isinjective {A B C : Type} {f : A -> B} {g : B -> C} `{I : isinj (g o f)}
  : isinj f.
A, B, C: Type
f: A -> B
g: B -> C
I: isinj (g o f)
isinj f
Proof.
A, B, C: Type
f: A -> B
g: B -> C
I: isinj (g o f)
isinj f
  intros a0 a1 p.
A, B, C: Type
f: A -> B
g: B -> C
I: isinj (g o f)
a0, a1: A
p: f a0 = f a1
a0 = a1
  apply I.
A, B, C: Type
f: A -> B
g: B -> C
I: isinj (g o f)
a0, a1: A
p: f a0 = f a1
g (f a0) = g (f a1)
  exact (ap g p).
Defined.

Lemma cancelL_isembedding {A B C : Type} `{IsHSet B} {f : A -> B} {g : B -> C} `{IsEmbedding (g o f)}
  : IsEmbedding f.
A, B, C: Type
IsHSet0: IsHSet B
f: A -> B
g: B -> C
IsEmbedding0: IsEmbedding (g o f)
IsEmbedding f
Proof.
A, B, C: Type
IsHSet0: IsHSet B
f: A -> B
g: B -> C
IsEmbedding0: IsEmbedding (g o f)
IsEmbedding f
  apply isembedding_isinj_hset.
A, B, C: Type
IsHSet0: IsHSet B
f: A -> B
g: B -> C
IsEmbedding0: IsEmbedding (g o f)
isinj f
  rapply (cancelL_isinjective (g:=g)).
A, B, C: Type
IsHSet0: IsHSet B
f: A -> B
g: B -> C
IsEmbedding0: IsEmbedding (g o f)
isinj (fun x : A => g (f x))
  rapply isinj_embedding.
Defined.