Definition total_set_category_pb_ump_2_cell_data : nat_trans_data φ₁ φ₂. Proof. refine (λ x, δ₁ x ,, _). 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). - apply α_inv_α_iso. Defined.
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. End PullbackFromTotal.