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

Section PresheafType.
  Variable (X : proType).
  Definition presheaf_type : Type := {mono X^r -> Prop}.
  Definition presheaf_of of phant X := presheaf_type.
  Identity Coercion type_of_presheaf : presheaf_of >-> presheaf_type.
  Identity Coercion mfun_of_presheaf : presheaf_type >-> mfun_of.
End PresheafType.

Notation presheaf X := (presheaf_of (Phant X)).

Section PresheafLaws.
  Variable (X : proType).
  Implicit Types (p q : presheaf X) (x y : X).

  Lemma presheaf_leE p q : (p ≤ q) = (forall x : X, p x -> q x).
  Proof. by []. Qed.

  Lemma presheaf_botE x : (bot : presheaf X) x = False.
  Proof. by rewrite mfun_botE prop_botE. Qed.

  Lemma presheaf_topE x : (top : presheaf X) x = True.
  Proof. by rewrite mfun_topE prop_topE. Qed.

  Lemma presheaf_joinE p q x : (p ∨ q) x = (p x \/ q x).
  Proof. by rewrite mfun_joinE prop_joinE. Qed.

  Lemma presheaf_meetE p q x : (p ∧ q) x = (p x /\ q x).
  Proof. by rewrite mfun_meetE prop_meetE. Qed.

  Lemma presheaf_exE I (F : I -> presheaf X) x :
    (sup F) x = exists i, F i x.
  Proof. by rewrite mfun_exE prop_exE. Qed.

  Lemma presheaf_allE I (F : I -> presheaf X) x :
    (inf F) x = forall i, F i x.
  Proof. by []. Qed.

  Lemma presheaf_exEc I (P : I -> Prop) (F : I -> presheaf X) x :
    (∃ i | P i, F i) x = exists i, P i /\ F i x.
  Proof.
    rewrite presheaf_exE; f_equal; fext=> i.
    rewrite presheaf_exE. apply: pext; by firstorder.
  Qed.

  Lemma presheaf_allEc I (P : I -> Prop) (F : I -> presheaf X) x :
    (∀ i | P i, F i) x = forall i, P i -> F i x.
  Proof. by []. Qed.

  Lemma presheaf_impE p q x :
    (p → q) x = forall y, y ≤ x -> p y -> q y.
  Proof.
    rewrite mfun_impE prop_allEc. fext=> y. by rewrite prop_impE.
  Qed.

  Lemma presheafP p x y :
    x ≤ y -> p y -> p x.
  Proof.
    move=> le_x_y. rewrite -prop_leE. apply: monotone_monofun. exact: le_x_y.
  Qed.
End PresheafLaws.

Section Yoneda.
  Variable (X : proType).
  Implicit Types (x y z : X).

  Definition yo (x : X) : presheaf X :=
    mk_mfun (fun y : X^r => y ≤ x :> X)
            (fun y z le_z_y le_y_x => le_trans y le_z_y le_y_x).

  Lemma yoneda (x : X) (p : presheaf X) :
    (yo x ≤ p) = p x.
  Proof.
    apply: pext => h. apply: h. exact: le_refl.
    move=> y le_x_y. apply: presheafP h. exact: le_x_y.
  Qed.

  Lemma presheaf_representables (p : {mono X^r -> Prop}) :
    p = ∃ x | p x, yo x.
  Proof.
    apply: le_eq.
    - hnf=> x; hnf=> px. rewrite presheaf_exEc. exists x. split=>//. exact: le_refl.
    - focus=> x; hnf=> px; hnf=> y; hnf=> le_x_y. apply: presheafP px. exact: le_x_y.
  Qed.

  Global Instance monotone_yo : monotone yo.
  Proof. move=> x y le_x_y. rewrite yoneda. exact: le_x_y. Qed.

  Lemma yo_embedding x y : yo x ≤ yo y -> x ≤ y.
  Proof. apply. exact: le_refl. Qed.

  Lemma yo_limit {T} (F : T -> X) x :
    is_glb F x -> is_glb (yo \o F) (yo x).
  Proof.
    move=> h. apply: mk_glb.
    - move=> y z /= ->. exact: lbP h.
    - move=> /= p h2 y /= py. apply/h => i. exact: h2.
  Qed.
End Yoneda.

Section YonedaOrd.
  Variable (X : ordType).

  Lemma yo_injective : injective (@yo X).
  Proof.
    move=> x y eqn. apply: le_eq; apply: yo_embedding; by rewrite eqn.
  Qed.
End YonedaOrd.

Section YonedaClat.
  Variable (X : clat).
  Implicit Types (x y z : X).

  Lemma yo_inf {T} (F : T -> X) : (∀ i, yo (F i)) = yo (inf F).
  Proof.
    apply: le_eq. hnf=>/=y; hnf=> h. apply: allI => i. exact: h.
    focus=> i. rewrite yoneda. rewrite/yo/=. exact: allE.
  Qed.

  Lemma yo_top : yo (⊤ : X) = ⊤.
  Proof.
    apply: top_eq. hnf=> x; hnf=> _. exact: topI.
  Qed.

  Lemma yo_meet x y : yo (x ∧ y) = (yo x ∧ yo y).
  Proof.
    apply: le_eq. focus; rewrite yoneda. exact: meetEl. exact: meetEr.
    move=> z. rewrite mfun_meetE prop_meetE; hnf=> -[le_x_z le_y_z].
    exact: meetI.
  Qed.
End YonedaClat.