Proposition pb_prod_is_inverse : is_inverse_in_precat map_from_pb_prod map_to_pb_prod. Proof. unfold map_from_pb_prod, map_to_pb_prod. split. - use (MorphismsIntoPullbackEqual (isPullback_Pullback pb)). + rewrite !assoc'. rewrite PullbackArrow_PullbackPr1. rewrite id_left. use BinProductArrowsEq. * rewrite !assoc'. rewrite BinProductPr1Commutes. rewrite !assoc. etrans. { apply maponpaths_2. apply BinProductPr1Commutes. } refine (!_). apply PullbackSqrCommutes. * rewrite !assoc'. rewrite BinProductPr2Commutes. apply BinProductPr2Commutes. + rewrite !assoc'. rewrite PullbackArrow_PullbackPr2. rewrite id_left. apply BinProductPr1Commutes. - use BinProductArrowsEq. + rewrite !assoc'. rewrite BinProductPr1Commutes. rewrite PullbackArrow_PullbackPr2. rewrite id_left. apply idpath. + rewrite !assoc'. rewrite BinProductPr2Commutes. rewrite !assoc. rewrite PullbackArrow_PullbackPr1. rewrite id_left. apply BinProductPr2Commutes. 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).