Order for cartesian closed categories

Stream: new members

[Gareth Ma]

(deleted)

[Gareth Ma]

(deleted) It seems I might be missing something indeed...

[Gareth Ma]

Actually, I believe part of my original question still holds.

Looking at the definition of closed monoidal categories

/-- An object `X` is (right) closed if `(X ⊗ -)` is a left adjoint. -/
class Closed {C : Type u} [Category.{v} C] [MonoidalCategory.{v} C] (X : C) where
  /-- a choice of a right adjoint for `tensorLeft X` -/
  rightAdj : C ⥤ C
  /-- `tensorLeft X` is a left adjoint -/
  adj : tensorLeft X ⊣ rightAdj

It's defined as adjunction $X \otimes - \dashv [X, -]$, but it seems the convention is $- \otimes Y \dashv [Y, -]$ (so $Hom(X \otimes Y, Z) = Hom(X, [Y, Z])$). Is that "intended"?

[Matt Diamond]

when I was working on a proof of Lawvere's fixed-point theorem I noticed that the evaluation map seemed to have the arguments reversed from what was in the literature... I wonder if this is why

[Matt Diamond]

@Bhavik Mehta might know why it's designed this way