Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare.
Require Import Diagrams.CommutativeSquares.

Local Open Scope path_scope.

(** * Pullbacks *)

(** The pullback as an object *)
Definition Pullback {A B C} (f : B -> A) (g : C -> A)
  := { b : B & { c : C & f b = g c }}.

Global Arguments Pullback {A B C}%_type_scope (f g)%_function_scope.

(** The universal commutative square *)
Definition pullback_pr1 {A B C} {f : B -> A} {g : C -> A}
: Pullback f g -> B := (fun z => z.1).
Definition pullback_pr2 {A B C} {f : B -> A} {g : C -> A}
: Pullback f g -> C := (fun z => z.2.1).
Definition pullback_commsq {A B C} (f : B -> A) (g : C -> A)
: f o pullback_pr1 == g o pullback_pr2
:= (fun z => z.2.2).

(** The universally induced map into it by any commutative square *)
Definition pullback_corec {A B C D}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h)
: A -> Pullback k g
:= fun a => (f a ; h a ; p a).

Definition pullback_corec_uncurried {A B C D} (k : B -> D) (g : C -> D)
  : { f : A -> B & { h : A -> C & k o f == g o h }} -> (A -> Pullback k g).
A, B, C, D: Type
k: B -> D
g: C -> D
{f : A -> B & {h : A -> C & k o f == g o h}} ->
A -> Pullback k g
Proof.
A, B, C, D: Type
k: B -> D
g: C -> D
{f : A -> B & {h : A -> C & k o f == g o h}} ->
A -> Pullback k g
  intros [f [h p]].
A, B, C, D: Type
k: B -> D
g: C -> D
f: A -> B
h: A -> C
p: (fun x : A => k (f x)) == (fun x : A => g (h x))
A -> Pullback k g
  exact (pullback_corec p).
Defined.

Instance isequiv_pullback_corec {A B C D} (k : B -> D) (g : C -> D)
  : IsEquiv (@pullback_corec_uncurried A B C D k g).
A, B, C, D: Type
k: B -> D
g: C -> D
IsEquiv (pullback_corec_uncurried k g)
Proof.
A, B, C, D: Type
k: B -> D
g: C -> D
IsEquiv (pullback_corec_uncurried k g)
  snapply isequiv_adjointify.
A, B, C, D: Type
k: B -> D
g: C -> D
(A -> Pullback k g) ->
{f : A -> B & {h : A -> C & k o f == g o h}}
A, B, C, D: Type
k: B -> D
g: C -> D
pullback_corec_uncurried k g o ?g == idmap
A, B, C, D: Type
k: B -> D
g: C -> D
?g o pullback_corec_uncurried k g == idmap
  -
A, B, C, D: Type
k: B -> D
g: C -> D
(A -> Pullback k g) ->
{f : A -> B & {h : A -> C & k o f == g o h}} intro m.
A, B, C, D: Type
k: B -> D
g: C -> D
m: A -> Pullback k g
{f : A -> B & {h : A -> C & k o f == g o h}}
    exact (pullback_pr1 o m ; pullback_pr2 o m ; (pullback_commsq k g) o m).
  -
A, B, C, D: Type
k: B -> D
g: C -> D
pullback_corec_uncurried k g
o (fun m : A -> Pullback k g =>
   (pullback_pr1 o m; pullback_pr2 o m;
   pullback_commsq k g o m)) == idmap reflexivity.
  -
A, B, C, D: Type
k: B -> D
g: C -> D
(fun m : A -> Pullback k g =>
 (pullback_pr1 o m; pullback_pr2 o m;
 pullback_commsq k g o m))
o pullback_corec_uncurried k g == idmap reflexivity.
Defined.

Definition equiv_pullback_corec {A B C D} (k : B -> D) (g : C -> D)
  : { f : A -> B & { h : A -> C & k o f == g o h }} <~> (A -> Pullback k g)
  := Build_Equiv _ _ _ (isequiv_pullback_corec k g).

