(* -*- mode: coq; mode: visual-line -*- *)

Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope nat_scope.
Local Open Scope path_scope.

Generalizable Variables A B f.

Section AssumeFunext.
Context `{Funext}.

(** * n-Path-split maps.

A map is n-path-split if its induced maps on the first n iterated path-spaces are split surjections.  Thus every map is 0-path-split, the 1-path-split maps are the split surjections, and so on.  It turns out that for n>1, being n-path-split is the same as being an equivalence. *)

Fixpoint PathSplit (n : nat) `(f : A -> B) : Type
  := match n with
       | 0 => Unit
       | S n => (forall a, hfiber f a) *
                forall (x y : A), PathSplit n (@ap _ _ f x y)
     end.

Definition isequiv_pathsplit (n : nat) `{f : A -> B}
: PathSplit n.+2 f -> IsEquiv f.
H: Funext
n: nat
A, B: Type
f: A -> B
PathSplit n.+2 f -> IsEquiv f
Proof.
H: Funext
n: nat
A, B: Type
f: A -> B
PathSplit n.+2 f -> IsEquiv f
  intros [g k].
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
k: forall x y : A, PathSplit n.+1 (ap f)
IsEquiv f
  pose (h := fun x y p => (fst (k x y) p).1).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
k: forall x y : A, PathSplit n.+1 (ap f)
h:= fun (x y : A) (p : f x = f y) => (fst (k x y) p).1: forall x y : A, f x = f y -> x = y
IsEquiv f
  pose (hs := fun x y => (fun p => (fst (k x y) p).2)
                         : (ap f) o (h x y) == idmap).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
k: forall x y : A, PathSplit n.+1 (ap f)
h:= fun (x y : A) (p : f x = f y) => (fst (k x y) p).1: forall x y : A, f x = f y -> x = y
hs:= fun x y : A =>
(fun p : f x = f y => (fst (k x y) p).2)
:
ap f o h x y == idmap: forall x y : A, ap f o h x y == idmap
IsEquiv f
  clearbody hs; clearbody h; clear k.
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
IsEquiv f
  apply isequiv_contr_map; intros b.
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
Contr (hfiber f b)
  apply contr_inhabited_hprop.
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
IsHProp (hfiber f b)
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
hfiber f b
  2:exact (g b).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
IsHProp (hfiber f b)
  apply hprop_allpath; intros [a p] [a' p'].
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
a: A
p: f a = b
a': A
p': f a' = b
(a; p) = (a'; p')
  refine (path_sigma' _ (h a a' (p @ p'^)) _).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
a: A
p: f a = b
a': A
p': f a' = b
transport (fun x : A => f x = b) (h a a' (p @ p'^)) p =
p'
  refine (transport_paths_Fl _ _ @ _).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
a: A
p: f a = b
a': A
p': f a' = b
(ap f (h a a' (p @ p'^)))^ @ p = p'
  refine ((inverse2 (hs a a' (p @ p'^)) @@ 1) @ _).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
a: A
p: f a = b
a': A
p': f a' = b
(p @ p'^)^ @ p = p'
  refine ((inv_pp p p'^ @@ 1) @ _).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
a: A
p: f a = b
a': A
p': f a' = b
((p'^)^ @ p^) @ p = p'
  refine (concat_pp_p _ _ _ @ _).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
a: A
p: f a = b
a': A
p': f a' = b
(p'^)^ @ (p^ @ p) = p'
  refine ((1 @@ concat_Vp _) @ _).
H: Funext
n: nat
A, B: Type
f: A -> B
g: forall a : B, hfiber f a
h: forall x y : A, f x = f y -> x = y
hs: forall x y : A, ap f o h x y == idmap
b: B
a: A
p: f a = b
a': A
p': f a' = b
(p'^)^ @ 1 = p'
  exact ((inv_V p' @@ 1) @ concat_p1 _).
Defined.

Global Instance contr_pathsplit_isequiv
           (n : nat) `(f : A -> B) `{IsEquiv _ _ f}
: Contr (PathSplit n f).
H: Funext
n: nat
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (PathSplit n f)
Proof.
H: Funext
n: nat
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (PathSplit n f)
  generalize dependent B; revert A.
H: Funext
n: nat
forall (A B : Type) (f : A -> B),
IsEquiv f -> Contr (PathSplit n f)
  simple_induction n n IHn; intros A B f ?.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (PathSplit 0 f)
H: Funext
n: nat
IHn: forall (A B : Type) (f : A -> B), IsEquiv f -> Contr (PathSplit n f)
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (PathSplit n.+1 f)
  -
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (PathSplit 0 f) exact _.
  -
H: Funext
n: nat
IHn: forall (A B : Type) (f : A -> B), IsEquiv f -> Contr (PathSplit n f)
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (PathSplit n.+1 f) apply contr_prod.
Defined.

Global Instance ishprop_pathsplit (n : nat) `(f : A -> B)
: IsHProp (PathSplit n.+2 f).
H: Funext
n: nat
A, B: Type
f: A -> B
IsHProp (PathSplit n.+2 f)
Proof.
H: Funext
n: nat
A, B: Type
f: A -> B
IsHProp (PathSplit n.+2 f)
  apply hprop_inhabited_contr; intros ps.
H: Funext
n: nat
A, B: Type
f: A -> B
ps: PathSplit n.+2 f
Contr (PathSplit n.+2 f)
  pose (isequiv_pathsplit n ps).
H: Funext
n: nat
A, B: Type
f: A -> B
ps: PathSplit n.+2 f
i:= isequiv_pathsplit n ps: IsEquiv f
Contr (PathSplit n.+2 f)
  exact _.
Defined.

