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. 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.
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.