package rocq-partial-orders

Library about partial orders with more or less infimas and suprema (semi-lattices, lattices, complete partial orders, complete lattices). Duality, fixpoint theorems (BourbakiWitt, Pataraia), instances (notably, various function spaces), adjunctions/Galois connections. Hierarchy of structures implemented with Hierarchy Builder. Based on setoids from the beginning, as a convenient way to obtain axiom-free quotients.