proposition: Lemma homset_conj'_after_conj_inv {c : C} {c' : C'} {g : C⟦c, G c'⟧} {d : D c} (d' : D' c') (alpha : d -->[g] GG _ d') : transportf _ (φ_adj_after_φ_adj_inv A g) (homset_conj' _ _ _ (homset_conj_inv g d d' alpha)) = alpha.
proof: Proof. unfold homset_conj_inv. cbn. set (eq := homset_conj'_natural_precomp (εε c' d') alpha). cbn in eq. rewrite eq. unfold homset_conj'. cbn. rewrite transport_f_b. assert (triangle2 : (ηη (G c') (GG c' d');; ♯ GG (εε c' d')) = transportb _ (triangle_id_right_ad A c') (id_disp _)) by (exact (pr2 (pr2 X) c' d')). cbn in triangle2. rewrite triangle2. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite id_right_disp. unfold transportb. rewrite 2 transport_f_f. intermediate_path (transportf _ (idpath _ ) alpha). - apply maponpaths_2, homset_property. - apply idpath. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Equivalences