category theory

Stream: mathlib4

[Scott Morrison]

@Mario Carneiro and/or @Gabriel Ebner, would one of you mind look at https://github.com/leanprover-community/mathlib4/pull/755? It has some meta functions that I found convenient in porting category theory. Until this is reviewed porting category theory is not going to proceed. There's a PR open at https://github.com/leanprover-community/mathlib4/pull/749 that depends on this, and ports the first half dozen or so files, along with the @[reassoc] attribute (which is where these meta functions are used).