Lemma lift_preserves_chosen_equalizers_uptoeq_after_isotoid_induction : ∥ H (E₂ (G x) (G y) f' g') = E₃ (H (G x)) (H (G y)) (# H f') (# H g') ∥. Proof. use (factor_through_squash _ _ (Feq x y f₁ g₁)). { apply isapropishinh. } intro pf_F. set (Geq := weak_equiv_preserves_equalizers_eq Gw (pr2 C2) E₁ E₂). use (factor_through_squash _ _ (Geq x y f₁ g₁)). { apply isapropishinh. } intro pf_G. clear Geq. assert (p₀ : f' = #G f₁). { apply pathsinv0, functor_on_fully_faithful_inv_hom. } assert (p₁ : g' = #G g₁). { apply pathsinv0, functor_on_fully_faithful_inv_hom. } apply hinhpr. rewrite p₀, p₁. clear p₀ p₁. etrans. { apply maponpaths. exact (! pf_G). } clear pf_G. set (ϕ := isotoid _ (pr2 C3) (nat_z_iso_pointwise_z_iso α (E₁ _ _ f₁ g₁))). refine (ϕ @ _). refine (pf_F @ _) ; clear pf_F. use (isotoid _ (pr2 C3)). pose (ϕ₁ := nat_z_iso_pointwise_z_iso α x). pose (ϕ₂ := nat_z_iso_pointwise_z_iso α y). pose (ψ₁ := isotoid _ (pr2 C3) ϕ₁). pose (ψ₂ := isotoid _ (pr2 C3) (z_iso_inv ϕ₂)). use (Equalizer_eq E₃ (f := #F f₁) (g := #F g₁) ψ₁ ψ₂). - unfold ψ₁, ψ₂. do 2 rewrite idtoiso_isotoid. etrans. { apply maponpaths_2. exact (! pr21 α _ _ _). } apply z_iso_inv_to_right. apply idpath. - unfold ψ₁, ψ₂. do 2 rewrite idtoiso_isotoid. etrans. { apply maponpaths_2. exact (! pr21 α _ _ _). } apply z_iso_inv_to_right. apply idpath. 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.Equalizers. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Equalizers. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Equalizers.