module Order.Heyting where

Heyting algebras🔗

A Heyting algebra is a lattice which is equipped to handle implication: it has a binary operation $a \mathrel{\scriptsize{⇨}} b$ for which we have an equivalence between $(a \land b) \le c$ and $a \le (b \mathrel{\scriptsize{⇨}} c)$. Reading this from the perspective of logic, we may interpret the parameter $a$ as a context, so that our equivalence says we have inference rules

When we enrich our poset of propositions to a category of contexts, the notion of Heyting algebra is generalised to that of Cartesian closed category (with finite coproducts).

record is-heyting-algebra {o ℓ} (P : Poset o ℓ) : Type (o ⊔ ℓ) where
  open Poset P

  field
    has-top    : Top P
    has-bottom : Bottom P

    _∪_      : Ob → Ob → Ob
    ∪-joins  : ∀ x y → is-join P x y (x ∪ y)

    _∩_      : Ob → Ob → Ob
    ∩-meets  : ∀ x y → is-meet P x y (x ∩ y)

    _⇨_  : ⌞ P ⌟ → ⌞ P ⌟ → ⌞ P ⌟
    ƛ    : ∀ {x y z} → x ∩ y ≤ z → x ≤ y ⇨ z
    ev   : ∀ {x y z} → x ≤ y ⇨ z → x ∩ y ≤ z

Elementary properties🔗

The first thing we note about Heyting algebras is that they are distributive lattices. This is because, for an arbitrary $P$, we can reduce the problem of showing

$$x \cap (y \cup z) \le P \text{,}$$

by adjointness, to showing

$$(y \cup z) \le x \mathrel{\scriptsize{⇨}} P \text{,}$$

where the universal property of the join is actually applicable — allowing us further reductions to showing showing $(y \land x) \le P$ and $(z \land x) \le P$. The following calculation formalises this sketch:

  ∩-∪-distrib≤ : ∀ {x y z} → x ∩ (y ∪ z) ≤ (x ∩ y) ∪ (x ∩ z)
  ∩-∪-distrib≤ {x} {y} {z} =
    let
      case₁ : y ∩ x ≤ (x ∩ y) ∪ (x ∩ z)
      case₁ = ≤-trans (≤-refl' ∩-comm) l≤∪

      case₂ : z ∩ x ≤ (x ∩ y) ∪ (x ∩ z)
      case₂ = ≤-trans (≤-refl' ∩-comm) r≤∪

      body : (y ∪ z) ≤ x ⇨ (x ∩ y) ∪ (x ∩ z)
      body = ∪-universal _ (ƛ case₁) (ƛ case₂)
    in x ∩ (y ∪ z)    =⟨ ∩-comm ⟩
       (y ∪ z) ∩ x    ≤⟨ ev body ⟩
       x ∩ y ∪ x ∩ z  ≤∎