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