As @plt-amy mentioned in the discord, the current printing situation for concrete limits and colimits is getting out of hand!
One way to resolve this is to have flat records like https://1lab.dev/Order.Lattice.html#628, where all operations that show up in goals are top-level fields. This refactor should also touch things like has-products.
As @plt-amy mentioned in the discord, the current printing situation for concrete limits and colimits is getting out of hand! One way to resolve this is to have flat records like https://1lab.dev/Order.Lattice.html#628, where all operations that show up in goals are top-level fields. This refactor should also touch things like
has-products.