Surface diagrams

LD-categories in the proof assistant homotopy.io