jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
750 stars 69 forks source link

Export a constructor that proves comp_assoc_sym #12

Closed langston-barrett closed 3 years ago

langston-barrett commented 6 years ago

This library and HoTT/HoTT have similar design for their central Category classes. However, they export a nice constructor that fills in the equivalent of comp_assoc_sym automagically.

jwiegley commented 6 years ago

Oh hey, what a nice and easy trick. Too bad we can't override {| ... |} to use a custom constructor for certain types...

jwiegley commented 3 years ago

See 98f6bdd.