Definition universalObjectFunctor (C:category) : RepresentedFunctor C ⟶ C. Proof. unshelve refine (makeFunctor _ _ _ _). - intro X. exact (universalObject (pr2 X)). - intros X Y p; simpl. exact (pr2 Y \\ (p ⟳ pr2 X)). - intros X; simpl. apply uOF_identity. - intros X Y Z p q; simpl. apply uOF_comp. Defined.
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.