proposition: Lemma dispBinProduct_endo_is_identity {a b : C} (aa : D a) (bb : D b) (P : BinProduct _ a b) (dP : dispBinProduct a b P aa bb) {k : BinProductObject _ P --> BinProductObject _ P} (kk: dispBinProductObject P dP -->[k] dispBinProductObject P dP) (H1 : k · BinProductPr1 _ P = BinProductPr1 _ P) (dH1 : kk ;; dispBinProductPr1 P dP = transportb _ H1 (dispBinProductPr1 P dP)) (H2 : k · BinProductPr2 _ P = BinProductPr2 _ P) (dH2 : kk ;; dispBinProductPr2 P dP = transportb _ H2 (dispBinProductPr2 P dP)) : transportf _ (BinProduct_endo_is_identity C a b P k H1 H2) (id_disp (dispBinProductObject P dP)) = kk.
proof: Proof. apply pathsinv0. etrans. { apply dispBinProductArrowEta. } apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. - etrans. { apply mor_disp_transportf_postwhisker. } rewrite id_left_disp. rewrite transport_f_b. apply transportf_comp_lemma. etrans. 2: { apply pathsinv0; exact dH1. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - etrans. { apply mor_disp_transportf_postwhisker. } rewrite id_left_disp. rewrite transport_f_b. apply transportf_comp_lemma. etrans. 2: { apply pathsinv0; exact dH2. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. 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