(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics Types Diagrams.CommutativeSquares HSet.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope equiv_scope.
Local Open Scope path_scope.

(** * Basic facts about fibrations *)

(* ** Homotopy fibers *)

(** Paths in homotopy fibers can be constructed using [path_sigma] and [transport_paths_Fl]. *)
Definition equiv_path_hfiber {A B : Type} {f : A -> B} {y : B}
  (x1 x2 : hfiber f y)
  : { q : x1.1 = x2.1 & x1.2 = ap f q @ x2.2 } <~> (x1 = x2).
A, B: Type
f: A -> B
y: B
x1, x2: hfiber f y
{q : x1.1 = x2.1 & x1.2 = ap f q @ x2.2} <~> x1 = x2
Proof.
A, B: Type
f: A -> B
y: B
x1, x2: hfiber f y
{q : x1.1 = x2.1 & x1.2 = ap f q @ x2.2} <~> x1 = x2
  refine (equiv_path_sigma _ _ _ oE _).
A, B: Type
f: A -> B
y: B
x1, x2: hfiber f y
{q : x1.1 = x2.1 & x1.2 = ap f q @ x2.2} <~>
{p : x1.1 = x2.1 &
transport (fun x : A => f x = y) p x1.2 = x2.2}
  apply equiv_functor_sigma_id.
A, B: Type
f: A -> B
y: B
x1, x2: hfiber f y
forall a : x1.1 = x2.1,
x1.2 = ap f a @ x2.2 <~>
transport (fun x : A => f x = y) a x1.2 = x2.2
  intros p; simpl.
A, B: Type
f: A -> B
y: B
x1, x2: hfiber f y
p: x1.1 = x2.1
x1.2 = ap f p @ x2.2 <~>
transport (fun x : A => f x = y) p x1.2 = x2.2
  refine (_ oE equiv_moveR_Vp _ _ _).
A, B: Type
f: A -> B
y: B
x1, x2: hfiber f y
p: x1.1 = x2.1
(ap f p)^ @ x1.2 = x2.2 <~>
transport (fun x : A => f x = y) p x1.2 = x2.2
  exact (equiv_concat_l (transport_paths_Fl _ _) _).
Defined.

Definition path_hfiber_uncurried {A B : Type} {f : A -> B} {y : B}
  {x1 x2 : hfiber f y}
  : { q : x1.1 = x2.1 & x1.2 = ap f q @ x2.2 } -> (x1 = x2)
  := equiv_path_hfiber x1 x2.

Definition path_hfiber {A B : Type} {f : A -> B} {y : B}
  {x1 x2 : hfiber f y} (q : x1.1 = x2.1) (r : x1.2 = ap f q @ x2.2)
  : x1 = x2
  := path_hfiber_uncurried (q;r).

(** If we rearrange this a bit, then it characterizes the fibers of [ap]. *)
Definition hfiber_ap {A B : Type} {f : A -> B} {x1 x2 : A}
           (p : f x1 = f x2)
  : hfiber (ap f) p <~> ((x1 ; p) = (x2 ; 1) :> hfiber f (f x2)).
A, B: Type
f: A -> B
x1, x2: A
p: f x1 = f x2
hfiber (ap f) p <~> (x1; p) = (x2; 1)
Proof.
A, B: Type
f: A -> B
x1, x2: A
p: f x1 = f x2
hfiber (ap f) p <~> (x1; p) = (x2; 1)
  refine (equiv_path_hfiber (x1;p) (x2;1%path) oE _).
A, B: Type
f: A -> B
x1, x2: A
p: f x1 = f x2
hfiber (ap f) p <~>
{q : (x1; p).1 = (x2; 1).1 &
(x1; p).2 = ap f q @ (x2; 1).2}
  unfold hfiber; simpl.
A, B: Type
f: A -> B
x1, x2: A
p: f x1 = f x2
{x : x1 = x2 & ap f x = p} <~>
{q : x1 = x2 & p = ap f q @ 1}
  apply equiv_functor_sigma_id; intros q.
A, B: Type
f: A -> B
x1, x2: A
p: f x1 = f x2
q: x1 = x2
ap f q = p <~> p = ap f q @ 1
  refine (_ oE equiv_path_inverse _ _).
A, B: Type
f: A -> B
x1, x2: A
p: f x1 = f x2
q: x1 = x2
p = ap f q <~> p = ap f q @ 1
  exact (equiv_concat_r (concat_p1 _)^ _).
Defined.

(** Homotopic maps have equivalent fibers. *)
Definition equiv_hfiber_homotopic
  {A B : Type} (f g : A -> B) (h : f == g) (b : B)
  : hfiber f b <~> hfiber g b.
A, B: Type
f, g: A -> B
h: f == g
b: B
hfiber f b <~> hfiber g b
Proof.
A, B: Type
f, g: A -> B
h: f == g
b: B
hfiber f b <~> hfiber g b
  refine (Build_Equiv _ _ (fun fx => (fx.1 ; (h fx.1)^ @ fx.2)) _).
A, B: Type
f, g: A -> B
h: f == g
b: B
IsEquiv
  (fun fx : {x : A & f x = b} =>
   (fx.1; (h fx.1)^ @ fx.2))
  refine (isequiv_adjointify _ (fun gx => (gx.1 ; (h gx.1) @ gx.2)) _ _);
    intros [a p]; simpl; apply ap.
A, B: Type
f, g: A -> B
h: f == g
b: B
a: A
p: g a = b
(h a)^ @ (h a @ p) = p
A, B: Type
f, g: A -> B
h: f == g
b: B
a: A
p: f a = b
h a @ ((h a)^ @ p) = p
  -
A, B: Type
f, g: A -> B
h: f == g
b: B
a: A
p: g a = b
(h a)^ @ (h a @ p) = p apply concat_V_pp.
  -
A, B: Type
f, g: A -> B
h: f == g
b: B
a: A
p: f a = b
h a @ ((h a)^ @ p) = p apply concat_p_Vp.
Defined.

(** Commutative squares induce maps between fibers. *)
Definition functor_hfiber {A B C D}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h) (b : B)
: hfiber f b -> hfiber g (k b).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
hfiber f b -> hfiber g (k b)
Proof.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
hfiber f b -> hfiber g (k b)
  snrapply @functor_sigma.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
