Proposition equalizer_from_pb_prod_eq : i · f = i · g. Proof. pose (maponpaths (λ z, z · BinProductPr1 _ _) (PullbackSqrCommutes e)) as p. cbn in p. rewrite !assoc' in p. unfold Δ, φ, diagonalMap' in p. rewrite !BinProductPr1Commutes in p. rewrite id_right in p. refine (!p @ _). clear p. pose (maponpaths (λ z, z · BinProductPr2 _ _) (PullbackSqrCommutes e)) as p. cbn in p. rewrite !assoc' in p. unfold Δ, φ, diagonalMap' in p. rewrite !BinProductPr2Commutes in p. rewrite id_right in p. exact p. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Section EqualizersFromPullbackProducts. End EqualizersFromPullbackProducts. - exact (BinProductsFromPullbacks PB T).