Definition groupoidal_disp_cat_weq_conservative {C : category} (D : disp_cat C) : groupoidal_disp_cat D ≃ conservative (pr1_category D). Proof. use weqimplimpl. - exact groupoidal_disp_cat_to_conservative. - exact conservative_to_groupoidal_disp_cat. - exact (isaprop_groupoidal_disp_cat D). - apply isaprop_conservative. 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.