From f9e85030055822e7b019efd08d55e142a9dc3802 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Oct 2014 00:05:37 -0700 Subject: [PATCH] chore(library/algebra/category): add workaround --- library/algebra/category/adjoint.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean index 5cb400df5..9036dcceb 100644 --- a/library/algebra/category/adjoint.lean +++ b/library/algebra/category/adjoint.lean @@ -22,13 +22,10 @@ namespace adjoint section parameters {obC obD : Type} (C : category obC) {D : category obD} - -- Add auxiliary category instance needed by functor.compose at (Hom D ∘f sorry) - private definition aux_prod_cat [instance] : category (obD × obD) := prod_category (opposite.opposite D) D - - definition adjoint (obC obD : Type) (C : category obC) (D : category obD) (F : C ⇒ D) (G : D ⇒ C) := - natural_transformation (Hom D ∘f sorry) + definition adjoint (F : C ⇒ D) (G : D ⇒ C) := + natural_transformation (@functor.compose _ _ _ _ _ _ (Hom D) sorry) --(Hom C ∘f sorry) ---product.prod_functor (opposite.opposite_functor F) (functor.ID D) + --product.prod_functor (opposite.opposite_functor F) (functor.ID D) end end adjoint