(** A homotopy commutative square is equivalent to a pullback of arrow types *)
Definition equiv_ispullback_commsq `{Funext} {A B C D} (k : B -> D) (g : C -> D)
  : { f : A -> B & { h : A -> C & k o f == g o h }}
    <~> @Pullback (A -> D) (A -> B) (A -> C) (fun f => k o f) (fun h => g o h).
H: Funext
A, B, C, D: Type
k: B -> D
g: C -> D
{f : A -> B & {h : A -> C & k o f == g o h}} <~>
Pullback (fun f : A -> B => k o f)
  (fun h : A -> C => g o h)
Proof.
H: Funext
A, B, C, D: Type
k: B -> D
g: C -> D
{f : A -> B & {h : A -> C & k o f == g o h}} <~>
Pullback (fun f : A -> B => k o f)
  (fun h : A -> C => g o h)
  apply equiv_functor_sigma_id; intro f.
H: Funext
A, B, C, D: Type
k: B -> D
g: C -> D
f: A -> B
{h : A -> C &
(fun x : A => k (f x)) == (fun x : A => g (h x))} <~>
{c : A -> C &
(fun x : A => k (f x)) = (fun x : A => g (c x))}
  apply equiv_functor_sigma_id; intro h.
H: Funext
A, B, C, D: Type
k: B -> D
g: C -> D
f: A -> B
h: A -> C
(fun x : A => k (f x)) == (fun x : A => g (h x)) <~>
(fun x : A => k (f x)) = (fun x : A => g (h x))
  apply equiv_path_forall.
Defined.

(** The diagonal of a map *)
Definition diagonal {X Y : Type} (f : X -> Y) : X -> Pullback f f
  := fun x => (x;x;idpath).

(** The fiber of the diagonal is a path-space in the fiber. *)
Definition hfiber_diagonal {X Y : Type} (f : X -> Y) (p : Pullback f f)
  : hfiber (diagonal f) p <~>  ((p.1 ; p.2.2) = (p.2.1 ; idpath) :> hfiber f (f p.2.1)).
X, Y: Type
f: X -> Y
p: Pullback f f
hfiber (diagonal f) p <~>
(p.1; (p.2).2) = ((p.2).1; 1)
Proof.
X, Y: Type
f: X -> Y
p: Pullback f f
hfiber (diagonal f) p <~>
(p.1; (p.2).2) = ((p.2).1; 1)
  destruct p as [x1 [x2 p]]; cbn.
X, Y: Type
f: X -> Y
x1, x2: X
p: f x1 = f x2
hfiber (diagonal f) (x1; x2; p) <~> (x1; p) = (x2; 1)
  refine (_ oE equiv_functor_sigma_id (fun x => (equiv_path_sigma _ _ _)^-1)); cbn.
X, Y: Type
f: X -> Y
x1, x2: X
p: f x1 = f x2
{x : X &
{p0 : x = x1 &
transport (fun b : X => {c : X & f b = f c}) p0 (x; 1) =
(x2; p)}} <~> (x1; p) = (x2; 1)
  refine (_ oE equiv_sigma_assoc' _ _).
X, Y: Type
f: X -> Y
x1, x2: X
p: f x1 = f x2
{ap : {a : X & a = x1} &
transport (fun b : X => {c : X & f b = f c}) ap.2
  (ap.1; 1) = (x2; p)} <~> (x1; p) = (x2; 1)
  refine (_ oE equiv_contr_sigma _); cbn.
X, Y: Type
f: X -> Y
x1, x2: X
p: f x1 = f x2
(x1; 1) = (x2; p) <~> (x1; p) = (x2; 1)
  refine (equiv_path_sigma _ _ _ oE _ oE (equiv_path_sigma _ _ _)^-1); cbn.
X, Y: Type
f: X -> Y
x1, x2: X
p: f x1 = f x2
{p0 : x1 = x2 &
transport (fun c : X => f x1 = f c) p0 1 = p} <~>
{p0 : x1 = x2 &
transport (fun x : X => f x = f x2) p0 p = 1}
  apply equiv_functor_sigma_id; intros q.
X, Y: Type
f: X -> Y
x1, x2: X
p: f x1 = f x2
q: x1 = x2
transport (fun c : X => f x1 = f c) q 1 = p <~>
transport (fun x : X => f x = f x2) q p = 1
  destruct q; cbn.
X, Y: Type
f: X -> Y
x1: X
p: f x1 = f x1
1 = p <~> p = 1
  apply equiv_path_inverse.
Defined.

(** Symmetry of the pullback *)
Definition equiv_pullback_symm {A B C} (f : B -> A) (g : C -> A)
: Pullback f g <~> Pullback g f.
A, B, C: Type
f: B -> A
g: C -> A
Pullback f g <~> Pullback g f
Proof.
A, B, C: Type
f: B -> A
g: C -> A
Pullback f g <~> Pullback g f
  refine (_ oE equiv_sigma_symm (fun b c => f b = g c)).
A, B, C: Type
f: B -> A
g: C -> A
{b : C & {a : B & f a = g b}} <~> Pullback g f
  apply equiv_functor_sigma_id; intros c.
A, B, C: Type
f: B -> A
g: C -> A
c: C
{a : B & f a = g c} <~> {c0 : B & g c = f c0}
  apply equiv_functor_sigma_id; intros b.
A, B, C: Type
f: B -> A
g: C -> A
c: C
b: B
f b = g c <~> g c = f b
  apply equiv_path_inverse.
Defined.

(** Pullback over [Unit] is equivalent to a product. *)
Definition equiv_pullback_unit_prod (A B : Type)
: Pullback (const_tt A) (const_tt B) <~> A * B.
A, B: Type
Pullback (const_tt A) (const_tt B) <~> A * B
Proof.
A, B: Type
Pullback (const_tt A) (const_tt B) <~> A * B
  refine (equiv_sigma_prod0 A B oE _).
A, B: Type
Pullback (const_tt A) (const_tt B) <~> {_ : A & B}
  snapply equiv_functor_sigma_id; intro a; cbn.
A, B: Type
a: A
{c : B & const_tt A a = const_tt B c} <~> B
  rapply equiv_sigma_contr.
Defined.

(** Pullback of [Unit] is equivalent to [hfiber]. *)
Definition equiv_pullback_unit_hfiber {A B : Type} (f : A -> B) (g : Unit -> B)
  : Pullback f g <~> hfiber f (g tt).
A, B: Type
f: A -> B
g: Unit -> B
Pullback f g <~> hfiber f (g tt)
Proof.
A, B: Type
f: A -> B
g: Unit -> B
Pullback f g <~> hfiber f (g tt)
  snapply equiv_functor_sigma_id; intro a; cbn.
A, B: Type
f: A -> B
g: Unit -> B
a: A
{c : Unit & f a = g c} <~> f a = g tt
  exact (equiv_contr_sigma (fun c => _ = g c)).
Defined.

(** The same for the symmetrical pullback. *)
Definition equiv_pullback_unit_hfiber' {A B : Type} (f : Unit -> B) (g : A -> B)
  : Pullback f g <~> hfiber g (f tt)
  := equiv_pullback_unit_hfiber _ _ oE equiv_pullback_symm _ _.

(** When both corners are [Unit] you get the path type. *)
Definition equiv_pullback_unit_unit_paths {B : Type} (f g : Unit -> B)
  : Pullback f g <~> (f tt = g tt).
B: Type
f, g: Unit -> B
Pullback f g <~> f tt = g tt
Proof.
B: Type
f, g: Unit -> B
Pullback f g <~> f tt = g tt
  refine (_ oE equiv_contr_sigma _).
B: Type
f, g: Unit -> B
{c : Unit & f (center Unit) = g c} <~> f tt = g tt
  exact (equiv_contr_sigma (fun c => _ = g c)).
Defined.

(** The property of a given commutative square being a pullback *)
Definition IsPullback {A B C D}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h)
  := IsEquiv (pullback_corec p).

Definition equiv_ispullback {A B C D}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h) (ip : IsPullback p)
  : A <~> Pullback k g
  := Build_Equiv _ _ (pullback_corec p) ip.

(** This is equivalent to the transposed square being a pullback. *)
Definition ispullback_symm {A B C D}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : g o h == k o f) (pb : IsPullback (fun a => (p a)^))
  : IsPullback p.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: g o h == k o f
pb: IsPullback (fun a : A => (p a)^)
IsPullback p
Proof.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: g o h == k o f
pb: IsPullback (fun a : A => (p a)^)
IsPullback p
  rapply (cancelL_isequiv (equiv_pullback_symm g k)).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: g o h == k o f
pb: IsPullback (fun a : A => (p a)^)
IsEquiv
  (fun x : A =>
   equiv_pullback_symm g k (pullback_corec p x))
  exact pb.
Defined.

(** The pullback of the projections [{d:D & P d} -> D <- {d:D & Q d}] is equivalent to [{d:D & P d * Q d}]. *)
Definition ispullback_sigprod {D : Type} (P Q : D -> Type)
  : IsPullback (fun z:{d:D & P d * Q d} => 1%path : (z.1;fst z.2).1 = (z.1;snd z.2).1).
D: Type
P, Q: D -> Type
IsPullback
  (fun z : {d : D & P d * Q d} =>
   1 : (z.1; fst z.2).1 = (z.1; snd z.2).1)
Proof.
D: Type
P, Q: D -> Type
IsPullback
  (fun z : {d : D & P d * Q d} =>
   1 : (z.1; fst z.2).1 = (z.1; snd z.2).1)
  srapply isequiv_adjointify.
D: Type
P, Q: D -> Type
Pullback pr1 pr1 -> {d : D & P d * Q d}
D: Type
P, Q: D -> Type
pullback_corec
  (fun z : {d : D & P d * Q d} =>
   1 : (z.1; fst z.2).1 = (z.1; snd z.2).1) o ?g ==
idmap
D: Type
P, Q: D -> Type
?g
o pullback_corec
    (fun z : {d : D & P d * Q d} =>
     1 : (z.1; fst z.2).1 = (z.1; snd z.2).1) == idmap
  -
D: Type
P, Q: D -> Type
Pullback pr1 pr1 -> {d : D & P d * Q d} intros [[d1 p] [[d2 q] e]]; cbn in e.
D: Type
P, Q: D -> Type
d1: D
p: P d1
d2: D
q: Q d2
e: d1 = d2
{d : D & P d * Q d}
    exists d1.
D: Type
P, Q: D -> Type
d1: D
p: P d1
d2: D
q: Q d2
e: d1 = d2
P d1 * Q d1 exact (p, e^ # q).
  -
D: Type
P, Q: D -> Type
pullback_corec
  (fun z : {d : D & P d * Q d} =>
   1 : (z.1; fst z.2).1 = (z.1; snd z.2).1)
o (fun X : Pullback pr1 pr1 =>
   (fun proj2 : {x : _ & P x} =>
    (fun (d1 : D) (p : P d1)
       (proj3 : {c : {x : _ & Q x} & (d1; p).1 = c.1})
     =>
     (fun proj4 : {x : _ & Q x} =>
      (fun (d2 : D) (q : Q d2)
         (e : (d1; p).1 = (d2; q).1) =>
       (d1; (p, transport Q e^ q))) proj4.1 proj4.2)
       proj3.1 proj3.2) proj2.1 proj2.2) X.1 X.2) ==
idmap intros [[d1 p] [[d2 q] e]]; unfold pullback_corec; cbn in *.
D: Type
P, Q: D -> Type
d1: D
p: P d1
d2: D
q: Q d2
e: d1 = d2
((d1; p); (d1; transport Q e^ q); 1) =
((d1; p); (d2; q); e)
    destruct e; reflexivity.
  -
D: Type
P, Q: D -> Type
(fun X : Pullback pr1 pr1 =>
 (fun proj2 : {x : _ & P x} =>
  (fun (d1 : D) (p : P d1)
     (proj3 : {c : {x : _ & Q x} & (d1; p).1 = c.1})
   =>
   (fun proj4 : {x : _ & Q x} =>
    (fun (d2 : D) (q : Q d2)
       (e : (d1; p).1 = (d2; q).1) =>
     (d1; (p, transport Q e^ q))) proj4.1 proj4.2)
     proj3.1 proj3.2) proj2.1 proj2.2) X.1 X.2)
o pullback_corec
    (fun z : {d : D & P d * Q d} =>
     1 : (z.1; fst z.2).1 = (z.1; snd z.2).1) == idmap intros [d [p q]]; reflexivity.
Defined.

Definition equiv_sigprod_pullback {D : Type} (P Q : D -> Type)
  : {d:D & P d * Q d} <~> Pullback (@pr1 D P) (@pr1 D Q)
  := Build_Equiv _ _ _ (ispullback_sigprod P Q).

(** For any commutative square, the fiber of the fibers is equivalent to the fiber of the "gap map" [pullback_corec]. *)
Definition hfiber_pullback_corec {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 : k b = g c)
  : hfiber (pullback_corec p) (b; c; q) <~> hfiber (functor_hfiber p b) (c; 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: k b = g c
hfiber (pullback_corec p) (b; c; q) <~>
hfiber (functor_hfiber p b) (c; 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: k b = g c
hfiber (pullback_corec p) (b; c; q) <~>
hfiber (functor_hfiber p b) (c; q^)
  unfold hfiber, functor_hfiber, 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
c: C
q: k b = g c
{x : A & pullback_corec p x = (b; c; q)} <~>
{x : {x : A & f x = b} &
(h x.1; (p x.1)^ @ ap k x.2) = (c; q^)}
  refine (equiv_sigma_assoc _ _ 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: k b = g c
{x : A & pullback_corec p x = (b; c; q)} <~>
{a : A &
{p0 : f a = b &
(h (a; p0).1; (p (a; p0).1)^ @ ap k (a; p0).2) =
(c; q^)}}
  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: k b = g c
a: A
pullback_corec p a = (b; c; q) <~>
{p0 : f a = b & (h a; (p a)^ @ ap k p0) = (c; q^)}
  refine (_ oE (equiv_path_sigma _ _ _)^-1); 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: k b = g c
a: A
{p0 : f a = b &
transport (fun b : B => {c : C & k b = g c}) p0
  (h a; p a) = (c; q)} <~>
{p0 : f a = b & (h a; (p a)^ @ ap k p0) = (c; q^)}
  apply equiv_functor_sigma_id; intro p0; 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: k b = g c
a: A
p0: f a = b
transport (fun b : B => {c : C & k b = g c}) p0
  (h a; p a) = (c; q) <~>
(h a; (p a)^ @ ap k p0) = (c; q^)
  rewrite transport_sigma'; 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: k b = g c
a: A
p0: f a = b
(h a; transport (fun x : B => k x = g (h a)) p0 (p a)) =
(c; q) <~> (h a; (p a)^ @ ap k p0) = (c; q^)
  refine ((equiv_path_sigma _ _ _) oE _ oE (equiv_path_sigma _ _ _)^-1); 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: k b = g c
a: A
p0: f a = b
{p1 : h a = c &
transport (fun c : C => k b = g c) p1
  (transport (fun x : B => k x = g (h a)) p0 (p a)) =
q} <~>
{p1 : h a = c &
transport (fun x : C => g x = k b) p1
  ((p a)^ @ ap k p0) = q^}
  apply equiv_functor_sigma_id; intro p1; 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: k b = g c
a: A
p0: f a = b
p1: h a = c
transport (fun c : C => k b = g c) p1
  (transport (fun x : B => k x = g (h a)) p0 (p a)) =
q <~>
transport (fun x : C => g x = k b) p1
  ((p a)^ @ ap k p0) = q^
  rewrite !transport_paths_Fr, !transport_paths_Fl.
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: k b = g c
a: A
p0: f a = b
p1: h a = c
((ap k p0)^ @ p a) @ ap g p1 = q <~>
(ap g p1)^ @ ((p a)^ @ ap k p0) = q^
  refine (_ oE (equiv_ap (equiv_path_inverse _ _) _ _)); 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: k b = g c
a: A
p0: f a = b
p1: h a = c
(((ap k p0)^ @ p a) @ ap g p1)^ = q^ <~>
(ap g p1)^ @ ((p a)^ @ ap k p0) = 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: k b = g c
a: A
p0: f a = b
p1: h a = c
(ap g p1)^ @ ((p a)^ @ ap k p0) =
(((ap k p0)^ @ p a) @ ap g p1)^
  refine (_ @ (inv_pp _ _)^).
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: k b = g c
a: A
p0: f a = b
p1: h a = c
(ap g p1)^ @ ((p a)^ @ ap k p0) =
(ap g p1)^ @ ((ap k p0)^ @ p a)^  apply whiskerL.
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: k b = g c
a: A
p0: f a = b
p1: h a = c
(p a)^ @ ap k p0 = ((ap k p0)^ @ p a)^
  refine (_ @ (inv_pp _ _)^).
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: k b = g c
a: A
p0: f a = b
p1: h a = c
(p a)^ @ ap k p0 = (p a)^ @ ((ap k p0)^)^  apply whiskerL.
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: k b = g c
a: A
p0: f a = b
p1: h a = c
ap k p0 = ((ap k p0)^)^
  symmetry; apply inv_V.
Defined.

(** If the induced maps on fibers are equivalences, then a square is a pullback. *)
Definition ispullback_isequiv_functor_hfiber {A B C D : Type}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h)
           (e : forall b:B, IsEquiv (functor_hfiber p b))
  : IsPullback p.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: forall b : B, IsEquiv (functor_hfiber p b)
IsPullback p
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
e: forall b : B, IsEquiv (functor_hfiber p b)
IsPullback p
  unfold IsPullback.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: forall b : B, IsEquiv (functor_hfiber p b)
IsEquiv (pullback_corec p)
  apply isequiv_contr_map; intro 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
e: forall b : B, IsEquiv (functor_hfiber p b)
x: Pullback k g
Contr (hfiber (pullback_corec p) x)
  rapply contr_equiv'.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: forall b : B, IsEquiv (functor_hfiber p b)
x: Pullback k g
?Goal <~> hfiber (pullback_corec p) 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
e: forall b : B, IsEquiv (functor_hfiber p b)
x: Pullback k g
Contr ?Goal
  -
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: forall b : B, IsEquiv (functor_hfiber p b)
x: Pullback k g
?Goal <~> hfiber (pullback_corec p) x symmetry; apply hfiber_pullback_corec.
  -
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: forall b : B, IsEquiv (functor_hfiber p b)
x: Pullback k g
Contr
  (hfiber (functor_hfiber p x.1) ((x.2).1; ((x.2).2)^)) exact _.
Defined.

(** Conversely, if the square is a pullback then the induced maps on fibers are equivalences. *)
Definition isequiv_functor_hfiber_ispullback {A B C D : Type}
           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h)
           (e : IsPullback p)
  : forall b:B, IsEquiv (functor_hfiber p 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
e: IsPullback p
forall b : B, IsEquiv (functor_hfiber p 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
e: IsPullback p
forall b : B, IsEquiv (functor_hfiber p b)
  apply isequiv_from_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
e: IsPullback p
IsEquiv (functor_sigma idmap (functor_hfiber p))
  unfold IsPullback in 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
e: IsEquiv (pullback_corec p)
IsEquiv (functor_sigma idmap (functor_hfiber p))
  snapply isequiv_commsq'.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
Type
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
Type
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
?C -> ?D
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
{x : _ & hfiber f x} -> ?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
e: IsEquiv (pullback_corec p)
{a : B & hfiber g (k a)} -> ?D
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
?g o ?h == ?k o functor_sigma idmap (functor_hfiber p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv ?g
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv ?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
e: IsEquiv (pullback_corec p)
IsEquiv ?k
  4: exact (equiv_fibration_replacement f)^-1%equiv.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
Type
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
A -> ?D
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
{a : B & hfiber g (k a)} -> ?D
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
?g o (equiv_fibration_replacement f)^-1%equiv ==
?k o functor_sigma idmap (functor_hfiber p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv ?g
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (equiv_fibration_replacement f)^-1%equiv
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv ?k
  1: exact (Pullback k g).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
A -> Pullback k g
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
{a : B & hfiber g (k a)} -> Pullback k g
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
?g o (equiv_fibration_replacement f)^-1%equiv ==
?k o functor_sigma idmap (functor_hfiber p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv ?g
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (equiv_fibration_replacement f)^-1%equiv
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv ?k
  1: exact (pullback_corec p).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
{a : B & hfiber g (k a)} -> Pullback k g
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
pullback_corec p
o (equiv_fibration_replacement f)^-1%equiv ==
?k o functor_sigma idmap (functor_hfiber p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (pullback_corec p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (equiv_fibration_replacement f)^-1%equiv
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv ?k
  {
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
{a : B & hfiber g (k a)} -> Pullback k g apply (functor_sigma idmap); intro 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
e: IsEquiv (pullback_corec p)
b: B
hfiber g (k b) -> {c : C & k b = g c}
    apply (functor_sigma idmap); intro 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
e: IsEquiv (pullback_corec p)
b: B
c: C
g c = k b -> k b = g c
    exact inverse. }
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
pullback_corec p
o (equiv_fibration_replacement f)^-1%equiv ==
functor_sigma idmap
  (fun b : B =>
   functor_sigma idmap (fun c : C => inverse))
o functor_sigma idmap (functor_hfiber p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (pullback_corec p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (equiv_fibration_replacement f)^-1%equiv
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv
  (functor_sigma idmap
     (fun b : B =>
      functor_sigma idmap (fun c : C => inverse)))
  {
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
pullback_corec p
o (equiv_fibration_replacement f)^-1%equiv ==
functor_sigma idmap
  (fun b : B =>
   functor_sigma idmap (fun c : C => inverse))
o functor_sigma idmap (functor_hfiber p) intros [x [y 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
e: IsEquiv (pullback_corec p)
x: B
y: A
q: f y = x
pullback_corec p
  ((equiv_fibration_replacement f)^-1%equiv (x; y; q)) =
functor_sigma idmap
  (fun b : B =>
   functor_sigma idmap (fun c : C => inverse))
  (functor_sigma idmap (functor_hfiber p) (x; y; q))
    destruct 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
e: IsEquiv (pullback_corec p)
y: A
pullback_corec p
  ((equiv_fibration_replacement f)^-1%equiv
     (f y; y; 1)) =
functor_sigma idmap
  (fun b : B =>
   functor_sigma idmap (fun c : C => inverse))
  (functor_sigma idmap (functor_hfiber p) (f y; y; 1))
    apply (path_sigma' _ idpath).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
y: A
transport (fun b : B => {c : C & k b = g c}) 1
  (h
     ((equiv_fibration_replacement f)^-1%equiv
        (f y; y; 1));
  p
    ((equiv_fibration_replacement f)^-1%equiv
       (f y; y; 1))) =
functor_sigma idmap (fun c : C => inverse)
  (functor_sigma idmap (functor_hfiber p) (f y; y; 1)).2
    apply (path_sigma' _ idpath).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
y: A
transport
  (fun c : C =>
   k
     (f
        ((equiv_fibration_replacement f)^-1%equiv
           (f y; y; 1))) = g c) 1
  (p
     ((equiv_fibration_replacement f)^-1%equiv
        (f y; y; 1))) =
(((functor_sigma idmap (functor_hfiber p) (f y; y; 1)).2).2)^
    simpl.
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
y: A
p y = ((p y)^ @ 1)^
    refine (_^ @ (inv_Vp _ _)^).
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
y: A
1^ @ p y = p y
    apply concat_1p. }
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (pullback_corec p)
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv (equiv_fibration_replacement f)^-1%equiv
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
e: IsEquiv (pullback_corec p)
IsEquiv
  (functor_sigma idmap
     (fun b : B =>
      functor_sigma idmap (fun c : C => inverse)))
  all: exact _.
Defined.

(** The pullback of a map along another one *)
Definition pullback_along {A B C} (f : B -> A) (g : C -> A)
: Pullback f g -> B
  := pr1.

Notation "f ^*" := (pullback_along f) : function_scope.

Definition hfiber_pullback_along {A B C} (f : B -> A) (g : C -> A) (b:B)
: hfiber (f ^* g) b <~> hfiber g (f b).
A, B, C: Type
f: B -> A
g: C -> A
b: B
hfiber (f^* g) b <~> hfiber g (f b)
Proof.
A, B, C: Type
f: B -> A
g: C -> A
b: B
hfiber (f^* g) b <~> hfiber g (f b)
  refine (equiv_functor_sigma_id (fun c => equiv_path_inverse _ _) oE _).
A, B, C: Type
f: B -> A
g: C -> A
b: B
hfiber (f^* g) b <~> {c : C & f b = g c}
  make_equiv_contr_basedpaths.
Defined.

(** And the dual sort of pullback *)
Definition pullback_along' {A B C} (g : C -> A) (f : B -> A)
: Pullback f g -> C
  := fun z => z.2.1.

Arguments pullback_along' / .

Notation "g ^*'" := (pullback_along' g) : function_scope.

Definition hfiber_pullback_along' {A B C} (g : C -> A) (f : B -> A) (c:C)
: hfiber (g ^*' f) c <~> hfiber f (g c).
A, B, C: Type
g: C -> A
f: B -> A
c: C
hfiber (g ^*' f) c <~> hfiber f (g c)
Proof.
A, B, C: Type
g: C -> A
f: B -> A
c: C
hfiber (g ^*' f) c <~> hfiber f (g c)
  make_equiv_contr_basedpaths.
Defined.

(** A version where [g] is pointed, but we unbundle the pointed condition to avoid importing pointed types. *)
Definition hfiber_pullback_along_pointed {A B C} {c : C} {a : A}
           (g : C -> A) (f : B -> A) (p : g c = a)
  : hfiber (g ^*' f) c <~> hfiber f a.
A, B, C: Type
c: C
a: A
g: C -> A
f: B -> A
p: g c = a
hfiber (g ^*' f) c <~> hfiber f a
Proof.
A, B, C: Type
c: C
a: A
g: C -> A
f: B -> A
p: g c = a
hfiber (g ^*' f) c <~> hfiber f a
  refine (_ oE hfiber_pullback_along' _ _ _); cbn.
A, B, C: Type
c: C
a: A
g: C -> A
f: B -> A
p: g c = a
hfiber f (g c) <~> hfiber f a
  srapply (equiv_functor_hfiber2 (h:=equiv_idmap) (k:=equiv_idmap)).
A, B, C: Type
c: C
a: A
g: C -> A
f: B -> A
p: g c = a
1%equiv o f == f o 1%equiv
A, B, C: Type
c: C
a: A
g: C -> A
f: B -> A
p: g c = a
1%equiv (g c) = a
  -
A, B, C: Type
c: C
a: A
g: C -> A
f: B -> A
p: g c = a
1%equiv o f == f o 1%equiv reflexivity.
  -
A, B, C: Type
c: C
a: A
g: C -> A
f: B -> A
p: g c = a
1%equiv (g c) = a assumption.
Defined.

Section Functor_Pullback.

  Context {A1 B1 C1 A2 B2 C2}
          (f1 : B1 -> A1) (g1 : C1 -> A1)
          (f2 : B2 -> A2) (g2 : C2 -> A2)
          (h : A1 -> A2) (k : B1 -> B2) (l : C1 -> C2)
          (p : f2 o k == h o f1) (q : g2 o l == h o g1).

  Definition functor_pullback : Pullback f1 g1 -> Pullback f2 g2
    := functor_sigma k
        (fun b1 => (functor_sigma l
                     (fun c1 e1 => p b1 @ ap h e1 @ (q c1)^))).

  Definition hfiber_functor_pullback (z : Pullback f2 g2)
  : hfiber functor_pullback z
    <~> Pullback (transport (hfiber h) z.2.2 o functor_hfiber (k := f2) p z.1)
                 (functor_hfiber q z.2.1).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
z: Pullback f2 g2
hfiber functor_pullback z <~>
Pullback
  (transport (hfiber h) (z.2).2 o functor_hfiber p z.1)
  (functor_hfiber q (z.2).1)
  Proof.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
z: Pullback f2 g2
hfiber functor_pullback z <~>
Pullback
  (transport (hfiber h) (z.2).2 o functor_hfiber p z.1)
  (functor_hfiber q (z.2).1)
    destruct z as [b2 [c2 e2]].
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
hfiber functor_pullback (b2; c2; e2) <~>
Pullback
  (fun x : hfiber k (b2; c2; e2).1 =>
   transport (hfiber h) ((b2; c2; e2).2).2
     (functor_hfiber p (b2; c2; e2).1 x))
  (functor_hfiber q ((b2; c2; e2).2).1)
    refine (_ oE hfiber_functor_sigma _ _ _ _ _ _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
{w : hfiber k b2 &
hfiber
  (functor_sigma l
     (fun (c1 : C1) (e1 : f1 w.1 = g1 c1) =>
      (p w.1 @ ap h e1) @ (q c1)^))
  (transport (fun b : B2 => {c : C2 & f2 b = g2 c})
     (w.2)^ (c2; e2))} <~>
Pullback
  (fun x : hfiber k (b2; c2; e2).1 =>
   transport (hfiber h) ((b2; c2; e2).2).2
     (functor_hfiber p (b2; c2; e2).1 x))
  (functor_hfiber q ((b2; c2; e2).2).1)
    apply equiv_functor_sigma_id.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
forall a : hfiber k b2,
hfiber
  (functor_sigma l
     (fun (c1 : C1) (e1 : f1 a.1 = g1 c1) =>
      (p a.1 @ ap h e1) @ (q c1)^))
  (transport (fun b : B2 => {c : C2 & f2 b = g2 c})
     (a.2)^ (c2; e2)) <~>
{c : hfiber l ((b2; c2; e2).2).1 &
transport (hfiber h) ((b2; c2; e2).2).2
  (functor_hfiber p (b2; c2; e2).1 a) =
functor_hfiber q ((b2; c2; e2).2).1 c}
    intros [b1 e1]; simpl.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
hfiber
  (functor_sigma l
     (fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
      (p b1 @ ap h e1) @ (q c1)^))
  (transport (fun b : B2 => {c : C2 & f2 b = g2 c})
     e1^ (c2; e2)) <~>
{c : hfiber l c2 &
transport (hfiber h) e2 (functor_hfiber p b2 (b1; e1)) =
functor_hfiber q c2 c}
    refine (_ oE (equiv_transport _ (transport_sigma' e1^ (c2; e2)))).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
hfiber
  (functor_sigma l
     (fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
      (p b1 @ ap h e1) @ (q c1)^))
  ((c2; e2).1;
  transport (fun x : B2 => f2 x = g2 (c2; e2).1) e1^
    (c2; e2).2) <~>
{c : hfiber l c2 &
transport (hfiber h) e2 (functor_hfiber p b2 (b1; e1)) =
functor_hfiber q c2 c}
    refine (_ oE hfiber_functor_sigma _ _ _ _ _ _); simpl.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
{w : hfiber l c2 &
hfiber
  (fun e1 : f1 b1 = g1 w.1 =>
   (p b1 @ ap h e1) @ (q w.1)^)
  (transport (fun c : C2 => f2 (k b1) = g2 c) (w.2)^
     (transport (fun x : B2 => f2 x = g2 c2) e1^ e2))} <~>
{c : hfiber l c2 &
transport (hfiber h) e2 (functor_hfiber p b2 (b1; e1)) =
functor_hfiber q c2 c}
    apply equiv_functor_sigma_id.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
forall a : hfiber l c2,
hfiber
  (fun e1 : f1 b1 = g1 a.1 =>
   (p b1 @ ap h e1) @ (q a.1)^)
  (transport (fun c : C2 => f2 (k b1) = g2 c) (a.2)^
     (transport (fun x : B2 => f2 x = g2 c2) e1^ e2)) <~>
transport (hfiber h) e2 (functor_hfiber p b2 (b1; e1)) =
functor_hfiber q c2 a
    intros [c1 e3]; simpl.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
hfiber
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  (transport (fun c : C2 => f2 (k b1) = g2 c) e3^
     (transport (fun x : B2 => f2 x = g2 c2) e1^ e2)) <~>
transport (hfiber h) e2 (functor_hfiber p b2 (b1; e1)) =
functor_hfiber q c2 (c1; e3)
    refine (_ oE (equiv_transport _
                   (ap (fun e => e3^ # e) (transport_paths_Fl e1^ e2)))).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
hfiber
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  (transport (fun c : C2 => f2 (k b1) = g2 c) e3^
     ((ap f2 e1^)^ @ e2)) <~>
transport (hfiber h) e2 (functor_hfiber p b2 (b1; e1)) =
functor_hfiber q c2 (c1; e3)
    refine (_ oE (equiv_transport _ (transport_paths_Fr e3^ _))).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
hfiber
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  (((ap f2 e1^)^ @ e2) @ ap g2 e3^) <~>
transport (hfiber h) e2 (functor_hfiber p b2 (b1; e1)) =
functor_hfiber q c2 (c1; e3)
    unfold functor_hfiber; simpl.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
hfiber
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  (((ap f2 e1^)^ @ e2) @ ap g2 e3^) <~>
transport (hfiber h) e2
  (functor_sigma f1
     (fun (a : B1) (e : k a = b2) => (p a)^ @ ap f2 e)
     (b1; e1)) =
functor_sigma g1
  (fun (a : C1) (e : l a = c2) => (q a)^ @ ap g2 e)
  (c1; e3)
    refine (equiv_concat_l (transport_sigma' e2 _) _ oE _); simpl.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
hfiber
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  (((ap f2 e1^)^ @ e2) @ ap g2 e3^) <~>
(f1 b1;
transport (fun x : A2 => h (f1 b1) = x) e2
  ((p b1)^ @ ap f2 e1)) =
functor_sigma g1
  (fun (a : C1) (e : l a = c2) => (q a)^ @ ap g2 e)
  (c1; e3)
    refine (equiv_path_sigma _ _ _ oE _); simpl.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
hfiber
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  (((ap f2 e1^)^ @ e2) @ ap g2 e3^) <~>
{p0 : f1 b1 = g1 c1 &
transport (fun y : A1 => h y = g2 c2) p0
  (transport (fun x : A2 => h (f1 b1) = x) e2
     ((p b1)^ @ ap f2 e1)) = (q c1)^ @ ap g2 e3}
    apply equiv_functor_sigma_id; intros e0; simpl.
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
transport (fun y : A1 => h y = g2 c2) e0
  (transport (fun x : A2 => h (f1 b1) = x) e2
     ((p b1)^ @ ap f2 e1)) = (q c1)^ @ ap g2 e3
    refine (equiv_concat_l (transport_paths_Fl e0 _) _ oE _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
(ap h e0)^ @
transport (fun x : A2 => h (f1 b1) = x) e2
  ((p b1)^ @ ap f2 e1) = (q c1)^ @ ap g2 e3
    refine (equiv_concat_l (whiskerL (ap h e0)^ (transport_paths_r e2 _)) _ oE _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
(ap h e0)^ @ (((p b1)^ @ ap f2 e1) @ e2) =
(q c1)^ @ ap g2 e3
    refine (equiv_moveR_Vp _ _ _ oE _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
((p b1)^ @ ap f2 e1) @ e2 =
ap h e0 @ ((q c1)^ @ ap g2 e3)
    refine (equiv_concat_l (concat_pp_p _ _ _) _ oE _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
(p b1)^ @ (ap f2 e1 @ e2) =
ap h e0 @ ((q c1)^ @ ap g2 e3)
    refine (equiv_moveR_Vp _ _ _ oE _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
ap f2 e1 @ e2 =
p b1 @ (ap h e0 @ ((q c1)^ @ ap g2 e3))
    do 2 refine (equiv_concat_r (concat_pp_p _ _ _) _ oE _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
ap f2 e1 @ e2 =
((p b1 @ ap h e0) @ (q c1)^) @ ap g2 e3
    refine (equiv_moveL_pM _ _ _ oE _).
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
b2: B2
c2: C2
e2: f2 b2 = g2 c2
b1: B1
e1: k b1 = b2
c1: C1
e3: l c1 = c2
e0: f1 b1 = g1 c1
(p b1 @ ap h e0) @ (q c1)^ =
((ap f2 e1^)^ @ e2) @ ap g2 e3^ <~>
(ap f2 e1 @ e2) @ (ap g2 e3)^ =
(p b1 @ ap h e0) @ (q c1)^
    abstract (rewrite !ap_V, inv_V; exact (equiv_path_inverse _ _)).
  Defined.

End Functor_Pullback.

Section EquivPullback.
  Context {A B C f g A' B' C' f' g'}
          (eA : A <~> A') (eB : B <~> B') (eC : C <~> C')
          (p : f' o eB == eA o f) (q :  g' o eC == eA o g).

  Lemma equiv_pullback
    : Pullback f g <~> Pullback f' g'.
A, B, C: Type
f: B -> A
g: C -> A
A', B', C': Type
f': B' -> A'
g': C' -> A'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: f' o eB == eA o f
q: g' o eC == eA o g
Pullback f g <~> Pullback f' g'
  Proof.
A, B, C: Type
f: B -> A
g: C -> A
A', B', C': Type
f': B' -> A'
g': C' -> A'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: f' o eB == eA o f
q: g' o eC == eA o g
Pullback f g <~> Pullback f' g'
    unfold Pullback.
A, B, C: Type
f: B -> A
g: C -> A
A', B', C': Type
f': B' -> A'
g': C' -> A'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: f' o eB == eA o f
q: g' o eC == eA o g
{b : B & {c : C & f b = g c}} <~>
{b : B' & {c : C' & f' b = g' c}}
    apply (equiv_functor_sigma' eB); intro b.
A, B, C: Type
f: B -> A
g: C -> A
A', B', C': Type
f': B' -> A'
g': C' -> A'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: f' o eB == eA o f
q: g' o eC == eA o g
b: B
{c : C & f b = g c} <~> {c : C' & f' (eB b) = g' c}
    apply (equiv_functor_sigma' eC); intro c.
A, B, C: Type
f: B -> A
g: C -> A
A', B', C': Type
f': B' -> A'
g': C' -> A'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: f' o eB == eA o f
q: g' o eC == eA o g
b: B
c: C
f b = g c <~> f' (eB b) = g' (eC c)
    refine (equiv_concat_l (p _) _ oE _).
A, B, C: Type
f: B -> A
g: C -> A
A', B', C': Type
f': B' -> A'
g': C' -> A'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: f' o eB == eA o f
q: g' o eC == eA o g
b: B
c: C
f b = g c <~> eA (f b) = g' (eC c)
    refine (equiv_concat_r (q _)^ _ oE _).
A, B, C: Type
f: B -> A
g: C -> A
A', B', C': Type
f': B' -> A'
g': C' -> A'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: f' o eB == eA o f
q: g' o eC == eA o g
b: B
c: C
f b = g c <~> eA (f b) = eA (g c)
    exact (equiv_ap' eA _ _).
  Defined.

End EquivPullback.


(** Pullbacks commute with sigmas *)
Section PullbackSigma.

  Context
    {X Y Z : Type}
    {A : X -> Type} {B : Y -> Type} {C : Z -> Type}
    (f : Y -> X) (g : Z -> X)
    (r : forall x, B x -> A (f x))
    (s : forall x, C x -> A (g x)).

  Definition equiv_sigma_pullback
    : {p : Pullback f g & Pullback (transport A p.2.2 o r p.1) (s p.2.1)}
      <~> Pullback (functor_sigma f r) (functor_sigma g s).
X, Y, Z: Type
A: X -> Type
B: Y -> Type
C: Z -> Type
f: Y -> X
g: Z -> X
r: forall x : Y, B x -> A (f x)
s: forall x : Z, C x -> A (g x)
{p : Pullback f g &
Pullback (transport A (p.2).2 o r p.1) (s (p.2).1)} <~>
Pullback (functor_sigma f r) (functor_sigma g s)
  Proof.
X, Y, Z: Type
A: X -> Type
B: Y -> Type
C: Z -> Type
f: Y -> X
g: Z -> X
r: forall x : Y, B x -> A (f x)
s: forall x : Z, C x -> A (g x)
{p : Pullback f g &
Pullback (transport A (p.2).2 o r p.1) (s (p.2).1)} <~>
Pullback (functor_sigma f r) (functor_sigma g s)
    refine (equiv_functor_sigma_id (fun _ => equiv_functor_sigma_id _) oE _).
X, Y, Z: Type
A: X -> Type
B: Y -> Type
C: Z -> Type
f: Y -> X
g: Z -> X
r: forall x : Y, B x -> A (f x)
s: forall x : Z, C x -> A (g x)
y: {x : _ & B x}
forall a : {x : _ & C x},
?Goal a <~> functor_sigma f r y = functor_sigma g s a
X, Y, Z: Type
A: X -> Type
B: Y -> Type
C: Z -> Type
f: Y -> X
g: Z -> X
r: forall x : Y, B x -> A (f x)
s: forall x : Z, C x -> A (g x)
{p : Pullback f g &
Pullback
  (fun x : B p.1 => transport A (p.2).2 (r p.1 x))
  (s (p.2).1)} <~>
{H : {x : _ & B x} & {x : _ & ?Goal@{y:=H} x}}
    -
X, Y, Z: Type
A: X -> Type
B: Y -> Type
C: Z -> Type
f: Y -> X
g: Z -> X
r: forall x : Y, B x -> A (f x)
s: forall x : Z, C x -> A (g x)
y: {x : _ & B x}
forall a : {x : _ & C x},
?Goal a <~> functor_sigma f r y = functor_sigma g s a intros; rapply equiv_path_sigma.
    -
X, Y, Z: Type
A: X -> Type
B: Y -> Type
C: Z -> Type
f: Y -> X
g: Z -> X
r: forall x : Y, B x -> A (f x)
s: forall x : Z, C x -> A (g x)
{p : Pullback f g &
Pullback
  (fun x : B p.1 => transport A (p.2).2 (r p.1 x))
  (s (p.2).1)} <~>
{H : {x : _ & B x} &
{a : {x : _ & C x} &
{p : (functor_sigma f r H).1 = (functor_sigma g s a).1
&
transport A p (functor_sigma f r H).2 =
(functor_sigma g s a).2}}} make_equiv.
  Defined.

End PullbackSigma.

(** ** Paths in pullbacks *)

Definition equiv_path_pullback {A B C} (f : B -> A) (g : C -> A)
           (x y : Pullback f g)
  : { p : x.1 = y.1 & { q : x.2.1 = y.2.1 & PathSquare (ap f p) (ap g q) x.2.2 y.2.2 } }
      <~> (x = y).
A, B, C: Type
f: B -> A
g: C -> A
x, y: Pullback f g
{p : x.1 = y.1 &
{q : (x.2).1 = (y.2).1 &
PathSquare (ap f p) (ap g q) (x.2).2 (y.2).2}} <~>
x = y
Proof.
A, B, C: Type
f: B -> A
g: C -> A
x, y: Pullback f g
{p : x.1 = y.1 &
{q : (x.2).1 = (y.2).1 &
PathSquare (ap f p) (ap g q) (x.2).2 (y.2).2}} <~>
x = y
  revert y; rapply equiv_path_from_contr.
A, B, C: Type
f: B -> A
g: C -> A
x: Pullback f g
{p : x.1 = x.1 &
{q : (x.2).1 = (x.2).1 &
PathSquare (ap f p) (ap g q) (x.2).2 (x.2).2}}
A, B, C: Type
f: B -> A
g: C -> A
x: Pullback f g
Contr
  {y : Pullback f g &
  {p : x.1 = y.1 &
  {q : (x.2).1 = (y.2).1 &
  PathSquare (ap f p) (ap g q) (x.2).2 (y.2).2}}}
  {
A, B, C: Type
f: B -> A
g: C -> A
x: Pullback f g
{p : x.1 = x.1 &
{q : (x.2).1 = (x.2).1 &
PathSquare (ap f p) (ap g q) (x.2).2 (x.2).2}} exists idpath.
A, B, C: Type
f: B -> A
g: C -> A
x: Pullback f g
{q : (x.2).1 = (x.2).1 &
PathSquare (ap f 1) (ap g q) (x.2).2 (x.2).2} exists idpath.
A, B, C: Type
f: B -> A
g: C -> A
x: Pullback f g
PathSquare (ap f 1) (ap g 1) (x.2).2 (x.2).2
    cbn.
A, B, C: Type
f: B -> A
g: C -> A
x: Pullback f g
PathSquare 1 1 (x.2).2 (x.2).2 apply sq_refl_v. }
A, B, C: Type
f: B -> A
g: C -> A
x: Pullback f g
Contr
  {y : Pullback f g &
  {p : x.1 = y.1 &
  {q : (x.2).1 = (y.2).1 &
  PathSquare (ap f p) (ap g q) (x.2).2 (y.2).2}}}
  destruct x as [b [c p]]; unfold Pullback; cbn.
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
p: f b = g c
Contr
  {y : {b : B & {c : C & f b = g c}} &
  {p0 : b = y.1 &
  {q : c = (y.2).1 &
  PathSquare (ap f p0) (ap g q) p (y.2).2}}}
  contr_sigsig b (idpath b).
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
p: f b = g c
Contr
  {y : {c : C & f b = g c} &
  {q : c = ((b; y).2).1 &
  PathSquare (ap f 1) (ap g q) p ((b; y).2).2}}
  contr_sigsig c (idpath c).
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
p: f b = g c
Contr
  {y : f b = g c &
  PathSquare (ap f 1) (ap g 1) p ((b; c; y).2).2}
  cbn.
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
p: f b = g c
Contr {y : f b = g c & PathSquare 1 1 p y}
  rapply (contr_equiv' {p' : f b = g c & p = p'}).
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
p: f b = g c
{p' : f b = g c & p = p'} <~>
{y : f b = g c & PathSquare 1 1 p y}
  apply equiv_functor_sigma_id; intros p'.
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
p, p': f b = g c
p = p' <~> PathSquare 1 1 p p'
  exact sq_1G.
Defined.

(** Maps into pullbacks are determined by their composites with the projections, and a coherence.  This can also be proved directly.  With [Funext], we could also prove an equivalence analogous to [equiv_path_pullback_rec_hset] below.  Not sure of the best name for this version. *)
Definition pullback_homotopic {A B C D} {g : C -> D} {k : B -> D}
           (f h : A -> Pullback k g)
           (p1 : pullback_pr1 o f == pullback_pr1 o h)
           (p2 : pullback_pr2 o f == pullback_pr2 o h)
           (q : forall a, (ap k) (p1 a) @ (h a).2.2 = (f a).2.2 @ (ap g) (p2 a))
  : f == h.
A, B, C, D: Type
g: C -> D
k: B -> D
f, h: A -> Pullback k g
p1: pullback_pr1 o f == pullback_pr1 o h
p2: pullback_pr2 o f == pullback_pr2 o h
q: forall a : A,
ap k (p1 a) @ ((h a).2).2 =
((f a).2).2 @ ap g (p2 a)
f == h
Proof.
A, B, C, D: Type
g: C -> D
k: B -> D
f, h: A -> Pullback k g
p1: pullback_pr1 o f == pullback_pr1 o h
p2: pullback_pr2 o f == pullback_pr2 o h
q: forall a : A,
ap k (p1 a) @ ((h a).2).2 =
((f a).2).2 @ ap g (p2 a)
f == h
  intro a.
A, B, C, D: Type
g: C -> D
k: B -> D
f, h: A -> Pullback k g
p1: pullback_pr1 o f == pullback_pr1 o h
p2: pullback_pr2 o f == pullback_pr2 o h
q: forall a : A,
ap k (p1 a) @ ((h a).2).2 =
((f a).2).2 @ ap g (p2 a)
a: A
f a = h a
  apply equiv_path_pullback.
A, B, C, D: Type
g: C -> D
k: B -> D
f, h: A -> Pullback k g
p1: pullback_pr1 o f == pullback_pr1 o h
p2: pullback_pr2 o f == pullback_pr2 o h
q: forall a : A,
ap k (p1 a) @ ((h a).2).2 =
((f a).2).2 @ ap g (p2 a)
a: A
{p : (f a).1 = (h a).1 &
{q : ((f a).2).1 = ((h a).2).1 &
PathSquare (ap k p) (ap g q) ((f a).2).2 ((h a).2).2}}
  exists (p1 a).
A, B, C, D: Type
g: C -> D
k: B -> D
f, h: A -> Pullback k g
p1: pullback_pr1 o f == pullback_pr1 o h
p2: pullback_pr2 o f == pullback_pr2 o h
q: forall a : A,
ap k (p1 a) @ ((h a).2).2 =
((f a).2).2 @ ap g (p2 a)
a: A
{q : ((f a).2).1 = ((h a).2).1 &
PathSquare (ap k (p1 a)) (ap g q) ((f a).2).2
  ((h a).2).2}  exists (p2 a).
A, B, C, D: Type
g: C -> D
k: B -> D
f, h: A -> Pullback k g
p1: pullback_pr1 o f == pullback_pr1 o h
p2: pullback_pr2 o f == pullback_pr2 o h
q: forall a : A,
ap k (p1 a) @ ((h a).2).2 =
((f a).2).2 @ ap g (p2 a)
a: A
PathSquare (ap k (p1 a)) (ap g (p2 a)) ((f a).2).2
  ((h a).2).2
  apply sq_path, q.
Defined.

(** When [A] is a set, the [PathSquare] becomes trivial. *)
Definition equiv_path_pullback_hset {A B C} `{IsHSet A} (f : B -> A) (g : C -> A)
           (x y : Pullback f g)
  : (x.1 = y.1) * (x.2.1 = y.2.1) <~> (x = y).
