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. 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.
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.