Definition conservative_to_groupoidal_disp_cat {C : category} {D : disp_cat C} (HD : conservative (pr1_category D)) : groupoidal_disp_cat D. Proof. intros x y f Hf xx yy ff. assert (@is_z_isomorphism (total_category D) (_ ,, _) (_ ,, _) (f ,, ff)) as Hff. { apply HD. apply Hf. } refine (transportf (λ z, is_z_iso_disp (make_z_iso' f z) ff) _ (is_z_iso_disp_from_total Hff)). apply isaprop_is_z_isomorphism. Defined.
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.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.