Definition preserves_equalizer_nat_z_iso_f (HF : preserves_equalizer F) : preserves_equalizer G. Proof. intros x y e f g h p Fp H. assert (q : # F h · # F f = # F h · # F g). { abstract (rewrite <- !functor_comp ; exact (maponpaths #F p)). } pose (eq := make_Equalizer _ _ _ q (HF _ _ _ _ _ _ _ _ H)). use (isEqualizer_z_iso (isEqualizer_Equalizer (Equalizer_z_iso_lr eq _ _ _ _))). - exact (z_iso_inv (nat_z_iso_pointwise_z_iso τ x)). - exact (z_iso_inv (nat_z_iso_pointwise_z_iso τ y)). - abstract (cbn ; use z_iso_inv_on_left ; rewrite !assoc' ; cbn ; refine (!_) ; use z_iso_inv_on_right ; apply nat_trans_ax). - abstract (cbn ; use z_iso_inv_on_left ; rewrite !assoc' ; cbn ; refine (!_) ; use z_iso_inv_on_right ; apply nat_trans_ax). - exact (z_iso_inv (nat_z_iso_pointwise_z_iso τ e)). - abstract (cbn ; rewrite nat_trans_ax ; refine (!(id_left _) @ !_) ; rewrite !assoc ; apply maponpaths_2 ; apply z_iso_after_z_iso_inv). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.PullbackConstructions. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.EquivalencePreservation. Require Import UniMath.CategoryTheory.Limits.LimitIso. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.whiskering. Let prodC : BinProducts C := BinProductsFromPullbacks PBC TC.