proposition: Lemma disp_functor_ff_reflect_disp_iso_left : gg ;; ff = transportb (mor_disp yy yy) (z_iso_after_z_iso_inv f) (id_disp yy).
proof: Proof. unfold ff, gg. rewrite <- disp_functor_ff_inv_compose. etrans. { do 2 apply maponpaths. exact (z_iso_disp_after_inv_mor 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