Definition mapUniqueness {C:category} (X:[C^op,HSET]) (r : Representation X) (c:C) (f g: c --> universalObject r) : r ⟲ f = r ⟲ g -> f = g := invmaponpathsweq (universalProperty _ _) _ _.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.