Timings for IsPullback.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-unimath.dev/./UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-unimath.dev/./UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.timing
(*******************************************************************************
Pullbacks from the Grothendieck construction
We show that the following square is a pullback square
∫ G₁ ⟶ ∫ G₂
| |
V V
C₁ ⟶ C₂
*******************************************************************************)
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.DisplayedCats.StreetOpFibration.
Require Import UniMath.CategoryTheory.categories.CategoryOfSetCategories.
Require Import UniMath.CategoryTheory.GrothendieckConstruction.TotalCategory.
Require Import UniMath.CategoryTheory.GrothendieckConstruction.Projection.
Require Import UniMath.CategoryTheory.GrothendieckConstruction.IsosInTotal.
Section PullbackFromTotal.
Context {C₁ C₂ : setcategory}
{F : C₁ ⟶ C₂}
{G₁ : C₁ ⟶ cat_of_setcategory}
{G₂ : C₂ ⟶ cat_of_setcategory}
(α : G₁ ⟹ F ∙ G₂)
(Hα : is_nat_z_iso α).
Let αiso : nat_z_iso G₁ (F ∙ G₂) := α ,, Hα.
Let αinv : F ∙ G₂ ⟹ G₁ := nat_z_iso_inv αiso.
Local Lemma α_iso_α_inv
(x : C₁)
(y : pr1 (G₂ (F x)))
: pr1 (α x) (pr1 (αinv x) y) = y.
exact (maponpaths
(λ z, pr11 z y)
(z_iso_after_z_iso_inv
(nat_z_iso_pointwise_z_iso αiso x))).
Local Lemma α_iso_α_inv_on_mor
(x : C₁)
{y₁ y₂ : pr1 (G₂ (F x))}
(f : y₁ --> y₂)
: # (pr1 (α x)) (# (pr1 (αinv x)) f)
=
idtoiso (α_iso_α_inv x y₁)
· f
· idtoiso (!(α_iso_α_inv x y₂)).
refine (from_eq_cat_of_setcategory
(z_iso_after_z_iso_inv
(nat_z_iso_pointwise_z_iso αiso x)) f @ _) ; cbn.
apply setcategory_eq_idtoiso_comp.
Local Lemma α_inv_α_iso
(x : C₁)
(y : pr1 (G₁ x))
: pr1 (αinv x) (pr1 (α x) y) = y.
exact (maponpaths
(λ z, pr11 z y)
(z_iso_inv_after_z_iso
(nat_z_iso_pointwise_z_iso αiso x))).
Local Lemma α_inv_α_iso_on_mor
(x : C₁)
{y₁ y₂ : pr1 (G₁ x)}
(f : y₁ --> y₂)
: # (pr1 (αinv x)) (# (pr1 (α x)) f)
=
idtoiso (α_inv_α_iso x y₁)
· f
· idtoiso (!(α_inv_α_iso x y₂)).
refine (from_eq_cat_of_setcategory
(z_iso_inv_after_z_iso
(nat_z_iso_pointwise_z_iso αiso x)) f @ _) ; cbn.
apply setcategory_eq_idtoiso_comp.
Context {C₀ : setcategory}
(P₁ : C₀ ⟶ C₁)
(P₂ : C₀ ⟶ total_setcategory_of_set_functor G₂)
(β : P₁ ∙ F ⟹ P₂ ∙ pr1_total_category_of_set_functor G₂)
(Hβ : is_nat_z_iso β).
Definition total_set_category_pb_ump_1_mor_eq
{x y : C₀}
(f : x --> y)
: pr1 (# G₁ (# P₁ f)) ((pr11 (αinv (P₁ x))) ((pr11 (# G₂ (pr1 (Hβ x)))) (pr2 (P₂ x))))
=
pr1 (αinv (P₁ y)) (pr1 (# G₂ (pr1 (Hβ y))) (pr1 (# G₂ (pr1 (# P₂ f))) (pr2 (P₂ x)))).
pose (maponpaths
(λ z, pr11 z ((pr11 (# G₂ (pr1 (Hβ x)))) (pr2 (P₂ x))))
(nat_trans_ax αinv _ _ (#P₁ f)))
as p.
refine (maponpaths
(λ z, pr11 z (pr2 (P₂ x)))
(!(functor_comp G₂ (pr1 (Hβ x)) (# F (# P₁ f)))) @ _).
refine (!(maponpaths
(λ z, pr1 (# G₂ z) (pr2 (P₂ x)))
(nat_trans_ax (nat_z_iso_inv (β ,, Hβ)) _ _ f)) @ _).
exact (maponpaths
(λ z, pr11 z (pr2 (P₂ x)))
(functor_comp G₂ _ _)).
Definition total_set_category_pb_ump_1_mor_data
: functor_data
C₀
(total_setcategory_of_set_functor G₁).
apply (# G₂ (pr1 (Hβ x))).
refine (λ x y f,
#P₁ f
,,
_ · #(pr1 (αinv (P₁ y))) (# (pr1 (# G₂ (pr1 (Hβ y)))) (pr2 (# P₂ f)))).
exact (total_set_category_pb_ump_1_mor_eq f).
Definition total_set_category_pb_ump_1_mor_is_functor
: is_functor total_set_category_pb_ump_1_mor_data.
use eq_mor_category_of_set_functor.
exact (eq_mor_category_of_set_functor_pr2 (functor_id P₂ x)).
apply (pr1_idtoiso_concat
_
(eq_in_set_fiber (functor_id G₂ _) _)).
apply (pr1_maponpaths_idtoiso (# G₂ (pr1 (Hβ x)))).
apply (pr1_maponpaths_idtoiso (αinv (P₁ x))).
apply (pr1_idtoiso_concat (total_set_category_pb_ump_1_mor_eq _)).
apply (pr1_idtoiso_concat
_
(eq_in_set_fiber (functor_id G₁ (P₁ x)) _)).
apply setcategory_eq_idtoiso.
use eq_mor_category_of_set_functor.
exact (eq_mor_category_of_set_functor_pr2 (functor_comp P₂ f g)).
refine (functor_comp _ _ _ @ _).
refine (functor_comp _ _ _ @ _).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₂ (pr1 (Hβ z)))).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (P₁ z))).
refine (assoc _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₂ (pr1 (Hβ z)))).
apply (pr1_maponpaths_idtoiso (αinv (P₁ z))).
apply (pr1_idtoiso_concat (total_set_category_pb_ump_1_mor_eq (f · g))).
apply (pr1_idtoiso_concat (total_set_category_pb_ump_1_mor_eq (f · g) @ _)).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₁ (# P₁ g))).
refine (assoc _ _ _ @ _).
apply (pr1_idtoiso_concat
_
(eq_in_set_fiber (functor_comp G₁ (# P₁ f) (# P₁ g)) _)).
apply (pr1_idtoiso_concat
(_ @ eq_in_set_fiber (functor_comp G₁ (# P₁ f) (# P₁ g)) _)).
exact (from_eq_cat_of_setcategory
(!(nat_trans_ax αinv _ _ (# P₁ g)))
(# (pr1 (# G₂ (pr1 (Hβ y)))) (pr2 (# P₂ f)))).
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_idtoiso_concat
((_ @ eq_in_set_fiber (functor_comp G₁ (# P₁ f) (# P₁ g)) _) @ _)).
refine (assoc' _ _ _ @ _).
apply (pr1_idtoiso_concat _ (total_set_category_pb_ump_1_mor_eq g)).
exact (from_eq_cat_of_setcategory
(!(functor_comp G₂ (pr1 (Hβ y)) (# F (# P₁ g)))
@ maponpaths
(λ q, # G₂ q)
(!(nat_trans_ax (nat_z_iso_inv (β ,, Hβ)) _ _ g))
@ functor_comp G₂ _ _)
(pr2 (# P₂ f))).
refine (functor_comp _ _ _ @ _).
do 2 (refine (assoc _ _ _ @ _) ; apply maponpaths_2).
apply (pr1_maponpaths_idtoiso (αinv (P₁ z))).
apply (pr1_idtoiso_concat
(((_ @ eq_in_set_fiber (functor_comp G₁ _ _) _) @ _) @ _)).
do 2 refine (assoc' _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (P₁ z))).
apply (pr1_idtoiso_concat
_
(_ @ total_set_category_pb_ump_1_mor_eq g)).
apply setcategory_refl_idtoiso.
apply setcategory_eq_idtoiso.
Definition total_set_category_pb_ump_1_mor
: C₀ ⟶ total_setcategory_of_set_functor G₁.
exact total_set_category_pb_ump_1_mor_data.
exact total_set_category_pb_ump_1_mor_is_functor.
Definition total_set_category_pb_ump_1_mor_pr1
: total_set_category_pb_ump_1_mor ∙ pr1_total_category_of_set_functor G₁
⟹
P₁.
abstract
(intros x y f ; cbn ;
rewrite id_left, id_right ;
apply idpath).
Definition total_set_category_pb_ump_1_mor_pr1_is_nat_z_iso
: is_nat_z_iso total_set_category_pb_ump_1_mor_pr1.
apply is_z_isomorphism_identity.
Definition total_set_category_pb_ump_1_mor_pr2_eq
(x : C₀)
: pr1 (# G₂ (β x))
(pr1 (pr1 α (P₁ x))
((pr11 (αinv (P₁ x)))
((pr11 (# G₂ (pr1 (Hβ x))))
(pr2 (P₂ x)))))
=
pr2 (P₂ x).
exact (maponpaths
(λ z, pr11 z (pr2 (P₂ x)))
(!(functor_comp G₂ (pr1 (Hβ x)) (β x)))).
exact (z_iso_after_z_iso_inv (_ ,, Hβ x)).
exact (maponpaths
(λ z, pr11 z (pr2 (P₂ x)))
(functor_id G₂ _)).
Definition total_set_category_pb_ump_1_mor_pr2_data
: nat_trans_data
(total_set_category_pb_ump_1_mor ∙ functor_total_category_of_set_functor F α)
P₂.
apply total_set_category_pb_ump_1_mor_pr2_eq.
Definition total_set_category_pb_ump_1_mor_pr2_is_nat_trans
: is_nat_trans
_ _
total_set_category_pb_ump_1_mor_pr2_data.
use eq_mor_category_of_set_functor.
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (α (P₁ y))).
apply α_iso_α_inv_on_mor.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_idtoiso_concat
(maponpaths
(pr11 (α (P₁ y)))
(total_set_category_pb_ump_1_mor_eq f))).
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_idtoiso_concat
_
(maponpaths
(pr11 (α (P₁ y)))
(total_set_category_pb_ump_1_mor_eq f) @ _)).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₂ (β y))).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₂ (β y))).
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_idtoiso_concat
(eq_in_set_fiber (functor_comp G₂ _ _) _)).
do 2 refine (assoc' _ _ _ @ _).
apply (pr1_idtoiso_concat
_
(total_set_category_pb_ump_1_mor_pr2_eq y)).
exact (from_eq_cat_of_setcategory
((!functor_comp G₂ (pr1 (Hβ y)) (β y))
@ maponpaths
(λ z, # G₂ z)
(z_iso_after_z_iso_inv (_ ,, Hβ y))
@ functor_id G₂ _)
(pr2 (# P₂ f))).
do 2 refine (assoc' _ _ _ @ _).
apply (pr1_idtoiso_concat
_
(_ @ total_set_category_pb_ump_1_mor_pr2_eq y)).
do 2 refine (assoc _ _ _ @ _).
apply (pr1_idtoiso_concat
(eq_in_set_fiber (functor_comp G₂ _ _) _ @ _)).
apply setcategory_refl_idtoiso.
refine (_ @ assoc' _ _ _).
apply (pr1_maponpaths_idtoiso (# G₂ (pr1 (# P₂ f)))).
apply (pr1_idtoiso_concat
(eq_in_set_fiber (functor_comp G₂ _ _) _)).
apply (pr1_idtoiso_concat
_
(eq_in_set_fiber (functor_comp G₂ _ _) _ @ _)).
apply setcategory_eq_idtoiso.
Definition total_set_category_pb_ump_1_mor_pr2
: total_set_category_pb_ump_1_mor ∙ functor_total_category_of_set_functor F α
⟹
P₂.
exact total_set_category_pb_ump_1_mor_pr2_data.
exact total_set_category_pb_ump_1_mor_pr2_is_nat_trans.
Definition total_set_category_pb_ump_1_mor_pr2_is_nat_z_iso_eq
(x : C₀)
: pr1 (# G₂ (pr1 (Hβ x))) (pr2 (P₂ x))
=
pr1 (pr1 α (P₁ x))
((pr11 (αinv (P₁ x)))
((pr11 (# G₂ (pr1 (Hβ x)))) (pr2 (P₂ x)))).
Definition total_set_category_pb_ump_1_mor_pr2_is_nat_z_iso
: is_nat_z_iso total_set_category_pb_ump_1_mor_pr2.
use is_z_iso_total_setcategory_of_set_functor.
exact (idtoiso (total_set_category_pb_ump_1_mor_pr2_is_nat_z_iso_eq x)).
abstract
(cbn ;
etrans ;
[ apply maponpaths_2 ;
refine (!_) ;
apply (pr1_maponpaths_idtoiso (# G₂ (pr1 (Hβ x))))
| ] ;
etrans ;
[ refine (!_) ;
apply (pr1_idtoiso_concat
_
(total_set_category_pb_ump_1_mor_pr2_is_nat_z_iso_eq x))
| ] ;
apply setcategory_eq_idtoiso).
abstract
(cbn ;
etrans ;
[ apply maponpaths_2 ;
refine (!_) ;
apply (pr1_maponpaths_idtoiso (# G₂ (β x)))
| ] ;
etrans ;
[ refine (!_) ;
apply (pr1_idtoiso_concat
_
(total_set_category_pb_ump_1_mor_pr2_eq x))
| ] ;
apply setcategory_eq_idtoiso).
Context {C₀ : setcategory}
{φ₁ φ₂ : pr1 C₀ ⟶ total_setcategory_of_set_functor G₁}
(δ₁ : φ₁ ∙ pr1_total_category_of_set_functor G₁
⟹
φ₂ ∙ pr1_total_category_of_set_functor G₁)
(δ₂ : φ₁ ∙ functor_total_category_of_set_functor F α
⟹
φ₂ ∙ functor_total_category_of_set_functor F α)
(q : ∏ (x : C₀), pr1 (δ₂ x) = # F (δ₁ x)).
Definition total_set_category_pb_ump_2_unique
: isaprop
(∑ (γ : φ₁ ⟹ φ₂),
post_whisker γ (pr1_total_category_of_set_functor G₁) = δ₁
×
post_whisker γ (functor_total_category_of_set_functor F α) = δ₂).
use isapropdirprod ; apply isaset_nat_trans ; apply homset_property.
use eq_mor_category_of_set_functor.
exact (nat_trans_eq_pointwise (pr12 ζ) x @ !(nat_trans_eq_pointwise (pr12 ξ) x)).
assert (p := maponpaths
(λ z, #(pr1 (αinv (pr1 (φ₂ x)))) z)
(eq_mor_category_of_set_functor_pr2
(nat_trans_eq_pointwise (pr22 ζ) x
@ !(nat_trans_eq_pointwise (pr22 ξ) x)))).
assert (pr1 (# G₁ (pr1 (pr1 ζ x))) (pr2 (φ₁ x))
=
pr1 (αinv (pr1 (φ₂ x)))
(pr1 (# G₂ (# F (pr1 ((pr11 ζ) x))))
(pr1 (pr1 α (pr1 (φ₁ x))) (pr2 (φ₁ x)))))
as X.
pose (maponpaths
(λ z, pr11 z (pr1 (pr1 α (pr1 (φ₁ x))) (pr2 (φ₁ x))))
(nat_trans_ax αinv _ _ (pr1 (pr11 ζ x))))
as r.
simple refine (_
@ maponpaths
(λ z, idtoiso X · z · idtoiso (α_inv_α_iso _ _))
p
@ _).
refine (functor_comp _ _ _ @ _).
apply α_inv_α_iso_on_mor.
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ x)))).
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
refine (assoc' _ _ _ @ _).
apply pr1_idtoiso_concat.
apply setcategory_refl_idtoiso.
apply setcategory_refl_idtoiso.
refine (functor_comp _ _ _ @ _).
refine (functor_comp _ _ _ @ _).
apply α_inv_α_iso_on_mor.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ x)))).
apply pr1_idtoiso_concat.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ x)))).
apply pr1_idtoiso_concat.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
do 2 refine (assoc' _ _ _ @ _).
apply pr1_idtoiso_concat.
apply setcategory_refl_idtoiso.
apply setcategory_eq_idtoiso.
Definition total_set_category_pb_ump_2_cell_data
: nat_trans_data φ₁ φ₂.
refine (idtoiso _ · # (pr1 (αinv (pr1 (φ₂ x)))) (pr2 (δ₂ x)) · idtoiso _).
abstract
(rewrite q ;
cbn -[αinv] ;
pose (maponpaths (λ z, pr11 z (pr2 (φ₁ x))) (nat_trans_ax α _ _ (δ₁ x))) as p ;
cbn in p ;
refine (!_) ;
etrans ;
[ apply maponpaths ;
exact (!p)
| ] ;
apply α_inv_α_iso).
Definition total_set_category_pb_ump_2_cell_is_nat_trans
: is_nat_trans φ₁ φ₂ total_set_category_pb_ump_2_cell_data.
use eq_mor_category_of_set_functor.
exact (nat_trans_ax δ₁ _ _ f).
apply (pr1_idtoiso_concat
_
(eq_in_set_fiber (functor_comp G₁ _ _) _)).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₁ (pr1 (# φ₂ f)))).
apply (pr1_idtoiso_concat
(_ @ eq_in_set_fiber (functor_comp G₁ _ _) _)).
exact (from_eq_cat_of_setcategory
(!(nat_trans_ax αinv _ _ (pr1 (# φ₂ f))))
(pr2 (δ₂ x))).
refine (assoc' _ _ _ @ _).
refine (assoc' _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₁ (pr1 (# φ₂ f)))).
apply (pr1_idtoiso_concat
_
(maponpaths (λ z, pr1 (# G₁ (pr1 (# φ₂ f))) z) _)).
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_idtoiso_concat
(_ @ maponpaths (λ z, pr1 (# G₁ (pr1 (# φ₂ f))) z) _)).
pose (maponpaths
(λ z, # (pr1 (αinv (pr1 (φ₂ y)))) z)
(eq_mor_category_of_set_functor_pr2
(nat_trans_ax δ₂ _ _ f)))
as p.
assert (pr1 (# G₁ (pr1 (# φ₁ f) · δ₁ y)) (pr2 (φ₁ x))
=
pr1 (αinv (pr1 (φ₂ y)))
(pr1 (# G₂ (# F (pr1 (# φ₁ f)) · pr1 (δ₂ y)))
(pr1 (pr1 α (pr1 (φ₁ x)))
(pr2 (φ₁ x)))))
as X1.
apply (maponpaths
(λ z, pr11 z (pr1 (pr1 α (pr1 (φ₁ x))) (pr2 (φ₁ x))))
(nat_trans_ax αinv _ _ (pr1 (# φ₁ f) · δ₁ y))).
simple refine (_
@ maponpaths
(λ z, idtoiso X1 · z · idtoiso (α_inv_α_iso _ _))
(!p)
@ _).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ y)))).
refine (functor_comp _ _ _ @ _).
refine (functor_comp _ _ _ @ _).
apply α_inv_α_iso_on_mor.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ y)))).
apply pr1_idtoiso_concat.
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ y)))).
do 3 refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
apply pr1_idtoiso_concat.
do 3 refine (assoc' _ _ _ @ _).
apply pr1_idtoiso_concat.
apply setcategory_refl_idtoiso.
do 2 refine (assoc _ _ _ @ _).
apply setcategory_eq_idtoiso_comp.
refine (functor_comp _ _ _ @ _).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ y)))).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₂ (pr1 (δ₂ y)))).
refine (functor_comp _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (αinv (pr1 (φ₂ y)))).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
exact (from_eq_cat_of_setcategory
(maponpaths (λ z, #G₂ z) (q y))
(# (pr1 (α (pr1 (φ₁ y)))) (pr2 (# φ₁ f)))).
refine (functor_comp _ _ _ @ _).
apply pr1_maponpaths_idtoiso.
refine (functor_comp _ _ _ @ _).
apply pr1_maponpaths_idtoiso.
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
apply (from_eq_cat_of_setcategory
(nat_trans_ax αinv _ _(δ₁ y))
(# (pr1 (α (pr1 (φ₁ y)))) (pr2 (# φ₁ f)))).
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply pr1_idtoiso_concat.
refine (assoc' _ _ _ @ _).
apply pr1_idtoiso_concat.
apply α_inv_α_iso_on_mor.
refine (functor_comp _ _ _ @ _).
refine (assoc _ _ _ @ _).
refine (assoc _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₁ (δ₁ y))).
apply pr1_idtoiso_concat.
refine (assoc' _ _ _ @ _).
apply (pr1_maponpaths_idtoiso (# G₁ (δ₁ y))).
apply pr1_idtoiso_concat.
apply setcategory_eq_idtoiso_comp.
Definition total_set_category_pb_ump_2_cell
: φ₁ ⟹ φ₂.
exact total_set_category_pb_ump_2_cell_data.
exact total_set_category_pb_ump_2_cell_is_nat_trans.
Definition total_set_category_pb_ump_2_pr1
: post_whisker
total_set_category_pb_ump_2_cell
(pr1_total_category_of_set_functor G₁)
=
δ₁.
Definition total_set_category_pb_ump_2_pr2
: post_whisker
total_set_category_pb_ump_2_cell
(functor_total_category_of_set_functor F α)
=
δ₂.
use eq_mor_category_of_set_functor.
refine (functor_comp _ _ _ @ _).
refine (functor_comp _ _ _ @ _).
apply α_iso_α_inv_on_mor.
apply (pr1_maponpaths_idtoiso (α (pr1 (φ₂ x)))).
apply pr1_idtoiso_concat.
apply (pr1_maponpaths_idtoiso (α (pr1 (φ₂ x)))).
apply (pr1_idtoiso_concat
(functor_total_category_of_set_functor_eq
F α
(total_set_category_pb_ump_2_cell_data x))).
apply (pr1_idtoiso_concat
(functor_total_category_of_set_functor_eq
F α
(total_set_category_pb_ump_2_cell_data x) @ _)).
apply setcategory_refl_idtoiso.
apply setcategory_eq_idtoiso.