Definition equiv_pathsplit_isequiv (n : nat) `(f : A -> B)
: PathSplit n.+2 f <~> IsEquiv f.
H: Funext
n: nat
A, B: Type
f: A -> B
PathSplit n.+2 f <~> IsEquiv f
Proof.
H: Funext
n: nat
A, B: Type
f: A -> B
PathSplit n.+2 f <~> IsEquiv f
  refine (equiv_iff_hprop _ _).
H: Funext
n: nat
A, B: Type
f: A -> B
PathSplit n.+2 f -> IsEquiv f
H: Funext
n: nat
A, B: Type
f: A -> B
IsEquiv f -> PathSplit n.+2 f
  -
H: Funext
n: nat
A, B: Type
f: A -> B
PathSplit n.+2 f -> IsEquiv f apply isequiv_pathsplit.
  -
H: Funext
n: nat
A, B: Type
f: A -> B
IsEquiv f -> PathSplit n.+2 f intros ?; refine (center _).
Defined.

(** Path-splitness transfers across commutative squares of equivalences. *)
Lemma equiv_functor_pathsplit (n : nat) {A B C D}
      (f : A -> B) (g : C -> D) (h : A <~> C) (k : B <~> D)
      (p : g o h == k o f)
: PathSplit n f <~> PathSplit n g.
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit n f <~> PathSplit n g
Proof.
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit n f <~> PathSplit n g
  destruct n as [|n].
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit 0 f <~> PathSplit 0 g
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit n.+1 f <~> PathSplit n.+1 g
  1:apply equiv_idmap.
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit n.+1 f <~> PathSplit n.+1 g
  destruct n as [|n].
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit 1 f <~> PathSplit 1 g
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit n.+2 f <~> PathSplit n.+2 g
  -
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit 1 f <~> PathSplit 1 g simpl.
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
(forall a : B, hfiber f a) * (A -> A -> Unit) <~>
(forall a : D, hfiber g a) * (C -> C -> Unit)
    refine (_ *E equiv_contr_contr).
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
(forall a : B, hfiber f a) <~>
(forall a : D, hfiber g a)
    refine (equiv_functor_forall' k^-1 _); intros d.
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
d: D
hfiber f ((k^-1)%equiv d) <~> hfiber g d
    unfold hfiber.
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
d: D
{x : A & f x = (k^-1)%equiv d} <~> {x : C & g x = d}
    refine (equiv_functor_sigma' h _); intros a.
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
d: D
a: A
f a = (k^-1)%equiv d <~> g (h a) = d
    refine (equiv_concat_l (p a) d oE _).
H: Funext
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
d: D
a: A
f a = (k^-1)%equiv d <~> k (f a) = d
    simpl; apply equiv_moveR_equiv_M.
  -
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
PathSplit n.+2 f <~> PathSplit n.+2 g refine (_ oE equiv_pathsplit_isequiv n f).
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
IsEquiv f <~> PathSplit n.+2 g
    refine ((equiv_pathsplit_isequiv n g)^-1 oE _).
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
IsEquiv f <~> IsEquiv g
    apply equiv_iff_hprop; intros e.
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
e: IsEquiv f
IsEquiv g
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
e: IsEquiv g
IsEquiv f
    +
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
e: IsEquiv f
IsEquiv g refine (isequiv_commsq f g h k (fun a => (p a)^)).
    +
H: Funext
n: nat
A, B, C, D: Type
f: A -> B
g: C -> D
h: A <~> C
k: B <~> D
p: g o h == k o f
e: IsEquiv g
IsEquiv f refine (isequiv_commsq' f g h k p).
Defined.

(** A map is oo-path-split if it is n-path-split for all n.  This is also equivalent to being an equivalence. *)

Definition ooPathSplit `(f : A -> B) : Type
  := forall n, PathSplit n f.

Definition isequiv_oopathsplit `{f : A -> B}
: ooPathSplit f -> IsEquiv f
  := fun ps => isequiv_pathsplit 0 (ps 2).

Global Instance contr_oopathsplit_isequiv
           `(f : A -> B) `{IsEquiv _ _ f}
: Contr (ooPathSplit f).
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (ooPathSplit f)
Proof.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr (ooPathSplit f)
  apply contr_forall.
Defined.

Global Instance ishprop_oopathsplit `(f : A -> B)
: IsHProp (ooPathSplit f).
H: Funext
A, B: Type
f: A -> B
IsHProp (ooPathSplit f)
Proof.
H: Funext
A, B: Type
f: A -> B
IsHProp (ooPathSplit f)
  apply hprop_inhabited_contr; intros ps.
H: Funext
A, B: Type
f: A -> B
ps: ooPathSplit f
Contr (ooPathSplit f)
  pose (isequiv_oopathsplit ps).
H: Funext
A, B: Type
f: A -> B
ps: ooPathSplit f
i:= isequiv_oopathsplit ps: IsEquiv f
Contr (ooPathSplit f)
  exact _.
Defined.

Definition equiv_oopathsplit_isequiv `(f : A -> B)
: ooPathSplit f <~> IsEquiv f.
H: Funext
A, B: Type
f: A -> B
ooPathSplit f <~> IsEquiv f
Proof.
H: Funext
A, B: Type
f: A -> B
ooPathSplit f <~> IsEquiv f
  refine (equiv_iff_hprop _ _).
H: Funext
A, B: Type
f: A -> B
ooPathSplit f -> IsEquiv f
H: Funext
A, B: Type
f: A -> B
IsEquiv f -> ooPathSplit f
  -
H: Funext
A, B: Type
f: A -> B
ooPathSplit f -> IsEquiv f apply isequiv_oopathsplit.
  -
H: Funext
A, B: Type
f: A -> B
IsEquiv f -> ooPathSplit f intros ?; refine (center _).
Defined.

End AssumeFunext.