Require Import base
  protype ordtype clat frame
  mono adj cont
  prod.

Polymorphic Cumulative Record mfun_type (X Y : proType) := mfun {
  monofun :> X -> Y;
  monotone_monofun : monotone monofun
}.

Section MFun.
  Variable (X Y : proType).
  Definition mfun_of of phant (X -> Y) := mfun_type X Y.
  Identity Coercion type_of_mfun : mfun_of >-> mfun_type.
End MFun.
Arguments mfun {X Y} f {fP} : rename.

Notation "{ 'mono' fT }" := (mfun_of (Phant fT))
  (at level 0, format "{ 'mono' '[hv' fT ']' }") : type_scope.

Instance mfun_monotone {X Y : proType} (f : {mono X -> Y}) : monotone f :=
  monotone_monofun f.
Instance mfun_proper {X Y : proType} (f : {mono X -> Y}) : Proper (ord_op ++> ord_op) f :=
  monotone_monofun f.

Definition mk_mfun {X Y : proType} (f : X -> Y) {H : forall x y : X, x ≤ y -> f x ≤ f y} :
  {mono X -> Y} := @mfun X Y f H.
Arguments mk_mfun {X Y} f H.

Lemma mfun_eq (X Y : proType) (f g : {mono X -> Y}) :
  f = g :> (X -> Y) -> f = g.
Proof.
  destruct f, g => /= eqn. destruct eqn. f_equal. exact: pi.
Qed.

Canonical mfun_proType (X Y : proType) :=
  Eval hnf in InducedProType {mono X -> Y} (@monofun X Y).

Canonical mfun_ordType (X : proType) (Y : ordType) :=
  Eval hnf in InducedOrdType {mono X -> Y} (@mfun_eq X Y).

Lemma mfun_leE (X Y : proType) (f g : {mono X -> Y}) :
  (f ≤ g) = (forall x, f x ≤ g x).
Proof. by []. Qed.

Global Instance monofun_is_proper {X Y : proType} :
  Proper (ord_op ++> ord_op) (@monofun X Y : {mono X -> Y} -> X -> Y).
Proof. move=> f g le_f_g x /=. exact: le_f_g. Qed.

Section MFunCLat.
  Variables (X : proType) (Y : clat).
  Implicit Types (f g h : {mono X -> Y}) (x : X).

  Program Definition mfun_inf I (F : I -> {mono X -> Y}) : {mono X -> Y} :=
    mk_mfun (fun x => inf (F^~ x)) _.
  Next Obligation. apply: all_mono => i. exact: mono. Qed.

  Lemma mfun_infP I (F : I -> {mono X -> Y}) : is_glb F (mfun_inf F).
  Proof.
    apply: mk_glb => [i|g h1] x /=. exact: allE. focus=> i. exact: h1.
  Qed.

  Canonical mfun_clatMixin := CLatMixin mfun_infP.
  Canonical mfun_clat := Eval hnf in CLat {mono X -> Y} mfun_clatMixin.

  Program Definition mceil (f : X -> Y) : {mono X -> Y} :=
    mk_mfun (fun x => ∃ y | y ≤ x, f y) _.
  Next Obligation.
    focus=> z le_z_x. apply: exIc (z) _ le_refl. by rewrite le_z_x.
  Qed.

  Program Definition mfloor (f : X -> Y) : {mono X -> Y} :=
    mk_mfun (fun x => ∀ y | x ≤ y, f y) _.
  Next Obligation.
    focus=> z le_y_z. apply: allEc (z) _ le_refl. by rewrite -le_y_z.
  Qed.

  Global Instance mceil_is_adjunction :
    is_adjunction mceil (@monofun X Y : {mono X -> Y} -> X -> Y).
  Proof.
    move=>/= f g. split=> [<-|le_f_g]x/=.
    exact: exIc (x) _ _. by focus=> y <-.
  Qed.

  Global Instance mfloor_is_adjunction :
    is_adjunction (@monofun X Y : {mono X -> Y} -> X -> Y) mfloor.
  Proof.
    move=>/= f g. split=> [le_f_g|->]x/=.
    by focus=> y ->. exact: allEc (x) _ _.
  Qed.

  Lemma mfun_topE x : (⊤ : {mono X -> Y}) x = ⊤.
  Proof. by rewrite adjT prod_topE. Qed.

  Lemma mfun_botE x : (⊥ : {mono X -> Y}) x = ⊥.
  Proof. by rewrite adjB prod_botE. Qed.

  Lemma mfun_joinE f g x : (f ∨ g) x = (f x ∨ g x).
  Proof. by rewrite adjJ prod_joinE. Qed.

  Lemma mfun_meetE f g x : (f ∧ g) x = (f x ∧ g x).
  Proof. by rewrite adjM prod_meetE. Qed.

  Lemma mfun_exE I (G : I -> {mono X -> Y}) x : (∃ i, G i) x = ∃ i, G i x.
  Proof. by rewrite adjE prod_exE. Qed.

  Lemma mfun_allE I (G : I -> {mono X -> Y}) x : (∀ i, G i) x = ∀ i, G i x.
  Proof. by []. Qed.
End MFunCLat.

Section MFunFrame.
  Variables (X : proType) (Y : frame).
  Implicit Types (f g h : {mono X -> Y}) (x : X).

  Lemma mfun_frameP I (F : I -> {mono X -> Y}) f :
    f ∧ (∃ i, F i) ≤ ∃ i, f ∧ F i.
  Proof.
    rewrite mfun_leE => x. rewrite mfun_meetE !mfun_exE meetxE.
    apply: ex_mono => i. by rewrite mfun_meetE.
  Qed.

  Canonical mfun_frameMixin := FrameMixin mfun_frameP.
  Canonical mfun_frame := Eval hnf in Frame {mono X -> Y} mfun_frameMixin.

  Lemma mfun_impE f g x : (f → g) x = ∀ y | x ≤ y, f y → g y.
  Proof.
    suff->: (f → g) = mfloor (fun x => f x → g x) => //{x}. apply: imp_def.
    - rewrite mfun_leE => x. rewrite mfun_meetE/mfloor/=.
      apply/impP. exact: allEc (x) _ _.
    - move=> /= h le_hf_g. rewrite -mfloor_is_adjunction => x.
      apply/impP. rewrite mfun_leE in le_hf_g. move: (le_hf_g x).
      rewrite mfun_meetE. exact.
  Qed.
End MFunFrame.