proposition: Lemma disp_functor_ff_reflect_disp_iso_right : ff ;; gg = transportb (mor_disp xx xx) (z_iso_inv_after_z_iso f) (id_disp xx).
proof: Proof. unfold ff, gg. rewrite <- disp_functor_ff_inv_compose. etrans. { do 2 apply maponpaths. exact (inv_mor_after_z_iso_disp Fff). } unfold transportb. rewrite <- (disp_functor_ff_inv_identity FF HFF). rewrite <- disp_functor_ff_inv_transportf. unfold transportb. rewrite !transport_f_f. apply maponpaths. apply maponpaths_2. apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Functors