Definition is_universal_arrow_to {D C : precategory} (S : functor D C) (c : C) (r : D) (v : C⟦c, S r⟧) : UU := ∏ (d : D) (f : C⟦c, S d⟧), ∃! (f' : D⟦r,d⟧), v · #S f' = f. Context {X A : category} (G : functor A X) (F0 : ob X -> ob A) (eta : ∏ x, X⟦x, G (F0 x)⟧) (Huniv : ∏ x, is_universal_arrow_to G x (F0 x) (eta x)). Local Definition F_data : functor_data X A. Proof. use tpair. + apply F0. + intros a b f. use (pr1 (pr1 (Huniv _ _ _ ))). apply (f · eta _ ). 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.