definitions convType_category_mixin and semiCompSemiLattConvType_category_mixin
are more uniform
hom_affine_function move earlier in the file as hom_affine to avoid case analysis
declared as Canonical to enjoy [affine of _] notation
similarly, hom_biglubmorph declared as Canonical for the generic lemma biglub_morph
to be usable
instead of the ill-named apply_affine
remove eps0'', eta1''
they may have been here to be uniform but they are really just redefinitions
more generally trying to reduce the number of identifiers and lemmas
ending with ' or '' by turning blah''/blah' definitions as Let
and favoring blahE lemmas (instead of blah''E/blah'E)
minor improvements coming partly from a new infotheo branch
is_convex_set_image' replaced with is_convex_set_image
NB: based on infotheo's
master0.3.1!@t6s