Computational Quadrinitarianism (2018)

Going the other way, we also run into obstacles: there is a general notion, opposite to the “syntactic category” of a type theory, which is the “internal logic” of a category. A Heyting algebra is a special type of distributive lattice (partially ordered set, equipped with meet and join operations, such that meet and join distribute over one another) which has an implication operation that satisfies curry/uncurry adjointness — i.e. such that c ∧ a ≤ b c ≤ a → b. (Replace meet here by “and” (spelled “*”), and ≤ by ⊢ and we have the familiar type-theoretic statement that c * a ⊢ b c ⊢ a → b). Another way to think of a → b is as the greatest element of the lattice such that a → b ∧ a ≤ b (exercise: relate this to the first definition).

Source: comonad.com