Definition pseudomonic_weq_locally_prop_and_iso_contractible {C : category} (D : disp_cat C) : pseudomonic_disp_cat D ≃ locally_propositional D × locally_iso_contractible D. Proof. use weqimplimpl. - intro H. split. + apply H. + apply pseudomonic_to_iso_contractible. exact H. - intro H. split. + exact (pr1 H). + intros x y f xx yy. apply (pr2 H). - apply isaprop_pseudomonic_disp_cat. - apply isapropdirprod. + apply isaprop_locally_propositional. + apply isaprop_locally_iso_contractible. 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.