exponential object

Stream: Is there code for X?

[Chris Henson]

I'm a bit confused about some of the category theory typeclasses. For example I'm not sure how to finish this:

import Mathlib.CategoryTheory.Closed.Cartesian
open CategoryTheory

def eval {X : Type} [Category X] [Limits.HasFiniteProducts X] [CartesianClosed X] (a b : X) : a ⨯ (a ⟹  b) ⟶  b := by
  sorry

[Kim Morrison]

def eval {X : Type} [Category X] [Limits.HasFiniteProducts X] [CartesianClosed X] (a b : X) :
  a ⨯ (a ⟹  b) ⟶  b := (exp.ev a).app b

[Kim Morrison]

That whole file is a bit more "point free" than it really needs to be. :-)

[Chris Henson]

Great, thank you!