Lemma isotoid_disp_transportf_idtoiso_disp {c c' : C} {e0 e1: c = c'} {d : D c} {d' : D c'} (e : transportf D e0 d = d') e2 e3 : isotoid_disp uD e1 (transportf (λ i0 : z_iso c c', z_iso_disp i0 d d') e2 (idtoiso_disp e0 e)) = transportf (λ en : c =c', transportf D en d = d') e3 e. Proof. destruct e3, e0, e. assert (e2 = idpath (identity_z_iso c)) as E. { apply uip. apply isaset_z_iso. } rewrite E. etrans. apply (isotoid_idtoiso_disp uD (idpath c) (idpath d)). reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.StreetFibration.