A, B, C: Type
IsHSet0: IsHSet A
f: B -> A
g: C -> A
x, y: Pullback f g
(x.1 = y.1) * ((x.2).1 = (y.2).1) <~> x = y
Proof.
A, B, C: Type
IsHSet0: IsHSet A
f: B -> A
g: C -> A
x, y: Pullback f g
(x.1 = y.1) * ((x.2).1 = (y.2).1) <~> x = y
  refine (equiv_path_pullback f g x y oE _^-1%equiv).
A, B, C: Type
IsHSet0: IsHSet A
f: B -> A
g: C -> A
x, y: Pullback f g
{p : x.1 = y.1 &
{q : (x.2).1 = (y.2).1 &
PathSquare (ap f p) (ap g q) (x.2).2 (y.2).2}} <~>
(x.1 = y.1) * ((x.2).1 = (y.2).1)
  refine (_ oE equiv_sigma_prod (fun pq => PathSquare (ap f (fst pq)) (ap g (snd pq)) (x.2).2 (y.2).2)).
A, B, C: Type
IsHSet0: IsHSet A
f: B -> A
g: C -> A
x, y: Pullback f g
{pq : (x.1 = y.1) * ((x.2).1 = (y.2).1) &
PathSquare (ap f (fst pq)) (ap g (snd pq)) (x.2).2
  (y.2).2} <~> (x.1 = y.1) * ((x.2).1 = (y.2).1)
  rapply equiv_sigma_contr. (* Uses [istrunc_sq]. *)
