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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors.