[Merged by Bors] - feat(Order/Category): partial orders with order embeddings as morphisms#30693
Closed
joelriou wants to merge 2 commits intoleanprover-community:masterfrom 
Closed
[Merged by Bors] - feat(Order/Category): partial orders with order embeddings as morphisms#30693joelriou wants to merge 2 commits intoleanprover-community:masterfrom 
joelriou wants to merge 2 commits intoleanprover-community:masterfrom