Defined.

Lemma equiv_path_pullback_rec_hset `{Funext} {A X Y Z : Type} `{IsHSet Z}
      (f : X -> Z) (g : Y -> Z) (phi psi : A -> Pullback f g)
  : ((pullback_pr1 o phi == pullback_pr1 o psi) * (pullback_pr2 o phi == pullback_pr2 o psi))
      <~> (phi == psi).
H: Funext
A, X, Y, Z: Type
IsHSet0: IsHSet Z
f: X -> Z
g: Y -> Z
phi, psi: A -> Pullback f g
(pullback_pr1 o phi == pullback_pr1 o psi) *
(pullback_pr2 o phi == pullback_pr2 o psi) <~>
phi == psi
Proof.
H: Funext
A, X, Y, Z: Type
IsHSet0: IsHSet Z
f: X -> Z
g: Y -> Z
phi, psi: A -> Pullback f g
(pullback_pr1 o phi == pullback_pr1 o psi) *
(pullback_pr2 o phi == pullback_pr2 o psi) <~>
phi == psi
  refine (_ oE equiv_prod_coind _ _).
H: Funext
A, X, Y, Z: Type
IsHSet0: IsHSet Z
f: X -> Z
g: Y -> Z
phi, psi: A -> Pullback f g
(forall x : A,
 (pullback_pr1 (phi x) = pullback_pr1 (psi x)) *
 (pullback_pr2 (phi x) = pullback_pr2 (psi x))) <~>
