Proposition preserves_pullback_from_binproduct_equalizer_unique : isaprop (∑ hk, (hk · # F (PullbackPr1 (PBC z x y f g)) = h) × (hk · # F (PullbackPr2 (PBC z x y f g)) = k)). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use (EqualizerInsEq FE). use (BinProductArrowsEq _ _ _ Fxy) ; cbn. - rewrite !assoc'. rewrite <- !functor_comp. exact (pr12 φ₁ @ !(pr12 φ₂)). - rewrite !assoc'. rewrite <- !functor_comp. exact (pr22 φ₁ @ !(pr22 φ₂)). Qed.
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.PullbackConstructions. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.EquivalencePreservation. Require Import UniMath.CategoryTheory.Limits.LimitIso. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.whiskering. Let prodC : BinProducts C := BinProductsFromPullbacks PBC TC.