Commit 2021-11-22 11:23 2aea9961

feat(data): define a fun_like class of bundled homs (function + proofs) (#10286) This PR introduces a class fun_like for types of bundled homomorphisms, like set_like is for bundled subobjects. This should be useful by itself, but an important use I see for it is the per-morphism class refactor, see #9888. Also, coe_fn_coe_base now has an appropriately low priority, so it doesn't take precedence over fun_like.has_coe_to_fun.