proposition: Lemma dispBinProductArrowEta {c d : C} (P : BinProduct C c d) (cc : D c) (dd : D d) (dP : dispBinProduct c d P cc dd) {x : C} (xx : D x) {fg : x --> BinProductObject C P } (fgfg : xx -->[ fg] dispBinProductObject P dP) : fgfg = transportb (mor_disp xx (dispBinProductObject P dP)) (BinProductArrowEta C c d P x fg) (dispBinProductArrow P dP (fgfg ;; dispBinProductPr1 P dP) (fgfg ;; dispBinProductPr2 P dP)).
proof: Proof. apply transportf_transpose_right. apply dispBinProductArrowUnique. - etrans. { apply mor_disp_transportf_postwhisker. } unfold transportb. apply (maponpaths (fun z => transportf (mor_disp xx cc) z (fgfg ;; dispBinProductPr1 P dP))). apply C. - etrans. { apply mor_disp_transportf_postwhisker. } unfold transportb. apply (maponpaths (fun z => transportf (mor_disp xx dd) z (fgfg ;; dispBinProductPr2 P dP))). apply C. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total