mathlib3

feat(logic/function): comp₂ -- useful for binary operations

#993

Merged