Lemma weq_hom {c1 : C} {c2 : C} (d1 : D c1) (d2 : D c2) (f : C ⟦ c1, c2 ⟧) : ∃! x : (∑ f0 : C ⟦ c1, c2 ⟧, d1 -->[ f0] d2), pr1 x = f. Proof. use tpair. - simple refine ((_ ,, _) ,, _). + exact f. + apply uf0. + apply idpath. - cbn. intros [[g gg] q]. use subtypePath. { intro ; apply homset_property. } use subtypePath. { intro. apply isapropifcontr. apply uf0. } exact q. 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.