Require Import base protype ordtype clat frame mono adj.

Class is_continuous {X Y : clat} (f : X -> Y) := mk_is_continuous {
  radj_of_cont : Y -> X;
  cont_is_adjunction :> is_adjunction f radj_of_cont;
  contT : f ⊤ = ⊤;
  contM : forall x y, f (x ∧ y) = (f x ∧ f y)
}.

Section ContCLat.
  Context {X Y : clat} (f : X -> Y) {fP : is_continuous f}.
  Implicit Types (x y : X).

  Lemma contB : f ⊥ = ⊥.
  Proof. exact: adjB. Qed.

  Lemma contJ x y : f (x ∨ y) = (f x ∨ f y).
  Proof. exact: adjJ. Qed.

  Lemma contE I (F : I -> X) : f (∃ i, F i) = ∃ i, f (F i).
  Proof. exact: adjE. Qed.

  Lemma contEc I (P : I -> Prop) (F : I -> X) :
    f (∃ i | P i, F i) = ∃ i | P i, f (F i).
  Proof. exact: adjEc. Qed.
End ContCLat.

Section ContFrame.
  Context {X Y : frame} (f : X -> Y) {fP : is_continuous f}.

  Global Instance cont_is_adjunction_frame : is_adjunction f radj_of_cont.
  Proof. exact: cont_is_adjunction. Qed.

  Lemma contH x y : f (x → y) ≤ (f x → f y).
  Proof. apply: impI. by rewrite -contM impEr. Qed.

  Hypothesis is_embedding : forall x, f (f^* x) = x.

  Lemma cont_embH x y : f^* (x → y) = (f^* x → f^* y).
  Proof.
    apply: le_eq. exact: adjH. apply/adjP. apply: impI.
    rewrite -{2}[x]is_embedding -contM impEr. exact: adj_counit.
  Qed.
End ContFrame.