phi == psi
  srapply equiv_functor_forall_id; intro a; cbn.
H: Funext
A, X, Y, Z: Type
IsHSet0: IsHSet Z
f: X -> Z
g: Y -> Z
phi, psi: A -> Pullback f g
a: A
(pullback_pr1 (phi a) = pullback_pr1 (psi a)) *
(pullback_pr2 (phi a) = pullback_pr2 (psi a)) <~>
phi a = psi a
  apply equiv_path_pullback_hset.
Defined.

(** The 3x3 Lemma *)

Section Pullback3x3.

  Context
    (A00 A02 A04 A20 A22 A24 A40 A42 A44 : Type)
    (f01 : A00 -> A02) (f03 : A04 -> A02)
    (f10 : A00 -> A20) (f12 : A02 -> A22) (f14 : A04 -> A24)
    (f21 : A20 -> A22) (f23 : A24 -> A22)
    (f30 : A40 -> A20) (f32 : A42 -> A22) (f34 : A44 -> A24)
    (f41 : A40 -> A42) (f43 : A44 -> A42)
    (H11 : f12 o f01 == f21 o f10) (H13 : f12 o f03 == f23 o f14)
    (H31 : f32 o f41 == f21 o f30) (H33 : f32 o f43 == f23 o f34).

  Let fX1 := functor_pullback f10 f30 f12 f32 f21 f01 f41 H11 H31.
  Let fX3 := functor_pullback f14 f34 f12 f32 f23 f03 f43 H13 H33.
  Let f1X := functor_pullback f01 f03 f21 f23 f12 f10 f14 (symmetry _ _ H11) (symmetry _ _ H13).
  Let f3X := functor_pullback f41 f43 f21 f23 f32 f30 f34 (symmetry _ _ H31) (symmetry _ _ H33).

  Theorem pullback3x3 : Pullback fX1 fX3 <~> Pullback f1X f3X.
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
Pullback fX1 fX3 <~> Pullback f1X f3X
  Proof.
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
Pullback fX1 fX3 <~> Pullback f1X f3X
    refine (_ oE _ oE _).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
