Lemma pullback_is_preserved_after_lift : isPullback Fq. Proof. use (Pullback_iso_squares _ (Fpb _ _ _ _ _ _ _ _ fully_faithful_inv_hom_of_pullback_diagram_commutes (Pullbacks.p_func fully_faithful_inv_hom_of_pullback_diagram_commutes) fully_faithful_inv_hom_of_pullback_is_pullback )). - exact (z_iso_comp (functor_on_z_iso H (z_iso_inv i1)) (_ ,, pr2 α _)). - exact (z_iso_comp (functor_on_z_iso H (z_iso_inv i2)) (_ ,, pr2 α _)). - exact (z_iso_comp (functor_on_z_iso H (z_iso_inv i')) (_ ,, pr2 α _)). - exact (z_iso_comp (functor_on_z_iso H (z_iso_inv i)) (_ ,, pr2 α _)). - exact images_of_fully_faithful_inv_hom_of_leg_commute₀. - exact images_of_fully_faithful_inv_hom_of_leg_commute₁. - exact images_of_fully_faithful_inv_hom_of_first_projection_commute. - exact images_of_fully_faithful_inv_hom_of_second_projection_commute. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.WeakEquivalences.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Pullbacks. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Pullbacks.