Commit 2025-01-28 22:24 f3eaa809
View on Github →feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element (#21094)
The preorder category of a meet-semilattice C with a top element has chosen finite products.
Motivation: I plan to use the induced monoidal structure to show that the preorder category of a distributive lattice is distributive. See this PR on Monoidal and cartesian distributive categories: #20182