?Goal0 <~> Pullback f1X f3X
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
?Goal <~> ?Goal0
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
Pullback fX1 fX3 <~> ?Goal
    1,3:do 2 (rapply equiv_functor_sigma_id; intro).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
?Goal0 a0 <~> f1X a = f3X a0
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f10 f30
a0: Pullback f14 f34
fX1 a = fX3 a0 <~> ?Goal1 a0
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
{a : Pullback f10 f30 & {x : _ & ?Goal1 x}} <~>
{a : Pullback f01 f03 & {x : _ & ?Goal0 x}}
    1:apply equiv_path_pullback.
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f10 f30
a0: Pullback f14 f34
fX1 a = fX3 a0 <~> ?Goal0 a0
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
{a : Pullback f10 f30 & {x : _ & ?Goal0 x}} <~>
{a : Pullback f01 f03 &
{a0 : Pullback f41 f43 &
{p : (f1X a).1 = (f3X a0).1 &
{q : ((f1X a).2).1 = ((f3X a0).2).1 &
PathSquare (ap f21 p) (ap f23 q) ((f1X a).2).2
  ((f3X a0).2).2}}}}
    1:symmetry; apply equiv_path_pullback.
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
{a : Pullback f10 f30 &
{a0 : Pullback f14 f34 &
{p : (fX1 a).1 = (fX3 a0).1 &
{q : ((fX1 a).2).1 = ((fX3 a0).2).1 &
PathSquare (ap f12 p) (ap f32 q) ((fX1 a).2).2
  ((fX3 a0).2).2}}}} <~>
{a : Pullback f01 f03 &
{a0 : Pullback f41 f43 &
{p : (f1X a).1 = (f3X a0).1 &
{q : ((f1X a).2).1 = ((f3X a0).2).1 &
PathSquare (ap f21 p) (ap f23 q) ((f1X a).2).2
  ((f3X a0).2).2}}}}
    refine (_ oE _).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
