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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.