Lemma fully_faithful_inv_hom_of_pullback_is_pullback : isPullback fully_faithful_inv_hom_of_pullback_diagram_commutes. Proof. use (weak_equiv_reflects_pullbacks Gw). use (Pullback_iso_squares q ispby). - exact i1. - exact i2. - exact i'. - exact i. - exact inv_of_pullback_leg_fy_commutes_with_image_modulo_isos. - exact inv_of_pullback_leg_gy_commutes_with_image_modulo_isos. - exact inv_of_pullback_first_projection_commutes_with_image_modulo_isos. - exact inv_of_pullback_second_projection_commutes_with_image_modulo_isos. Qed.
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.