?Goal <~>
{a : Pullback f01 f03 &
{a0 : Pullback f41 f43 &
{p : (f1X a).1 = (f3X a0).1 &
{q : ((f1X a).2).1 = ((f3X a0).2).1 &
PathSquare (ap f21 p) (ap f23 q) ((f1X a).2).2
  ((f3X a0).2).2}}}}
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
{a : Pullback f10 f30 &
{a0 : Pullback f14 f34 &
{p : (fX1 a).1 = (fX3 a0).1 &
{q : ((fX1 a).2).1 = ((fX3 a0).2).1 &
PathSquare (ap f12 p) (ap f32 q) ((fX1 a).2).2
  ((fX3 a0).2).2}}}} <~> ?Goal
    {
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
?Goal <~>
{a : Pullback f01 f03 &
{a0 : Pullback f41 f43 &
{p : (f1X a).1 = (f3X a0).1 &
{q : ((f1X a).2).1 = ((f3X a0).2).1 &
PathSquare (ap f21 p) (ap f23 q) ((f1X a).2).2
  ((f3X a0).2).2}}}} do 4 (rapply equiv_functor_sigma_id; intro).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
a1: (f1X a).1 = (f3X a0).1
a2: ((f1X a).2).1 = ((f3X a0).2).1
?Goal0 a2 <~>
PathSquare (ap f21 a1) (ap f23 a2) ((f1X a).2).2
  ((f3X a0).2).2
      refine (sq_tr oE _).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
a1: (f1X a).1 = (f3X a0).1
a2: ((f1X a).2).1 = ((f3X a0).2).1
?Goal0 a2 <~>
PathSquare ((f1X a).2).2 ((f3X a0).2).2 (ap f21 a1)
  (ap f23 a2)
      refine (sq_move_14^-1 oE _).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
a1: (f1X a).1 = (f3X a0).1
a2: ((f1X a).2).1 = ((f3X a0).2).1
?Goal0 a2 <~>
PathSquare
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11 a.1 @
   ap f12 (a.2).2) ((f3X a0).2).2 (ap f21 a1)
  ((symmetry (fun x : A04 => f12 (f03 x))
      (fun x : A04 => f23 (f14 x)) H13 (a.2).1)^ @
   ap f23 a2)
      refine (sq_move_31 oE _).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
a1: (f1X a).1 = (f3X a0).1
a2: ((f1X a).2).1 = ((f3X a0).2).1
?Goal0 a2 <~>
PathSquare (ap f12 (a.2).2) ((f3X a0).2).2
  ((symmetry (fun x : A00 => f12 (f01 x))
      (fun x : A00 => f21 (f10 x)) H11 a.1)^ @
   ap f21 a1)
  ((symmetry (fun x : A04 => f12 (f03 x))
      (fun x : A04 => f23 (f14 x)) H13 (a.2).1)^ @
   ap f23 a2)
      refine (sq_move_24^-1 oE _).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
