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