proposition: Proposition equalizer_from_pb_prod_eq : i · f = i · g.
proof: 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.
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