Definition is_universal_arrow_from {D C : category} (S : functor D C) (c : C) (r : D) (v : C⟦S r, c⟧) : UU := ∏ (d : D) (f : C⟦S d,c⟧), ∃! (f' : D⟦d,r⟧), f = # S f' · v. Context {X A : category} (F : functor X A) (G0 : ob A -> ob X) (eps : ∏ a, A⟦F (G0 a),a⟧) (Huniv : ∏ a, is_universal_arrow_from F a (G0 a) (eps a)). Local Definition G_data : functor_data A X. Proof. use tpair. + apply G0. + intros a b f. apply (pr1 (pr1 (Huniv b (G0 a) (eps a · f)))). Defined.
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.NaturalTransformations. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.SplitMonicsAndEpis. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Section HomSetIsoRightFromPartial. End HomSetIsoRightFromPartial. Section HomSetIsoLeftFromPartial. End HomSetIsoLeftFromPartial.