# 📝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