proposition: Lemma id_conjugation_disp {C: category} {D: disp_cat C} {a b: C} {da: D a} {db: D b} {f: a--> b} {g: b --> a} {x: b --> b} (df: da -->[f] db) (dg: db -->[g] da) (dx: db -->[x] db) (e0: x = identity _) (e1 : f · g = identity _) : dx = transportb _ e0 (id_disp _) -> df ;; dg = transportb _ e1 (id_disp _) -> df ;; dx ;;dg = transportb _ (id_conjugation f g x e0 e1) (id_disp _).
proof: Proof. intros H H'. rewrite H. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite (id_right_disp df). rewrite transport_f_b. repeat rewrite mor_disp_transportf_postwhisker. rewrite H'. rewrite transport_f_b. apply (maponpaths (λ e, transportf _ e _)). apply uip. apply homset_property. Qed.
imports: UniMath.Foundations.Sets UniMath.Foundations.PartD UniMath.MoreFoundations.PartA UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering