# Commit 2021-01-07 21:43 4da83134

View on Github →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.