Commit 2021-01-07 21:43 4da83134

feat(category_theory/closed): golf definition and proofs (#5623) Using the new mates framework, simplify the definition of pre and shorten proofs about it. To be more specific,

• pre is now explicitly a natural transformation, rather than indexed morphisms with a naturality property
• The new definition of pre means things like pre_map which I complained about before are easier to prove, and pre_post_comm is automatic
• There are now more lemmas relating pre to coev, ev and uncurry: uncurry_pre in particular was a hole in the API.
• internal_hom has a shorter construction. In particular I changed the type to Cᵒᵖ ⥤ C ⥤ C, which I think is better since the usual external hom functor is given as Cᵒᵖ ⥤ C ⥤ Type*, so this is consistent with that. In a subsequent PR I'll do the same for exp_comparison, but that's a bigger change with improved API so they're separate for now.