proposition: Lemma dispPostcompWithBinProductArrow {c d : C} {Pcd : BinProduct C c d} {cc : D c} {dd : D d} (dPcd : dispBinProduct c d Pcd cc dd) {a b : C} {Pab : BinProduct C a b} {aa : D a} {bb : D b} (dPab : dispBinProduct a b Pab aa bb) {f : a --> c} {g : b --> d} (ff : aa -->[f] cc) (gg : bb -->[g] dd) {x : C} {xx : D x} {k : x --> a} {h : x --> b} (kk: xx -->[k] aa) (hh: xx -->[h] bb) : dispBinProductArrow Pab dPab kk hh ;; dispBinProductOfArrows dPcd dPab ff gg = transportb _ (postcompWithBinProductArrow C Pcd Pab f g k h) (dispBinProductArrow Pcd dPcd (kk ;; ff) (hh ;; gg)).
proof: Proof. apply transportb_transpose_right. apply dispBinProductArrowUnique. - etrans. { apply mor_disp_transportf_postwhisker. } rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr1. rewrite transport_f_f. apply pathsinv0, transportf_comp_lemma. etrans. 2: { apply pathsinv0, mor_disp_transportf_prewhisker. } rewrite assoc_disp. rewrite dispBinProductPr1Commutes. rewrite transport_f_b. apply transportf_comp_lemma. unfold transportb. etrans. 2: { apply pathsinv0, mor_disp_transportf_postwhisker. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - etrans. { apply mor_disp_transportf_postwhisker. } rewrite assoc_disp_var. rewrite dispBinProductOfArrowsPr2. rewrite transport_f_f. apply pathsinv0, transportf_comp_lemma. etrans. 2: { apply pathsinv0, mor_disp_transportf_prewhisker. } rewrite assoc_disp. rewrite dispBinProductPr2Commutes. rewrite transport_f_b. apply transportf_comp_lemma. unfold transportb. etrans. 2: { apply pathsinv0, mor_disp_transportf_postwhisker. } 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