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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.DisplayedCats.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.