search

b-mehta / topos

Topos theory in lean
55 stars 2 forks source link

Cartesian closed #4

Closed b-mehta closed 4 years ago

b-mehta commented 4 years ago

We're going to need cartesian closed categories. My intuition is to define it by asserting that the right adjoint to product exists, but maybe this is awkward to phrase using what's in mathlib - let's investigate.

b-mehta commented 4 years ago

It doesn't seem too bad. We might need to add that (- * X) is a functor, and then can just say is_left_adjoint (prod X)

EdAyers commented 4 years ago

93163fec907ec6daf8ffe469a366538ad17d0a5a

b-mehta commented 4 years ago

This seems pretty done I think. Let's make them easy to use now