\import Category.Adjoint
\import Category.CartesianClosed
\import Category.Functor
\import Function.Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths

\lemma \infixr  =<= {E : Preorder} {x y z : E}
                     (p : x = y) (q : y <= z) : x <= z => transport (__ <= z) (inv p) q

\class HeytingAlebra \extends BoundedDistributiveLattice, CartesianClosedPrecat (\lp, \lp) {
  | implies \alias \infixr  --> : E -> E -> E
  | exponent-left {x a b : E} : x ∧ a <= b -> x <= a --> b
  | exponent-right {x a b : E} : x <= a --> b -> x ∧ a <= b

  \default top \as top-impl => bottom --> bottom
  \default top-univ {x : E} : x <= top-impl => exponent-left meet-right
  \default ldistr>= {x y z : E} : x ∧ (y ∨ z) <= (x ∧ y) ∨ (x ∧ z) => meet-comm =<= exponent-right (join-univ (exponent-left (meet-comm =<= join-left)) (exponent-left (meet-comm =<= join-right)))

  \use \lemma eval {x y : E} : (x --> y) ∧ x <= y
    => exponent-right <=-refl

  \lemma modus-ponens {x y : E} : x ∧ (x --> y) <= y
    => meet-comm =<= eval

  \lemma composition-law {x y z : E} : (x --> y) ∧ (y --> z) <= x --> z
    => exponent-left $ (meet-assoc *> meet-comm *> meet-assoc) =<= meet-monotone <=-refl modus-ponens <=∘ eval

  \func continuation (y : E) (x : E) => (x --> y) --> y

  \func neg (x : E) => x --> bottom

  \lemma neg_bottom : neg bottom = top
    => <=-antisymmetric TopMeetSemilattice.top-univ (exponent-left meet-right)

  \lemma neg_top : neg top = bottom
    => <=-antisymmetric (meet-univ <=-refl TopMeetSemilattice.top-univ <=∘ eval) bottom-univ

  \lemma id<=neg_neg {x : E} : x <= neg (neg x)
    => double-->-increasing

  \lemma neg_join {x y : E} : neg (x ∨ y) = neg x ∧ neg y
    => -->_join

  \func IsNegated (x : E) : \Prop
    => neg (neg x) <= x

  \lemma bottom-negated : IsNegated bottom
    => =_<= $ pmap neg neg_bottom *> neg_top

  \lemma meet-negated {x y : E} (xn : IsNegated x) (yn : IsNegated y) : IsNegated (x ∧ y)
    => meet-univ (double-->-monotone meet-left <=∘ xn) (double-->-monotone meet-right <=∘ yn)

  \lemma neg-negated {x : E} : IsNegated (neg x)
    => _-->-antimonotone double-->-increasing

  \func double-neg => continuation bottom

  \func curry {x y z : E} : x ∧ y --> z <= x --> (y --> z) =>
    exponent-left (exponent-left (meet-assoc =<= eval))

  \use \func -->-monotone {x y z : E} (p : y <= z) : x --> y <= x --> z => exponent-left (eval <=∘ p)

  \func -->-increasing {x y : E} : y <= x --> y => exponent-left meet-left

  \use \lemma meet-monotone-partial {x y z : E} (p : y <= z) : x ∧ y <= x ∧ z => meet-monotone <=-refl p

  \use \lemma meet-monotone-partial' {x y z : E} (p : x <= y) : x ∧ z <= y ∧ z =>
    meet-comm =<= meet-monotone-partial p <=∘ (=_<= meet-comm)

  \lemma _-->-antimonotone {x y z : E} (p : y <= z) : z --> x <= y --> x
    => exponent-left (meet-monotone-partial p <=∘ eval)

  \lemma -->_join {x y z : E} : x ∨ y --> z = (x --> z) ∧ (y --> z)
    => <=-antisymmetric (meet-univ (_-->-antimonotone join-left) (_-->-antimonotone join-right)) $ exponent-left $
        ldistr>= <=∘ join-univ (meet-monotone meet-left <=-refl <=∘ eval) (meet-monotone meet-right <=-refl <=∘ eval)

  \lemma double-->-increasing {x y : E} : x <= (x --> y) --> y => exponent-left modus-ponens

  \lemma double-->-idempotent {x y : E} : (((x --> y) --> y) --> y) --> y <= (x --> y) --> y
    => exponent-left (meet-monotone-partial double-->-increasing <=∘ eval)

  \lemma double-->-monotone {x y z : E} (p : y <= z) : continuation x y <= continuation x z
    => exponent-left (meet-monotone-partial (_-->-antimonotone p) <=∘ eval)

  \use \lemma exponent-adj-unit {x y : E} : x <= y --> x ∧ y => exponent-left <=-refl

  \use \lemma adj-lemma {x y z : E} (f : x <= z --> y) : x ∧ z <= y => meet-monotone-partial' f <=∘ eval

  \use \func exponent-functor (X : E) : Functor \this \this \cowith
    | F Y => X --> Y
    | Func f => -->-monotone f
    | Func-id => idp
    | Func-o => idp

  \default exp (Y : E) : RightAdjoint \this \this \cowith
    | LAdj => bprodFunctorRight Y
    | Functor => exponent-functor Y
    | eta {
      | trans X => exponent-adj-unit
      | natural f => idp
    }
    | epsilon {
      | trans X => eval
      | natural f => idp
    }
    | eta_epsilon-left => idp
    | eta_epsilon-right => idp
}