Lemma fully_faithful_inv_hom_of_pullback_diagram_commutes : π₁x · fx = π₂x · gx. Proof. unfold π₁x, fx, π₂x, gx. do 2 rewrite <- fully_faithful_inv_comp. apply maponpaths. rewrite ! assoc'. apply maponpaths. rewrite ! assoc. apply maponpaths_2. refine (_ @ q @ _). - apply maponpaths_2. refine (_ @ id_right _). refine (assoc' _ _ _ @ _). apply maponpaths. apply z_iso_after_z_iso_inv. - apply maponpaths_2. rewrite assoc'. refine (! id_right _ @ _). apply maponpaths. apply pathsinv0, z_iso_after_z_iso_inv. 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.