Instance confusion

Stream: maths

[Bhavik Mehta]

Here's where I'm at right now, and presumably this suggests something has been set up wrong, can anyone help?

import category_theory.adjunction.limits
import category_theory.closed.cartesian

universes v u₁ u₂

namespace category_theory
open category limits
variables {C : Type u₁} [category.{v} C] [has_finite_products C] [cartesian_closed C]
variables {D : Type u₂} [category.{v} D] [has_finite_products D] [cartesian_closed D]
variables (F : C ⥤ D)

class cartesian_closed_functor [preserves_limits_of_shape (discrete walking_pair) F] :=
(comparison_iso : ∀ A B, is_iso (exp_comparison F A B))

variables {F} {L : D ⥤ C}

def frobenius_map (A : C) (B : D) (adj : L ⊣ F) : L.obj (B ⨯ F.obj A) ⟶ L.obj B ⨯ A :=
prod_comparison _ _ _ ≫ limits.prod.map (𝟙 _) (adj.counit.app A)

instance (adj : L ⊣ F) : preserves_limits_of_shape (discrete walking_pair) F :=
begin
  haveI := adjunction.right_adjoint_preserves_limits adj,
  apply_instance,
end

instance (adj : L ⊣ F) [∀ A B, is_iso (frobenius_map A B adj)] : cartesian_closed_functor F :=
begin

end

[Bhavik Mehta]

Actually I suppose the point here is that in maths the question of if a functor is cartesian closed first needs binary products to be preserved, and in my case it's a right adjoint so that's fine

[Bhavik Mehta]

But in lean this inference isn't immediate so it would be sensible to have preservation of binary prods as part of the definition of cartesian closed functor

[Johan Commelin]

What exactly is the problem? Do you get an error?

[Johan Commelin]

Also, should the haveI be a letI?

[Bhavik Mehta]

The instance at the bottom doesn't have a valid statement

[Bhavik Mehta]

Potentially, I'm not sure it makes a huge difference though since preserving limits is subsingleton

[Bhavik Mehta]

I've got to step away for a little - I'll continue trying later