proposition: Proposition equalizer_from_pb_prod_comm : equalizer_from_pb_prod_map · i = h.
proof: Proof. exact (PullbackArrow_PullbackPr2 e _ (h · f) h equalizer_from_pb_prod_map_eq). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Pullbacks