generalising closed cartesian categories to closed monoidal

Stream: maths

[Scott Morrison]

@Bhavik Mehta, I want to have some of the material you developed for closed cartesian categories available more generally for closed monoidal categories. Lots of the basic stuff just generalises directly (indeed, you left a comment to this effect).

I'm having trouble seeing how to do it without duplicating everything however.

#12386 is a start on this, and you can see I've just duplicated the material on currying. Any suggestions on improving this? The fundamental problem is that I don't think we want to use the "general" ihom everywhere in place of exp, because then there will be unification/typechecking problems all over the place when Lean can't see that the monoidal structure involved is just the cartesian structure.

[Adam Topaz]

@Scott Morrison perhaps worthwhile mentioning that I experimented with a definition of the internal Hom in the LTE repo. See for_mathlib/internal_hom.lean there (I think?). I found it to be quite annoying to get the fully functorial construction...

[Adam Topaz]

Your construction looks much smoother!

[Scott Morrison]

It's not mine: I'm just copying and pasting what Bhavik had already done in the cartesian closed case.

[Scott Morrison]

(Noting that it works in any closed monoidal category.)

[Scott Morrison]

Wow... I have not looked for a while at how big the for_mathlib folder has become in LTE...

[Adam Topaz]

Do I understand correctly that the internal Hom functor Cop -> C -> C is still missing I'm the ihom approach?

[Scott Morrison]

It's there in the cartesian closed case, and I haven't looked yet at whether there is any obstacle to generalising it.

[Scott Morrison]

@Adam Topaz, no the internal hom functor easily generalises too. I've updated the PR.

[Adam Topaz]

Great!