a1: (f1X a).1 = (f3X a0).1
a2: ((f1X a).2).1 = ((f3X a0).2).1
?Goal0 a2 <~>
PathSquare (ap f12 (a.2).2)
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31 a0.1 @
   ap f32 (a0.2).2)
  ((symmetry (fun x : A00 => f12 (f01 x))
      (fun x : A00 => f21 (f10 x)) H11 a.1)^ @
   ap f21 a1)
  (((symmetry (fun x : A04 => f12 (f03 x))
       (fun x : A04 => f23 (f14 x)) H13 (a.2).1)^ @
    ap f23 a2) @
   symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33 (a0.2).1)
      refine (sq_move_23^-1 oE _).
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
a1: (f1X a).1 = (f3X a0).1
a2: ((f1X a).2).1 = ((f3X a0).2).1
?Goal0 a2 <~>
PathSquare (ap f12 (a.2).2) (ap f32 (a0.2).2)
  (((symmetry (fun x : A00 => f12 (f01 x))
       (fun x : A00 => f21 (f10 x)) H11 a.1)^ @
    ap f21 a1) @
   symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31 a0.1)
  (((symmetry (fun x : A04 => f12 (f03 x))
       (fun x : A04 => f23 (f14 x)) H13 (a.2).1)^ @
    ap f23 a2) @
   symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33 (a0.2).1)
      rewrite 2 inv_V.
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
a: Pullback f01 f03
a0: Pullback f41 f43
a1: (f1X a).1 = (f3X a0).1
a2: ((f1X a).2).1 = ((f3X a0).2).1
?Goal0 a2 <~>
PathSquare (ap f12 (a.2).2) (ap f32 (a0.2).2)
  ((H11 a.1 @ ap f21 a1) @
   symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31 a0.1)
  ((H13 (a.2).1 @ ap f23 a2) @
   symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33 (a0.2).1)
      reflexivity. }
A00, A02, A04, A20, A22, A24, A40, A42, A44: Type
f01: A00 -> A02
f03: A04 -> A02
f10: A00 -> A20
f12: A02 -> A22
f14: A04 -> A24
f21: A20 -> A22
f23: A24 -> A22
f30: A40 -> A20
f32: A42 -> A22
f34: A44 -> A24
f41: A40 -> A42
f43: A44 -> A42
H11: f12 o f01 == f21 o f10
H13: f12 o f03 == f23 o f14
H31: f32 o f41 == f21 o f30
H33: f32 o f43 == f23 o f34
fX1:= functor_pullback f10 f30 f12 f32 f21 f01 f41 H11
  H31: Pullback f10 f30 -> Pullback f12 f32
fX3:= functor_pullback f14 f34 f12 f32 f23 f03 f43 H13
  H33: Pullback f14 f34 -> Pullback f12 f32
f1X:= functor_pullback f01 f03 f21 f23 f12 f10 f14
  (symmetry (fun x : A00 => f12 (f01 x))
     (fun x : A00 => f21 (f10 x)) H11)
  (symmetry (fun x : A04 => f12 (f03 x))
     (fun x : A04 => f23 (f14 x)) H13): Pullback f01 f03 -> Pullback f21 f23
f3X:= functor_pullback f41 f43 f21 f23 f32 f30 f34
  (symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31)
  (symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33): Pullback f41 f43 -> Pullback f21 f23
{a : Pullback f10 f30 &
{a0 : Pullback f14 f34 &
{p : (fX1 a).1 = (fX3 a0).1 &
{q : ((fX1 a).2).1 = ((fX3 a0).2).1 &
PathSquare (ap f12 p) (ap f32 q) ((fX1 a).2).2
  ((fX3 a0).2).2}}}} <~>
{a : Pullback f01 f03 &
{a0 : Pullback f41 f43 &
{a1 : (f1X a).1 = (f3X a0).1 &
{a2 : ((f1X a).2).1 = ((f3X a0).2).1 &
PathSquare (ap f12 (a.2).2) (ap f32 (a0.2).2)
  ((H11 a.1 @ ap f21 a1) @
   symmetry (fun x : A40 => f32 (f41 x))
     (fun x : A40 => f21 (f30 x)) H31 a0.1)
  ((H13 (a.2).1 @ ap f23 a2) @
   symmetry (fun x : A44 => f32 (f43 x))
     (fun x : A44 => f23 (f34 x)) H33 (a0.2).1)}}}}
    make_equiv.
  Defined.

End Pullback3x3.

(** Pasting for pullbacks (or 2-pullbacks lemma) *)

Section Pasting.

  (** Given the following diagram where the right square is a pullback square, then the outer square is a pullback square if and only if the left square is a pullback. *)
  (* A --k--> B --l--> C
     |    //  |    //  |
     f  comm  g  comm  h
     |  //    |  //    |
     V //     V //     V
     X --i--> Y --j--> Z *)
  Context
    {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) {e1 : IsPullback K}.

  Definition ispullback_pasting_left
    : IsPullback (comm_square_comp' H K) -> IsPullback H.
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
e1: IsPullback K
IsPullback (comm_square_comp' H K) -> IsPullback H
  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
e1: IsPullback K
IsPullback (comm_square_comp' H K) -> IsPullback H
    intro e2.
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
IsPullback H
    apply ispullback_isequiv_functor_hfiber.
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
forall b : X, IsEquiv (functor_hfiber H b)
    intro b.
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
IsEquiv (functor_hfiber H b)
    pose (e1' := isequiv_functor_hfiber_ispullback _ e1 (i b)).
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
IsEquiv (functor_hfiber H b)
    pose (e2' := isequiv_functor_hfiber_ispullback _ e2 b).
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv (functor_hfiber H b)
    snapply isequiv_commsq'.
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
Type
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
Type
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
?C -> ?D
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
hfiber f b -> ?C
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
hfiber g (i b) -> ?D
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
?g o ?h == ?k o functor_hfiber H b
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv ?g
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv ?h
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv ?k
    7: apply isequiv_idmap.
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
Type
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
hfiber f b -> ?C
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
hfiber g (i b) -> ?C
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
idmap o ?h == ?k o functor_hfiber H b
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv ?h
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv ?k
    4: exact (functor_hfiber_compose H K b).
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv
  (fun u : {x : A & f x = b} =>
   ((fun x : A => l (k x)) u.1;
   (fun (a : A) (e : (fun x : A => f x = b) a) =>
    (comm_square_comp' H K a)^ @
    ap (fun x : X => j (i x)) e) u.1 u.2))
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
e1: IsPullback K
e2: IsPullback (comm_square_comp' H K)
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback
  (comm_square_comp' H K) e2 b: IsEquiv (functor_hfiber (comm_square_comp' H K) b)
IsEquiv (functor_hfiber K (i b))
    1,2: exact _.
  Defined.

  Definition ispullback_pasting_outer
    : IsPullback H -> IsPullback (comm_square_comp' H K).
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
e1: IsPullback K
IsPullback H -> IsPullback (comm_square_comp' H K)
  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
e1: IsPullback K
IsPullback H -> IsPullback (comm_square_comp' H K)
    intro e2.
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
e1: IsPullback K
e2: IsPullback H
IsPullback (comm_square_comp' H K)
    apply ispullback_isequiv_functor_hfiber.
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
e1: IsPullback K
e2: IsPullback H
forall b : X,
IsEquiv (functor_hfiber (comm_square_comp' H K) b)
    intro b.
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
e1: IsPullback K
e2: IsPullback H
b: X
IsEquiv (functor_hfiber (comm_square_comp' H K) b)
    pose (e1' := isequiv_functor_hfiber_ispullback _ e1 (i b)).
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
IsEquiv (functor_hfiber (comm_square_comp' H K) b)
    pose (e2' := isequiv_functor_hfiber_ispullback _ e2 b).
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv (functor_hfiber (comm_square_comp' H K) b)
    snapply isequiv_commsq'.
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
Type
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
Type
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
?C -> ?D
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
hfiber f b -> ?C
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
hfiber h (j (i b)) -> ?D
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
?g o ?h ==
?k o functor_hfiber (comm_square_comp' H K) b
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv ?g
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv ?h
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv ?k
    9: apply isequiv_idmap.
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
Type
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
?C -> hfiber h (j (i b))
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
hfiber f b -> ?C
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
?g o ?h ==
idmap o functor_hfiber (comm_square_comp' H K) b
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv ?g
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv ?h
    4: symmetry; exact (functor_hfiber_compose H K b).
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv (functor_hfiber K (i b))
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
e1: IsPullback K
e2: IsPullback H
b: X
e1':= isequiv_functor_hfiber_ispullback K e1 (i b): IsEquiv (functor_hfiber K (i b))
e2':= isequiv_functor_hfiber_ispullback H e2 b: IsEquiv (functor_hfiber H b)
IsEquiv (functor_hfiber H b)
    1,2: exact _.
  Defined.

End Pasting.