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


  • 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