✐‹creator "Kevin Kappelmann"› theory Order_Functors imports Order_Functors_Base Order_Equivalences Order_Isomorphisms begin paragraph ‹Summary› text ‹Functors between orders aka. order-homomorphisms aka. monotone functions.› end