A -> C
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
forall a : A,
(fun x : A => f x = b) a ->
(fun x : C => g x = k b) (?f a)
  -
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
A -> C exact h.
  -
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
forall a : A,
(fun x : A => f x = b) a ->
(fun x : C => g x = k b) (h a) intros a e; exact ((p a)^ @ ap k e).
Defined.

(** This doesn't need to be defined as an instance, since typeclass search can already find it, but we state it here for the reader's benefit. *)
Definition isequiv_functor_hfiber {A B C D}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           `{IsEquiv A C h} `{IsEquiv B D k}
           (p : k o f == g o h) (b : B)
: IsEquiv (functor_hfiber p b) := _.

Definition equiv_functor_hfiber {A B C D}
           {f : A -> B} {g : C -> D} {h : A <~> C} {k : B <~> D}
           (p : k o f == g o h) (b : B)
  : hfiber f b <~> hfiber g (k b)
  := Build_Equiv _ _ (functor_hfiber p b) _.

(** A version of functor_hfiber which is functorial in both the function and the point *)
Definition functor_hfiber2 {A B C D}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h) {b : B} {b' : D} (q : k b = b')
  : hfiber f b -> hfiber g b'.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
b': D
q: k b = b'
hfiber f b -> hfiber g b'
Proof.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
b': D
q: k b = b'
hfiber f b -> hfiber g b'
  srapply functor_sigma.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
