proposition: Lemma is_exists_unique {A : UU} {B : A → UU} (H : ∃! a : A, B a) : B ( pr1 (iscontrpr1 H)).
proof: Proof. exact(pr2 (pr1 H)). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits