Zulip Chat Archive

Stream: Is there code for X?

Topic: Cartesian Closed Categories

Reed Mullanix (Jun 14 2020 at 21:01):

Does anyone know if there is a definition of cartesian closed categories floating about?

Bhavik Mehta (Jun 14 2020 at 21:02):

Yes!

Bhavik Mehta (Jun 14 2020 at 21:02):

It's in my PR here: https://github.com/leanprover-community/mathlib/pull/2894

Bhavik Mehta (Jun 14 2020 at 21:02):

I just haven't had the chance yet to make the (small) changes needed there

Reed Mullanix (Jun 14 2020 at 21:08):

This looks awesome!

Bhavik Mehta (Jun 16 2020 at 03:50):

@Reed Mullanix It's now merged to mathlib :)

Last updated: Dec 20 2023 at 11:08 UTC