Definition are_relative_adjoints {I: precategory_data} {C D: precategory_data} (J: functor_data I C) (L: functor_data I D) (R: functor_data D C) : UU := ∑ (hom_weq : ∏ {X : I} {Y : D}, L X --> Y ≃ J X --> R Y), (∏ (Y : I) (Z : D) (f : L Y --> Z) (X : I) (h : X --> Y), hom_weq (#L h · f) = #J h · hom_weq f) × (∏ (X : I) (Y : D) (f : L X --> Y) (Z : D) (k : Y --> Z), hom_weq (f · k) = hom_weq f · #R k).
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.