search

b-mehta / topos

Topos theory in lean
56 stars 2 forks source link

Theorem I.5.2 (Colimit of representables) #3

Closed b-mehta closed 4 years ago

b-mehta commented 4 years ago

Theorem I.5.2 from MM is a great result (and its corollary I.5.3 is important). Let's put it in.

b-mehta commented 4 years ago

Completed in category.colimits.