fact: 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).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Epis UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.Monics UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering