Zulip Chat Archive

Stream: Is there code for X?

Topic: Cartesian Closed Categories


view this post on Zulip Reed Mullanix (Jun 14 2020 at 21:01):

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

view this post on Zulip Bhavik Mehta (Jun 14 2020 at 21:02):

Yes!

view this post on Zulip Bhavik Mehta (Jun 14 2020 at 21:02):

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

view this post on Zulip Bhavik Mehta (Jun 14 2020 at 21:02):

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

view this post on Zulip Reed Mullanix (Jun 14 2020 at 21:08):

This looks awesome!

view this post on Zulip Bhavik Mehta (Jun 16 2020 at 03:50):

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


Last updated: May 07 2021 at 22:14 UTC