## Stream: maths

### Topic: Instance confusion

#### Bhavik Mehta (Jul 06 2020 at 14:18):

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
apply_instance,
end

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

end


#### Bhavik Mehta (Jul 06 2020 at 14:23):

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 (Jul 06 2020 at 14:24):

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 (Jul 06 2020 at 14:24):

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

#### Johan Commelin (Jul 06 2020 at 14:24):

Also, should the haveI be a letI?

#### Bhavik Mehta (Jul 06 2020 at 14:25):

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

#### Bhavik Mehta (Jul 06 2020 at 14:26):

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

#### Bhavik Mehta (Jul 06 2020 at 14:27):

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

Last updated: May 09 2021 at 10:11 UTC