feat(category_theory): associator and unitors for functors (#478)
feat(category_theory): associator and unitors for functors (#478)

also check pentagon and triangle
leanprover-community/mathlib,leanprover-community/mathlib