has_internal_hom class carrying data #12472

Stream: PR reviews

[Johan Commelin]

Just like @Scott Morrison I hadn't realised that is_left_adjoint was already carrying data. I wonder whether it is still worth putting more emphasis on the ihom part of the data. Right now we have

/--
This is the internal hom `A ⟶[C] -`.
Note that this is essentially an opaque definition,
and so will not agree definitionally with any "native" internal hom the category has.
TODO: we could introduce a `has_ihom` class
that allows specifying a particular definition of the internal hom,
and provide a low priority opaque instance.
-/
def ihom : C ⥤ C :=
(@closed.is_adj _ _ _ A _).right

As I understand it, this docstring is incorrect. But it still points to a problem with the current approach: even if there are no defeq problems, the ihom is still taking a back seat, in some sense.

[Johan Commelin]

cc @Bhavik Mehta

[Scott Morrison]

I'll fix that comment at some point. I

[Scott Morrison]

I'm not sure that it's a problem having ihom take a back seat. I've been using the internal hom in Module R today a bit, and it seems to work fine.

[Scott Morrison]

Perhaps the monoidal_closed (Module R) instance would be slightly more understandable if we rearranged the definition?

[Johan Commelin]

Yeah, that's exactly what I'm hoping