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

\class HeytingAlebra \extends BoundedDistributiveLattice {
  | \infixr  --> : E -> E -> E
  | <=-curry {x a b : E} : x ∧ a <= b -> x <= a --> b
  | <=-uncurry {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 => <=-curry meet-right
  \default ldistr>= {x y z : E} : x ∧ (y ∨ z) <= (x ∧ y) ∨ (x ∧ z) => meet-comm =<= <=-uncurry (join-univ (<=-curry (meet-comm =<= join-left)) (<=-curry (meet-comm =<= join-right)))

  \lemma <=-eval {x y : E} : (x --> y) ∧ x <= y
    => <=-uncurry <=-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
    => <=-curry $ (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-inverse {x y : E} (p : x <= y) : neg y <= neg x
    => <=-curry $ meet-monotone <=-refl p <=∘ <=-eval

  \lemma neg_bottom : neg bottom = top
    => <=-antisymmetric TopMeetSemilattice.top-univ (<=-curry 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-exponent-increasing

  \lemma neg_join {x y : E} : neg (x ∨ y) = neg x ∧ neg y
    => exponent_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-exponent-monotone meet-left <=∘ xn) (double-exponent-monotone meet-right <=∘ yn)

  \lemma neg-negated {x : E} : IsNegated (neg x)
    => exponent-monotone double-exponent-increasing <=-refl

  \protected \func curry {x y z : E} : x ∧ y --> z = x --> (y --> z)
    => <=-antisymmetric (<=-curry $ <=-curry $ meet-assoc =<= <=-eval) (<=-curry $ inv meet-assoc =<= meet-monotone <=-eval <=-refl <=∘ <=-eval)

  \lemma top_exponent {x y : E} (p : x <= y) : top <= x --> y
    => <=-curry (meet-right <=∘ p)

  \lemma exponent-monotone {x y x' y' : E} (p : x' <= x) (q : y <= y') : x --> y <= x' --> y'
    => <=-curry $ meet-monotone <=-refl p <=∘ <=-eval <=∘ q

  \lemma exponent_meet {x y z : E} : x --> y ∧ z = (x --> y) ∧ (x --> z)
    => <=-antisymmetric (meet-univ (exponent-monotone <=-refl meet-left) (exponent-monotone <=-refl meet-right)) (<=-curry (meet-univ (meet-monotone meet-left <=-refl <=∘ <=-eval) (meet-monotone meet-right <=-refl <=∘ <=-eval)))

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

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

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

  \lemma double-exponent-monotone {x y z : E} (p : y <= z) : continuation x y <= continuation x z
    => <=-curry (meet-monotone <=-refl (exponent-monotone p <=-refl) <=∘ <=-eval)

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

  \func exponent-functor (x : E) : Functor \this \this \cowith
    | F y => x --> y
    | Func f => exponent-monotone <=-refl f
    | Func-id => idp
    | Func-o => idp

  \func toCCC : CartesianClosedPrecat \cowith
    | CartesianPrecat => \this
    | CHom => -->
    | CHom-eval => <=-eval
    | CHom-univ => inP \new QEquiv {
      | ret => <=-curry
      | ret_f p => prop-pi
      | f_sec p => prop-pi
    }
}