proposition: Lemma isweq_z_iso_to_z_iso_disp (a : disp_over_unit tt) (b : disp_over_unit tt) : isweq (X := z_iso a b) (Y := z_iso_disp (identity_z_iso (tt : unit_category)) a b) (λ f, (_ ,, _ ,, z_iso_after_z_iso_inv f ,, z_iso_inv_after_z_iso f)).
proof: Proof. use isweq_iso. - intro f. exact (make_z_iso _ _ (inv_mor_after_z_iso_disp f ,, z_iso_disp_after_inv_mor f)). - intro. now apply z_iso_eq. - intro. now apply eq_z_iso_disp. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Examples UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Fiber