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. 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.
Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering.