Require Import base order.

Section AdjunctionType.
  Variable (X Y : proType).

  Definition is_adjunction (f : X -> Y) (g : Y -> X) :=
    forall x y, (f x <= y) <-> (x <= g y).

  Structure adjunction_type := mk_adjunction_type {
    lower_adjoint :> X -> Y;
    upper_adjoint : Y -> X;
    _ : is_adjunction lower_adjoint upper_adjoint
  }.

  Definition adjunction_of of phant (X -> Y) := adjunction_type.
  Identity Coercion type_of_adjunction: adjunction_of >-> adjunction_type.
End AdjunctionType.

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

(* Make adjunction into a type class.
   The packaging function adj uses type class inference to come up with the missing argument. *)
Existing Class is_adjunction.
Definition adj {X Y : proType} (f : X -> Y) {g : Y -> X} {h : is_adjunction f g} :
  {adj X -> Y} := mk_adjunction_type h.
Arguments adj {X Y} f {g h}.

(* In the reverse direction we can infer that a packaged adjunction is an adjunction. *)
Instance is_adjunction_proj {X Y : proType} (f : {adj X -> Y}) :
  is_adjunction f (upper_adjoint f) := let: mk_adjunction_type _ _ h := f in h.

Definition upper_adjoint_proj {X Y : proType} (f : X -> Y)
  {g : Y -> X} {h : is_adjunction f g} : Y -> X := g.
Notation "f ^*" := (@upper_adjoint_proj _ _ f _ _) (at level 8, format "f ^*") : ord_scope.

Lemma adjP {X Y : proType} (f : X -> Y) {g : Y -> X} {h : is_adjunction f g} x y :
  f x <= y <-> x <= g y.
Proof. by []. Qed.

(* The lemmas are stated about the unbundled structures, with type class
   inference for the missing arguments. *)

Section LeftAdjoints.
  Variables (X Y : proType) (f : X -> Y).
  Context {g : Y -> X} {adjP : is_adjunction f g}.

  Lemma adj_unit x : x <= f^* (f x).
  Proof. by rewrite -adjP. Qed.

  Global Instance adj_monoL : monotone f.
  Proof.
    move=> x y lxy. rewrite adjP. apply: le_trans lxy _. exact: adj_unit.
  Qed.

  Global Instance ladjoint_proper : Proper (ord_op ++> ord_op) f. exact _. Qed.

  Lemma adj_lub I (F : I -> X) x :
    is_lub F x -> is_lub (f \o F) (f x).
  Proof.
    move=> lub y. rewrite adjP lub. split=> ub i /=. by rewrite adjP.
    rewrite -adjP. exact: ub.
  Qed.
End LeftAdjoints.

Instance dual_adjunction {X Y : proType} (f : X -> Y) {g : Y -> X} (h : is_adjunction f g) :
  @is_adjunction (reverse_proType Y) (reverse_proType X) g f.
Proof. move=> x y. by rewrite !rev_leE h. Qed.

Definition adj_dual {X Y : proType} (f : {adj X -> Y}) :
  {adj Y^r -> X^r} := adj (f^* : Y^r -> X^r).

Section RightAdjoints.
  Variables (X Y : proType) (f : X -> Y).
  Context {g : Y -> X} {adjP : is_adjunction f g}.
  Let gr := g : Y^r -> X^r.

  Lemma adj_counit x : f (f^* x) <= x.
  Proof. exact: (@adj_unit _ _ gr). Qed.

  Global Instance adj_monoR : monotone g.
  Proof. move=> x y. exact: (@adj_monoL _ _ gr). Qed.

  Global Instance radjoint_proper : Proper (ord_op ++> ord_op) g. exact _. Qed.

  Lemma adj_glb I (F : I -> Y) x :
    is_glb F x -> is_glb (g \o F) (f^* x).
  Proof. exact: (@adj_lub _ _ gr). Qed.
End RightAdjoints.

Arguments adj_counit {X Y} f {g adjP} x.

Section AdjunctionsOrd.
  Variables X Y : ordType.

  Lemma adj_uniqR (f : X -> Y) (g1 g2 : Y -> X)
        (adj1 : is_adjunction f g1) (adj2 : is_adjunction f g2) : g1 = g2.
  Proof.
    wlog suff: g1 g2 adj1 adj2 / g1 <= g2. move=> h. apply: le_eq; exact: h.
    move=> x. exact/adj2/adj1.
  Qed.

  Lemma adj_eq (f g : {adj X -> Y}) : f = g :> (X -> Y) -> f = g.
  Proof.
    move: f g => [f fr adj1] [g gr adj2] /= e. destruct e.
    destruct (adj_uniqR adj1 adj2). f_equal. exact: pi.
  Qed.

  Variable (f : X -> Y).
  Context {g : Y -> X} {adjP : is_adjunction f g}.

  Lemma adj_tripleL x : f^* (f (f^* x)) = f^* x.
  Proof.
    apply: le_eq. apply: mono. exact: adj_counit. by rewrite -adjP.
  Qed.
End AdjunctionsOrd.

Lemma adj_tripleR {X Y : ordType} (f : X -> Y) {g : Y -> X} {fP : is_adjunction f g} x :
  f (f^* (f x)) = f x.
Proof. exact: (@adj_tripleL _ _ (g : Y^r -> X^r)). Qed.

Canonical adj_proType (X Y : proType) :=
  Eval hnf in induced_proType {adj X -> Y} (@lower_adjoint X Y).
Canonical adj_ordType (X Y : ordType) :=
  Eval hnf in induced_ordType {adj X -> Y} (@adj_eq X Y).

Section AdjunctionsCategory.
  Variables (X Y Z : proType) (f : X -> Y) (g : Y -> Z).
  Context {fr : Y -> X} {fP : is_adjunction f fr}.
  Context {gr : Z -> Y} {gP : is_adjunction g gr}.

  Global Instance is_adjunction_comp : is_adjunction (g \o f) (fr \o gr).
  Proof. move=> x y. by rewrite/=!adjP. Qed.

  Global Instance is_adjunction_id : is_adjunction (@id X) (@id X).
  Proof. by []. Qed.
End AdjunctionsCategory.

Definition is_closure {X : proType} (f : X -> X) := forall x y, (f x <= f y) <-> (x <= f y).
Existing Class is_closure.

Section ClosureType.
  Variable (X : proType).

  Structure closure_type := mk_closure_type {
    closure_op :> X -> X;
    _ : is_closure closure_op
  }.

  Definition closure_of of phant (X -> X) := closure_type.
  Identity Coercion type_of_closure : closure_of >-> closure_type.
End ClosureType.

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

Definition mk_closure {X : proType} (f : X -> X) {fP : is_closure f} := mk_closure_type fP.
Arguments mk_closure {X} f {fP}.

Instance closure_is_closure {X : proType} (f : {closure X -> X}) : is_closure f :=
  let: mk_closure_type _ fP := f in fP.

Section ClosureOperatorsProType.
  Variables (X : proType) (c : X -> X).
  Context {clP : is_closure c}.

  Lemma closureP x y : (c x <= c y) <-> (x <= c y). exact: clP. Qed.

  Lemma closure_inc x : x <= c x.
  Proof. by rewrite -closureP. Qed.

  Global Instance closure_mono : monotone c.
  Proof.
    move=> x y le_x_y. rewrite closureP. rewrite le_x_y. exact: closure_inc.
  Qed.

  Global Instance closure_proper : Proper (ord_op ++> ord_op) c. exact _. Qed.
End ClosureOperatorsProType.

Lemma closure_op_eq {X : proType} (c d : {closure X -> X}) : c = d :> (X -> X) -> c = d.
Proof. move: c d => [f p] [g q] /=. destruct 1. f_equal. exact: pi. Qed.

Section ClosureOperatorsOrdType.
  Variable (X : ordType) (c : X -> X).
  Context {clP : is_closure c}.

  Lemma closure_idem x : c (c x) = c x.
  Proof. apply: le_eq. by rewrite closureP. exact: closure_inc. Qed.

  Lemma closure_eq x y : x <= c y -> y <= c x -> c x = c y.
  Proof. move=> lxy lyx. apply: le_eq; by rewrite closureP. Qed.

  Lemma closure_stable x : c x <= x -> c x = x.
  Proof. move=> h. apply: le_eq h _. exact: closure_inc. Qed.

  Lemma closure_lub T (f : T -> X) x y :
    is_lub (c \o f) x -> is_lub f y -> c x = c y.
  Proof.
    move=> lub1 lub2. apply: closure_eq.
    - rewrite lub1 => i /=. apply: mono. exact: ubP lub2.
    - rewrite lub2 => i. rewrite -closureP -[c x]closure_inc. exact: ubP lub1.
  Qed.

  Lemma closure_glb T (f : T -> X) x :
    is_glb (c \o f) x -> c x = x.
  Proof.
    move=> glb. apply: closure_stable. apply: glbP (glb) _ => i /=.
    rewrite closureP. exact: lbP glb.
  Qed.
End ClosureOperatorsOrdType.

Canonical closure_proType (X : proType) :=
  Eval hnf in induced_proType {closure X -> X} (@closure_op X).
Canonical closure_ordType (X : ordType) :=
  Eval hnf in induced_ordType {closure X -> X} (@closure_op_eq X).

Instance unit_closure {X Y : proType} (f : X -> Y) {g : Y -> X} {fP : is_adjunction f g} :
  is_closure (f^* \o f).
Proof.
  move=> x y /=. split=> [<-|e]. exact: adj_unit. apply: mono. by rewrite adjP.
Qed.

Definition unit {X Y : ordType} (f : X -> Y) {g : Y -> X} {fP : is_adjunction f g} :
  {closure X -> X} := mk_closure (f^* \o f).

Definition is_kernel {X : proType} (f : X -> X) := forall x y, (f x <= f y) <-> (f x <= y).
Existing Class is_kernel.

Section KernelType.
  Variable (X : proType).

  Structure kernel_type := mk_kernel_type {
    kernel_op :> X -> X;
    _ : is_kernel kernel_op
  }.

  Definition kernel_of of phant (X -> X) := kernel_type.
  Identity Coercion type_of_kernel : kernel_of >-> kernel_type.
End KernelType.

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

Definition mk_kernel {X : proType} (f : X -> X) {fP : is_kernel f} := mk_kernel_type fP.
Arguments mk_kernel {X} f {fP}.

Instance kernel_is_kernel {X : proType} (f : {kernel X -> X}) : is_kernel f :=
  let: mk_kernel_type _ fP := f in fP.

(* Closure and kernel operators are dual concepts. *)
(* Do *not* add the reverse instances (from {closure X^r -> X^r} to {kernel X -> X})
   unless you want typeclass inference to diverge... *)
Instance closure_to_kernel {X : proType} (f : X -> X) {fP : is_closure f} :
  is_kernel (f : X^r -> X^r) := fun x y => fP y x.

Instance kernel_to_closure {X : proType} (f : X -> X) {fP : is_kernel f} :
  is_closure (f : X^r -> X^r) := fun x y => fP y x.

Section KernelOperators.
  Variables (X : proType) (c : X -> X).
  Context {cP : is_kernel c}.
  Implicit Types (x y z : X).
  Let k : X^r -> X^r := c.

  Lemma kernelP x y : (c x <= c y) <-> (c x <= y). by []. Qed.

  Lemma kernel_dec x : c x <= x.
  Proof. exact: (@closure_inc _ k). Qed.

  Global Instance kernel_mono : monotone c.
  Proof. move=> x y. exact: (@closure_mono _ k). Qed.

  Global Instance kernel_proper : Proper (ord_op ++> ord_op) c. exact _. Qed.
End KernelOperators.

Lemma kernel_op_eq {X : proType} (c d : {kernel X -> X}) : c = d :> (X -> X) -> c = d.
Proof. move: c d => [f p] [g q] /=. destruct 1. f_equal. exact: pi. Qed.

Section KernelOperationsOrder.
  Variable (X : ordType) (c : X -> X).
  Context {cP : is_kernel c}.
  Implicit Types (x y z : X).
  Let k : X^r -> X^r := c.

  Lemma kernel_idem x : c (c x) = c x.
  Proof. exact: (@closure_idem _ k). Qed.

  Lemma kernel_eq x y : c x <= y -> c y <= x -> c x = c y.
  Proof. move=> h1 h2. exact: (@closure_eq _ k). Qed.

  Lemma kernel_stable x : x <= c x -> c x = x.
  Proof. exact: (@closure_stable _ k). Qed.

  Lemma kernel_glb I (f : I -> X) x y :
    is_glb (c \o f) x -> is_glb f y -> c x = c y.
  Proof. exact: (@closure_lub _ k). Qed.

  Lemma kernel_lub I (f : I -> X) x :
    is_lub (c \o f) x -> c x = x.
  Proof. exact: (@closure_glb _ k). Qed.
End KernelOperationsOrder.

Canonical kernel_proType (X : proType) :=
  Eval hnf in induced_proType {kernel X -> X} (@kernel_op X).
Canonical kernel_ordType (X : ordType) :=
  Eval hnf in induced_ordType {kernel X -> X} (@kernel_op_eq X).

Instance counit_kernel {X Y : proType} (f : X -> Y) {g : Y -> X} {fP : is_adjunction f g} :
  is_kernel (f \o f^*).
Proof. move=> x y. exact: (unit_closure (f^* : Y^r -> X^r)). Qed.

Definition counit {X Y : ordType} (f : {adj X -> Y}) : {kernel Y -> Y} :=
  mk_kernel (f \o f^*).