Definition pseudomonic_disp_cat_weq_pseudomonic_pr1 {C : category} (D : disp_cat C) : pseudomonic_disp_cat D ≃ pseudomonic_pr1_category D. Proof. use weqimplimpl. - exact (pseudomonic_disp_cat_to_pseudomonic_pr1 D). - exact (pseudomonic_disp_cat_from_pseudomonic_pr1 D). - apply isaprop_pseudomonic_disp_cat. - apply isaprop_pseudomonic. 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.