proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.StreetFibration