Definition pr1_category_inhabited : locally_inhabited D. Proof. intros x y f xx yy. pose (pr1 HD (x ,, xx) (y ,, yy) f) as i. unfold issurjective in i. cbn in i. use (@hinhuniv _ (make_hProp _ _) _ i). - apply disp_cat_is_locally_propositional. apply HD. - cbn ; intros z. pose (pr21 z) as m. pose (pr2 z) as p. cbn in m, p. exact (transportf (λ z, xx -->[ z ] yy) p m). 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.