Definition adj_equiv_preserves_equalizers_b (E : Equalizers C₂) : Equalizers C₁. Proof. intros x y f g. use (Equalizer_z_iso_lr (make_Equalizer _ _ _ _ (right_adjoint_preserves_equalizer _ HL _ _ _ _ _ _ _ _ (isEqualizer_Equalizer (E (L x) (L y) (#L f) (#L g)))))). - rewrite <- !functor_comp. apply maponpaths. apply EqualizerEqAr. - apply (nat_z_iso_pointwise_z_iso η). - apply (nat_z_iso_pointwise_z_iso η). - abstract (exact (!(nat_trans_ax η _ _ f))). - abstract (exact (!(nat_trans_ax η _ _ g))). 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.Preservation. Require Import UniMath.CategoryTheory.Limits.LimitIso. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.