b': D
q: k b = b'
A -> C
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
b': D
q: k b = b'
forall a : A,
(fun x : A => f x = b) a ->
(fun x : C => g x = b') (?f a)
  -
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
b': D
q: k b = b'
A -> C exact h.
  -
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
b': D
q: k b = b'
forall a : A,
(fun x : A => f x = b) a ->
(fun x : C => g x = b') (h a) intros a e.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
b': D
q: k b = b'
a: A
e: (fun x : A => f x = b) a
(fun x : C => g x = b') (h a) exact ((p a)^ @ ap k e @ q).
Defined.

Global Instance isequiv_functor_hfiber2 {A B C D}
       {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
       `{IsEquiv A C h} `{IsEquiv B D k}
       (p : k o f == g o h) {b : B} {b' : D} (q : k b = b')
  : IsEquiv (functor_hfiber2 p q).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
H: IsEquiv h
H0: IsEquiv k
p: k o f == g o h
b: B
b': D
q: k b = b'
IsEquiv (functor_hfiber2 p q)
Proof.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
H: IsEquiv h
H0: IsEquiv k
p: k o f == g o h
b: B
b': D
q: k b = b'
IsEquiv (functor_hfiber2 p q)
  refine (isequiv_functor_sigma (f := h)); intros a.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
H: IsEquiv h
H0: IsEquiv k
p: k o f == g o h
b: B
b': D
q: k b = b'
a: A
IsEquiv (fun e : f a = b => ((p a)^ @ ap k e) @ q)
  refine (isequiv_compose (f := fun e => (p a)^ @ ap k e) (g := fun e' => e' @ q)).
Defined.

Definition equiv_functor_hfiber2 {A B C D}
           {f : A -> B} {g : C -> D} {h : A <~> C} {k : B <~> D}
           (p : k o f == g o h) {b : B} {b' : D} (q : k b = b')
  : hfiber f b <~> hfiber g b'
  := Build_Equiv _ _ (functor_hfiber2 p q) _.

Definition functor_hfiber_compose {A B C X Y Z : Type} {k : A -> B} {l : B -> C}
    {f : A -> X} {g : B -> Y} {h : C -> Z} {i : X -> Y} {j : Y -> Z}
    (H : i o f == g o k) (K : j o g == h o l)
  : forall x, functor_hfiber (comm_square_comp' H K) x
    == (functor_hfiber K (i x)) o (functor_hfiber H x : hfiber f x -> _).
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
forall x : X,
functor_hfiber (comm_square_comp' H K) x ==
functor_hfiber K (i x)
o (functor_hfiber H x : hfiber f x -> hfiber g (i x))
Proof.
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
forall x : X,
functor_hfiber (comm_square_comp' H K) x ==
functor_hfiber K (i x)
o (functor_hfiber H x : hfiber f x -> hfiber g (i x))
  intros x [y p].
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
x: X
y: A
p: f y = x
functor_hfiber (comm_square_comp' H K) x (y; p) =
functor_hfiber K (i x) (functor_hfiber H x (y; p))
  destruct p.
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
y: A
functor_hfiber (comm_square_comp' H K) (f y) (y; 1) =
functor_hfiber K (i (f y))
  (functor_hfiber H (f y) (y; 1))
  apply (path_sigma' _ idpath).
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
y: A
transport (fun x : C => h x = j (i (f y))) 1
  ((comm_square_comp' H K (y; 1).1)^ @
   ap (fun x : X => j (i x)) (y; 1).2) =
(K (functor_hfiber H (f y) (y; 1)).1)^ @
ap j (functor_hfiber H (f y) (y; 1)).2
  refine (concat_p1 _ @ _).
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
y: A
(comm_square_comp' H K (y; 1).1)^ =
(K (functor_hfiber H (f y) (y; 1)).1)^ @
ap j (functor_hfiber H (f y) (y; 1)).2
  refine (inv_pp _ _ @ ap _ _).
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
y: A
(ap j (H (y; 1).1))^ =
ap j (functor_hfiber H (f y) (y; 1)).2
  refine ((ap_V _ _)^ @ ap _ _^).
A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
y: A
(functor_hfiber H (f y) (y; 1)).2 = (H (y; 1).1)^
  apply concat_p1.
Defined.

(** ** The 3x3 lemma for fibrations *)
Definition hfiber_functor_hfiber {A B C D}
  {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
  (p : k o f == g o h) (b : B) (c : C) (q : g c = k b)
  : hfiber (functor_hfiber p b) (c;q)
    <~> hfiber (functor_hfiber (fun x => (p x)^) c) (b;q^).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
hfiber (functor_hfiber p b) (c; q) <~>
hfiber (functor_hfiber (fun x : A => (p x)^) c)
  (b; q^)
Proof.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
hfiber (functor_hfiber p b) (c; q) <~>
hfiber (functor_hfiber (fun x : A => (p x)^) c)
  (b; q^)
  rapply (equiv_functor_sigma_id _ oE _ oE (equiv_functor_sigma_id _)^-1).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
forall a : hfiber h c,
?Goal a <~>
functor_hfiber (fun x : A => (p x)^) c a = (b; q^)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
{x : _ & ?Goal2 x} <~> {x : _ & ?Goal x}
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
forall a : hfiber f b,
?Goal2 a <~> functor_hfiber p b a = (c; q)
  1,3:intros; rapply equiv_path_sigma.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
{a : hfiber f b &
{p0 : (functor_hfiber p b a).1 = (c; q).1 &
transport (fun x : C => g x = k b) p0
  (functor_hfiber p b a).2 = (c; q).2}} <~>
{a : hfiber h c &
{p0
: (functor_hfiber (fun x : A => (p x)^) c a).1 =
  (b; q^).1 &
transport (fun x : B => k x = g c) p0
  (functor_hfiber (fun x : A => (p x)^) c a).2 =
(b; q^).2}}
  refine (equiv_sigma_assoc _ _ oE _ oE (equiv_sigma_assoc _ _)^-1).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
{a : A &
{p0 : f a = b &
{p1 : (functor_hfiber p b (a; p0)).1 = (c; q).1 &
transport (fun x : C => g x = k b) p1
  (functor_hfiber p b (a; p0)).2 = (c; q).2}}} <~>
{a : A &
{p0 : h a = c &
{p1
: (functor_hfiber (fun x : A => (p x)^) c (a; p0)).1 =
  (b; q^).1 &
transport (fun x : B => k x = g c) p1
  (functor_hfiber (fun x : A => (p x)^) c (a; p0)).2 =
(b; q^).2}}}
  apply equiv_functor_sigma_id; intros a; cbn.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
a: A
{p0 : f a = b &
{p1 : h a = c &
transport (fun x : C => g x = k b) p1
  ((p a)^ @ ap k p0) = q}} <~>
{p0 : h a = c &
{p1 : f a = b &
transport (fun x : B => k x = g c) p1
  (((p a)^)^ @ ap g p0) = q^}}
  refine (equiv_sigma_symm _ oE _).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
a: A
{p0 : f a = b &
{p1 : h a = c &
transport (fun x : C => g x = k b) p1
  ((p a)^ @ ap k p0) = q}} <~>
{a0 : f a = b &
{b0 : h a = c &
transport (fun x : B => k x = g c) a0
  (((p a)^)^ @ ap g b0) = q^}}
  do 2 (apply equiv_functor_sigma_id; intro).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
a: A
a0: f a = b
a1: h a = c
transport (fun x : C => g x = k b) a1
  ((p a)^ @ ap k a0) = q <~>
transport (fun x : B => k x = g c) a0
  (((p a)^)^ @ ap g a1) = q^
  refine ((equiv_ap inverse _ _)^-1 oE _).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
a: A
a0: f a = b
a1: h a = c
transport (fun x : C => g x = k b) a1
  ((p a)^ @ ap k a0) = q <~>
(transport (fun x : B => k x = g c) a0
   (((p a)^)^ @ ap g a1))^ = (q^)^
  refine (equiv_concat_r (inv_V q)^ _ oE _).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
a: A
a0: f a = b
a1: h a = c
transport (fun x : C => g x = k b) a1
  ((p a)^ @ ap k a0) = q <~>
(transport (fun x : B => k x = g c) a0
   (((p a)^)^ @ ap g a1))^ = q
  apply equiv_concat_l.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
b: B
c: C
q: g c = k b
a: A
a0: f a = b
a1: h a = c
(transport (fun x : B => k x = g c) a0
   (((p a)^)^ @ ap g a1))^ =
transport (fun x : C => g x = k b) a1
  ((p a)^ @ ap k a0)
  abstract (rewrite !transport_paths_Fl, !inv_pp, !inv_V, concat_pp_p; reflexivity).
Defined.

(** ** Replacing a map with a fibration *)
Definition equiv_fibration_replacement  {B C} (f:C ->B)
  : C <~> {y:B & hfiber f y}.
B, C: Type
f: C -> B
C <~> {y : B & hfiber f y}
Proof.
B, C: Type
f: C -> B
C <~> {y : B & hfiber f y}
  snrefine (Build_Equiv _ _ _ (
    Build_IsEquiv C {y:B & {x:C & f x = y}}
      (fun c => (f c; (c; idpath)))
      (fun c => c.2.1)
      _
      (fun c => idpath)
       _)).
B, C: Type
f: C -> B
(fun c : C => (f c; c; 1))
o (fun c : {y : B & {x : C & f x = y}} => (c.2).1) ==
idmap
B, C: Type
f: C -> B
forall x : C,
?eisretr ((fun c : C => (f c; c; 1)) x) =
ap (fun c : C => (f c; c; 1)) ((fun c : C => 1) x)
  -
B, C: Type
f: C -> B
(fun c : C => (f c; c; 1))
o (fun c : {y : B & {x : C & f x = y}} => (c.2).1) ==
idmap intros [? [? []]]; reflexivity.
  -
B, C: Type
f: C -> B
forall x : C,
((fun x0 : {y : B & {x0 : C & f x0 = y}} =>
  (fun (proj1 : B) (proj2 : {x1 : C & f x1 = proj1})
   =>
   (fun (proj0 : C) (proj3 : f proj0 = proj1) =>
    match
      proj3 as p in (_ = b)
      return
        ((f ((b; proj0; p).2).1; ((b; proj0; p).2).1;
         1) = (b; proj0; p))
    with
    | 1 => 1
    end) proj2.1 proj2.2) x0.1 x0.2)
 :
 (fun c : C => (f c; c; 1))
 o (fun c : {y : B & {x0 : C & f x0 = y}} => (c.2).1) ==
 idmap) ((fun c : C => (f c; c; 1)) x) =
ap (fun c : C => (f c; c; 1)) ((fun c : C => 1) x) reflexivity.
Defined.

Definition hfiber_fibration {X} (x : X) (P:X->Type)
  : P x <~> @hfiber (sig P) X pr1 x.
X: Type
x: X
P: X -> Type
P x <~> hfiber pr1 x
Proof.
X: Type
x: X
P: X -> Type
P x <~> hfiber pr1 x
  snrefine (Build_Equiv _ _ _
    (Build_IsEquiv (P x) { z : sig P & z.1 = x }
      (fun Px => ((x; Px); idpath))
      (fun Px => transport P Px.2 Px.1.2)
      _
      (fun Px => idpath)
      _)).
X: Type
x: X
P: X -> Type
(fun Px : P x => ((x; Px); 1))
o (fun Px : {z : {x : _ & P x} & z.1 = x} =>
   transport P Px.2 (Px.1).2) == idmap
X: Type
x: X
P: X -> Type
forall x0 : P x,
?eisretr ((fun Px : P x => ((x; Px); 1)) x0) =
ap (fun Px : P x => ((x; Px); 1))
  ((fun Px : P x => 1) x0)
  -
X: Type
x: X
P: X -> Type
(fun Px : P x => ((x; Px); 1))
o (fun Px : {z : {x : _ & P x} & z.1 = x} =>
   transport P Px.2 (Px.1).2) == idmap intros [[] []]; reflexivity.
  -
X: Type
x: X
P: X -> Type
forall x0 : P x,
((fun x1 : {z : {x : _ & P x} & z.1 = x} =>
  (fun proj1 : {x : _ & P x} =>
   (fun (proj2 : X) (proj3 : P proj2)
      (proj0 : (proj2; proj3).1 = x) =>
    match
      proj0 as p in (_ = x)
      return
        (((x;
          transport P ((proj2; proj3); p).2
            (((proj2; proj3); p).1).2); 1) =
         ((proj2; proj3); p))
    with
    | 1 => 1
    end) proj1.1 proj1.2) x1.1 x1.2)
 :
 (fun Px : P x => ((x; Px); 1))
 o (fun Px : {z : {x : _ & P x} & z.1 = x} =>
    transport P Px.2 (Px.1).2) == idmap)
  ((fun Px : P x => ((x; Px); 1)) x0) =
ap (fun Px : P x => ((x; Px); 1))
  ((fun Px : P x => 1) x0) reflexivity.
Defined.

(** ** Exercise 4.4: The unstable octahedral axiom. *)
Section UnstableOctahedral.

  Context (n : trunc_index) {A B C : Type} (f : A -> B) (g : B -> C).

  Definition hfiber_compose_map (c : C)
    : hfiber (g o f) c -> hfiber g c
    := fun x => (f x.1 ; x.2).

  Definition hfiber_hfiber_compose_map (b : B)
    : hfiber (hfiber_compose_map (g b)) (b;1) <~> hfiber f b.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
b: B
hfiber (hfiber_compose_map (g b)) (b; 1) <~>
hfiber f b
  Proof.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
b: B
hfiber (hfiber_compose_map (g b)) (b; 1) <~>
hfiber f b
    unfold hfiber, hfiber_compose_map.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
b: B
{x : {x : A & g (f x) = g b} & (f x.1; x.2) = (b; 1)} <~>
{x : A & f x = b}
    (** Once we "destruct" the equality in a sigma type, the rest is just shuffling of data and path induction. *)
    refine (_ oE equiv_functor_sigma_id (fun x => (equiv_path_sigma _ _ _)^-1)); cbn.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
b: B
{x : {x : A & g (f x) = g b} &
{p : f x.1 = b &
transport (fun x0 : B => g x0 = g b) p x.2 = 1}} <~>
{x : A & f x = b}
    make_equiv_contr_basedpaths.
  Defined.

  Definition hfiber_compose (c : C)
    : hfiber (g o f) c <~> { w : hfiber g c & hfiber f w.1 }.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
c: C
hfiber (g o f) c <~> {w : hfiber g c & hfiber f w.1}
  Proof.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
c: C
hfiber (g o f) c <~> {w : hfiber g c & hfiber f w.1}
    make_equiv_contr_basedpaths.
  Defined.

  Global Instance istruncmap_compose `{!IsTruncMap n g} `{!IsTruncMap n f}
    : IsTruncMap n (g o f).
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
IsTruncMap0: IsTruncMap n g
IsTruncMap1: IsTruncMap n f
IsTruncMap n (g o f)
  Proof.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
IsTruncMap0: IsTruncMap n g
IsTruncMap1: IsTruncMap n f
IsTruncMap n (g o f)
    intros c.
n: trunc_index
A, B, C: Type
f: A -> B
g: B -> C
IsTruncMap0: IsTruncMap n g
IsTruncMap1: IsTruncMap n f
c: C
IsTrunc n (hfiber (fun x : A => g (f x)) c)
    exact (istrunc_isequiv_istrunc _ (hfiber_compose c)^-1).
  Defined.

End UnstableOctahedral.

(** ** Fibers of constant functions *)
Definition hfiber_const A {B} (y y' : B)
  : hfiber (fun _ : A => y) y' <~> A * (y = y')
  := equiv_sigma_prod0 A (y = y').

Global Instance istruncmap_const n {A B} `{!IsTrunc n A}
       (y : B) `{!forall y', IsTrunc n (y = y')}
  : IsTruncMap n (fun _ : A => y)
  := fun y' => _.

(** ** [IsTruncMap n.+1 f <-> IsTruncMap n (ap f)] *)
Global Instance istruncmap_ap {A B} n (f:A -> B) `{!IsTruncMap n.+1 f}
  : forall x y, IsTruncMap n (@ap _ _ f x y)
  := fun x x' y =>
       istrunc_equiv_istrunc _ (hfiber_ap y)^-1.

Definition istruncmap_from_ap {A B} n (f:A -> B) `{!forall x y, IsTruncMap n (@ap _ _ f x y)}
  : IsTruncMap n.+1 f.
A, B: Type
n: trunc_index
f: A -> B
H: forall x y : A, IsTruncMap n (ap f)
IsTruncMap n.+1 f
Proof.
A, B: Type
n: trunc_index
f: A -> B
H: forall x y : A, IsTruncMap n (ap f)
IsTruncMap n.+1 f
  intro y; apply istrunc_S.
A, B: Type
n: trunc_index
f: A -> B
H: forall x y : A, IsTruncMap n (ap f)
y: B
forall x y0 : hfiber f y, IsTrunc n (x = y0)
  intros [a p] [b q];
    destruct q;
    exact (istrunc_equiv_istrunc _ (hfiber_ap p)).
Defined.

Definition equiv_istruncmap_ap `{Funext} {A B} n (f:A -> B)
  : IsTruncMap n.+1 f <~> (forall x y, IsTruncMap n (@ap _ _ f x y))
  := equiv_iff_hprop (@istruncmap_ap _ _ n f) (@istruncmap_from_ap _ _ n f).

Global Instance isequiv_ap_isembedding {A B} (f : A -> B) `{!IsEmbedding f}
  : forall x y, IsEquiv (@ap _ _ f x y).
A, B: Type
f: A -> B
IsEmbedding0: IsEmbedding f
forall x y : A, IsEquiv (ap f)
Proof.
A, B: Type
f: A -> B
IsEmbedding0: IsEmbedding f
forall x y : A, IsEquiv (ap f)
  intros x y.
A, B: Type
f: A -> B
IsEmbedding0: IsEmbedding f
x, y: A
IsEquiv (ap f) apply isequiv_contr_map,_.
Defined.

Definition equiv_ap_isembedding {A B} (f : A -> B) `{!IsEmbedding f} (x y : A)
  : (x = y) <~> (f x = f y)
  := Build_Equiv _ _ (ap f) _.

Definition isembedding_isequiv_ap {A B} (f : A -> B) `{!forall x y, IsEquiv (@ap _ _ f x y)}
  : IsEmbedding f.
A, B: Type
f: A -> B
H: forall x y : A, IsEquiv (ap f)
IsEmbedding f
Proof.
A, B: Type
f: A -> B
H: forall x y : A, IsEquiv (ap f)
IsEmbedding f
  rapply istruncmap_from_ap.
Defined.

Definition equiv_isequiv_ap_isembedding `{Funext} {A B} (f : A -> B)
  : IsEmbedding f <~> (forall x y, IsEquiv (@ap _ _ f x y)).
H: Funext
A, B: Type
f: A -> B
IsEmbedding f <~> (forall x y : A, IsEquiv (ap f))
Proof.
H: Funext
A, B: Type
f: A -> B
IsEmbedding f <~> (forall x y : A, IsEquiv (ap f))
  exact (equiv_iff_hprop (@isequiv_ap_isembedding _ _ f) (@isembedding_isequiv_ap _ _ f)).
Defined.

Lemma ap_isinj_embedding_beta {X Y : Type} (f : X -> Y) {I : IsEmbedding f} {x0 x1 : X}
  : forall (p : f x0 = f x1), ap f (isinj_embedding f I x0 x1 p) = p.
X, Y: Type
f: X -> Y
I: IsEmbedding f
x0, x1: X
forall p : f x0 = f x1,
ap f (isinj_embedding f I x0 x1 p) = p
Proof.
X, Y: Type
f: X -> Y
I: IsEmbedding f
x0, x1: X
forall p : f x0 = f x1,
ap f (isinj_embedding f I x0 x1 p) = p
  equiv_intro (equiv_ap_isembedding f x0 x1) q.
X, Y: Type
f: X -> Y
I: IsEmbedding f
x0, x1: X
q: x0 = x1
ap f
  (isinj_embedding f I x0 x1
     (equiv_ap_isembedding f x0 x1 q)) =
equiv_ap_isembedding f x0 x1 q
  induction q.
X, Y: Type
f: X -> Y
I: IsEmbedding f
x0: X
ap f
  (isinj_embedding f I x0 x0
     (equiv_ap_isembedding f x0 x0 1)) =
equiv_ap_isembedding f x0 x0 1 cbn.
X, Y: Type
f: X -> Y
I: IsEmbedding f
x0: X
ap f (isinj_embedding f I x0 x0 1) = 1
  exact (ap _ (isinj_embedding_beta f)).
Defined.