📝Algebraic Subtyping

Theory books recommendations:

• Introduction to Lattices and Order by Davey and Priestley
• Categories for the Working Mathematician by Mac Lane
• Stone Spaces by Johnstone (mix of order and category theories)
• Galois connections and fixed point calculus by Backhouse (Kleene algebra)

theory:

• preorder ≤ on a set A is reflexive transitive binary relation.
• ≡ is a kernel of preorder such that a ≡ b iff a ≤ b and b ≤ a
• partial order is a preorder satisfying antisymmetry (if a ≤ b and b ≤ a, then a = b)
• partial order is preorder which kernel is equivalence (=)
• poset is a set equipped with partial order
• if S ≤ A then upper bound of S is a of A such that s ≤ a for any s in S
• least upper bound or join is upper bound b of S such that b ≤ a for any a = upper bound of S
• meet is greatest lower bound
• ⊔S - join
• ⊔∅ = ⊥
• ⊓S - meet
• ⊓∅ = ⊤
• lattice is a poset where every finite subset has a meet and join (has finite joins and meets)
• join-semilattice is a poset that has finite joins
• meet-semilattice is a poset that has finite meets
• complete lattice is a poset that has arbitrary joins and meets (not necessary of finite subsets)
• ^ same for complete semilattices