Lemma weq_hom' {c1 : C} {c2 : C} (f : C ⟦ c1, c2 ⟧) : ∃! x : (∑ f0 : C ⟦ c1, c2 ⟧, pr1 (uo c1) -->[ f0] pr1 (uo c2)), pr1 x = f. Proof. use tpair. - simple refine ((_ ,, _) ,, _). + exact f. + apply (pr1 (is_contr_disp_mor _ _ f)). + apply idpath. - intros [[g gg] p]. use subtypePath. { intro ; apply homset_property. } use subtypePath. { intro. apply isapropifcontr. apply is_contr_disp_mor. } exact p. Qed.
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.catiso. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.