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

Definition Cover (X : Type) := X -> Prop.
Definition cover_le {X : proType} (U V : Cover X) :=
  forall x, U x -> exists2 y, V y & x ≤ y.

Lemma cover_le_refl {X : proType} (U : Cover X) : cover_le U U.
Proof. move=> x uy. by exists x. Qed.

Lemma cover_le_trans {X : proType} (U V W : Cover X) : cover_le U V -> cover_le V W -> cover_le U W.
Proof.
  move=> le_u_v le_v_w a /le_u_v[b /le_v_w[c wc le_b_c] le_a_b].
  exists c => //. by transitivity b.
Qed.

Canonical cover_proMixin (X : proType) :=
  Eval hnf in ProMixin (@cover_le_refl X) (@cover_le_trans X).
Canonical cover_proType (X : proType) :=
  Eval hnf in ProType (Cover X) (cover_proMixin X).

Lemma cover_sup {X : clat} (U V : Cover X) :
  U ≤ V -> ∃ x | U x, x ≤ ∃ y | V y, y.
Proof.
  move=> le_u_v. focus=> x /le_u_v[]. exact: exIc.
Qed.

Definition basis (X : Type) := X -> Cover X -> Prop.

Structure basis_pred (X : proType) := mk_basis_pred {
  basis_cov :> X -> Cover X -> Prop;
  _ : forall U x y, basis_cov x U -> U y -> y ≤ x;
  _ : forall V x y, basis_cov y V -> x ≤ y -> exists2 U, basis_cov x U & U ≤ V
}.

Section BasisLaws.
  Variable (X : proType) (cov : basis_pred X).

  Lemma basisE U x y : cov x U -> U y -> y ≤ x.
  Proof. by case: cov U x y. Qed.

  Lemma basisP V x y : cov y V -> x ≤ y -> exists2 U, cov x U & U ≤ V.
  Proof. by case: cov V x y. Qed.
End BasisLaws.

Definition is_sheaf {X : proType} (cov : basis X) (p : presheaf X) :=
  forall U x, cov x U -> (forall y, U y -> p y) -> p x.

Structure sheaf {X : proType} (cov : basis X) : Type := mk_sheaf {
  presheaf_of_sheaf :> presheaf X;
  _ : is_sheaf cov presheaf_of_sheaf
}.

Lemma sheafP {X : proType} {cov : basis X} (p : sheaf cov) : is_sheaf cov p.
Proof. by case: p. Qed.

Lemma sheaf_eq {X : proType} {cov : basis X} (p q : sheaf cov) :
  p = q :> presheaf X -> p = q.
Proof.
  destruct p, q => /= eqn. destruct eqn. f_equal. exact: pi.
Qed.

Canonical sheaf_proType (X : proType) (cov : basis X) :=
  Eval hnf in InducedProType (sheaf cov) (@presheaf_of_sheaf X cov).

Canonical sheaf_ordType (X : proType) (cov : basis X) :=
  Eval hnf in InducedOrdType (sheaf cov) (@sheaf_eq X cov).

Lemma sheaf_leE (X : proType) (cov : basis X) (p q : sheaf cov) :
  (p ≤ q) = (forall x : X, p x -> q x).
Proof. by []. Qed.

Instance presheaf_of_sheaf_monotone (X : proType) (cov : basis X) :
  monotone (@presheaf_of_sheaf X cov).
Proof. by []. Qed.

Section SheafCLat.
  Variable (X : proType) (cov : basis X).

  Lemma is_sheaf_inf_closed I (F : I -> presheaf X) :
    (forall i, is_sheaf cov (F i)) -> is_sheaf cov (∀ i, F i).
  Proof.
    move=> h1 U x cx h2. rewrite presheaf_allE => i.
    apply: h1 cx _ => y /h2. exact.
  Qed.

  Program Definition sheaf_inf I (F : I -> sheaf cov) : sheaf cov :=
    @mk_sheaf _ _ (inf (F : I -> presheaf X)) _.
  Next Obligation.
    apply: is_sheaf_inf_closed => i. exact: sheafP.
  Qed.

  Lemma sheaf_infP I (F : I -> sheaf cov) : is_glb F (sheaf_inf F).
  Proof.
    apply: mk_glb => [i|g h1] x /=. exact: allE. focus=> i. exact: h1.
  Qed.

  Canonical sheaf_clatMixin := CLatMixin sheaf_infP.
  Canonical sheaf_clat := Eval hnf in CLat (sheaf cov) sheaf_clatMixin.

  Definition sheafify (p : presheaf X) : sheaf cov :=
    ∀ q : sheaf cov | p ≤ q :> presheaf X, q.

  Global Instance sheafify_adj :
    is_adjunction sheafify (@presheaf_of_sheaf X cov).
  Proof.
    move=> p q. split=> [<-|le_p_q]. apply: allIc => r.
    exact: le_trans. exact: allEc (q) _ _.
  Qed.

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

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

  Lemma sheaf_topE (x : X) : (⊤ : sheaf cov) x = True.
  Proof. by rewrite adjT presheaf_topE. Qed.

  Lemma sheaf_meetE (p q : sheaf cov) (x : X) :
    (p ∧ q) x = (p x /\ q x).
  Proof. by rewrite adjM presheaf_meetE. Qed.

  Lemma sheafifyB : sheafify ⊥ = ⊥.
  Proof. exact: adjB. Qed.

  Lemma sheafifyJ (p q : presheaf X) :
    sheafify (p ∨ q) = (sheafify p ∨ sheafify q).
  Proof. exact: adjJ. Qed.

  Lemma sheafifyE I (F : I -> presheaf X) :
    sheafify (sup F) = ∃ i, sheafify (F i).
  Proof. exact: adjE. Qed.

  Lemma sheafifyEc I (P : I -> Prop) (F : I -> presheaf X) :
    sheafify (∃ i | P i, F i) = ∃ i | P i, sheafify (F i).
  Proof. exact: adjEc. Qed.

  Lemma sheafifyT : sheafify ⊤ = ⊤.
  Proof.
    apply: top_eq. rewrite/sheafify. focus=> p.
    rewrite presheaf_leE sheaf_leE => le x _.
    exact: le.
  Qed.

  Lemma sheafify_inc (p : presheaf X) : p ≤ sheafify p.
  Proof. exact: adj_unit. Qed.

  Lemma sheafify_idem (p : sheaf cov) :
    sheafify p = p.
  Proof.
    apply: le_eq. exact/adjP. exact: sheafify_inc.
  Qed.

  Lemma sheafify_is_sheaf (p : presheaf X) (x : X) :
    is_sheaf cov p -> sheafify p x = p x.
  Proof.
    move=> H. suff->: sheafify p = mk_sheaf H by [].
    exact: (@sheafify_idem (mk_sheaf H)).
  Qed.

  Lemma sheaf_bot_sheafify : ⊥ = sheafify ⊥.
  Proof. by rewrite sheafifyB. Qed.

  Lemma sheaf_join_sheafify (p q : sheaf cov) :
    (p ∨ q) = sheafify ((p : presheaf X) ∨ q).
  Proof. by rewrite sheafifyJ !sheafify_idem. Qed.

  Lemma sheaf_ex_sheafify I (F : I -> sheaf cov) :
    (∃ i, F i) = sheafify (∃ i, (F i : presheaf X)).
  Proof.
    rewrite sheafifyE. f_equal; fext=> i. by rewrite sheafify_idem.
  Qed.

  Lemma sheaf_exc_sheafify I (P : I -> Prop) (F : I -> sheaf cov) :
    (∃ i | P i, F i) = sheafify (∃ i | P i, (F i : presheaf X)).
  Proof.
    rewrite sheafifyEc. f_equal; fext=> i. f_equal. by rewrite sheafify_idem.
  Qed.

  Lemma sheaf_joinI (p q : sheaf cov) (x : X) :
    (p x \/ q x) -> (p ∨ q) x.
  Proof.
    move=> H. rewrite sheaf_join_sheafify. apply: sheafify_inc.
      by rewrite presheaf_joinE.
  Qed.

  Lemma sheaf_exI I (F : I -> sheaf cov) (x : X) :
    (exists i, F i x) -> (∃ i, F i) x.
  Proof.
    move=> H. rewrite sheaf_ex_sheafify. apply: sheafify_inc.
      by rewrite presheaf_exE.
  Qed.

  Lemma sheaf_exIc I (P : I -> Prop) (F : I -> sheaf cov) (x : X) :
    (exists2 i, P i & F i x) -> (∃ i | P i, F i) x.
  Proof.
    move=> [i pi fi]. apply: sheaf_exI. exists i.
    apply: sheaf_exI. by exists pi.
  Qed.

  Definition embed (x : X) : sheaf cov :=
    sheafify (yo x).

  Lemma embedI (x y : X) :
    y ≤ x -> embed x y.
  Proof.
    move=> le_y_x. apply: sheafify_inc. exact: le_y_x.
  Qed.

  Lemma embedE (x : X) (p : sheaf cov) :
    (embed x ≤ p) = p x.
  Proof.
    apply: pext.
    - apply. rewrite/embed. apply: embedI. exact: le_refl.
    - move=> px. rewrite/embed. apply/adjP. by rewrite yoneda.
  Qed.

  Global Instance monotone_embed : monotone embed.
  Proof.
    move=> x y le_x_y. rewrite embedE. apply: embedI. exact: le_x_y.
  Qed.

  Lemma embedT (x : X) :
    (forall y : X, y ≤ x) -> embed x = ⊤.
  Proof.
    move=> xP. apply: top_eq; hnf=> y _. apply: embedI. exact: xP.
  Qed.

  Lemma sheaf_representables (p : sheaf cov) :
    p = ∃ x : X | p x, embed x.
  Proof.
    apply: le_eq; last first. focus=> x px. by rewrite embedE.
    move=> x px. apply: sheaf_exIc. exists x => //. exact: embedI.
  Qed.
End SheafCLat.

Section SheafFrame.
  Variable (X : proType) (cov : basis_pred X).

  Lemma is_sheaf_exponential_ideal (p q : presheaf X) :
    is_sheaf cov q -> is_sheaf cov (p → q).
  Proof.
    move=> h1 U x cx h2. rewrite presheaf_impE => y le_y_x py.
    case: (basisP cx le_y_x) => V cy le_v_u. apply: h1 (cy) _ => z vz.
    case: (le_v_u z vz) => w uw le_z_w. move: (h2 w uw).
    rewrite presheaf_impE. apply=> //. move: py. rewrite -prop_leE.
    apply: monotone_monofun. rewrite rev_leE. exact: basisE cy vz.
  Qed.

  Program Definition sheaf_imp (p : presheaf X) (q : sheaf cov) : sheaf cov :=
    @mk_sheaf _ _ (p → q) _.
  Next Obligation. apply: is_sheaf_exponential_ideal. exact: sheafP. Qed.

  Lemma sheaf_impP (p q : presheaf X) (r : sheaf cov) :
    (p ∧ q ≤ r) <-> (p ≤ sheaf_imp q r).
  Proof. by rewrite impP. Qed.

  Lemma sheaf_frameP I (F : I -> sheaf cov) (p : sheaf cov) :
    p ∧ sup F ≤ ∃ i, p ∧ F i.
  Proof.
    rewrite meetC /ord_op/=/induced_le. rewrite adjM. apply/sheaf_impP.
    change (∃ i, F i ≤ sheaf_imp p (∃ i, p ∧ F i) :> sheaf cov).
    focus=> i. apply/sheaf_impP. rewrite meetC. rewrite -adjM.
    change (p ∧ F i ≤ ∃ i, p ∧ F i :> sheaf cov).
    exact: exI (i) _.
  Qed.

  Canonical sheaf_frameMixin := FrameMixin sheaf_frameP.
  Canonical sheaf_frame := Eval hnf in Frame (sheaf cov) sheaf_frameMixin.

  (* Typeclasses and canonical structures don't play nice, so we have to add this
     instances both for frames and complete lattices. *)
  Global Instance sheafify_adj_frame : is_adjunction (@sheafify X cov) (@presheaf_of_sheaf X cov).
  Proof. exact: sheafify_adj. Qed.

  Lemma presheaf_of_imp (p q : sheaf cov) :
    (p → q) = ((p : presheaf X) → q) :> presheaf X.
  Proof.
    suff->: (p → q) = sheaf_imp (presheaf_of_sheaf p) q. by []. apply: imp_def.
    - rewrite/ord_op/=/induced_le adjM. exact: impEr.
    - move=> /= z le_zx_y. rewrite/ord_op/=/induced_le. apply/impP.
      rewrite -adjM. exact: le_zx_y.
  Qed.

  (*Lemma insub_imp a x : (a → val x) = val (insub a → x).
  Proof.
    apply: le_eq; last first.
    - rewrite val_imp. apply: imp_proper => //. rewrite/flip. exact: insub_inc.
    - rewrite val_imp. apply: impI. rewrite meetC impP /insub valI.
      apply: infE (subtype_imp a x → x) _. rewrite valI. apply: infE.
      + rewrite val_imp SubK. apply: impI. exact: impEl.
      + by rewrite val_imp SubK.
  Qed.*)

  Lemma sheafify_imp_ideal (p : presheaf X) (q : sheaf cov) :
    presheaf_of_sheaf (sheafify cov (p → presheaf_of_sheaf q)) ≤ p → presheaf_of_sheaf q.
  Proof.
    rewrite/sheafify. rewrite adjAc. exact: allEc (sheaf_imp p q) _ _.
  Qed.

  Lemma sheafify_strong (p q : presheaf X) :
    p ∧ sheafify cov q ≤ sheafify cov (p ∧ q).
  Proof.
    rewrite meetC. apply/impP. rewrite -sheafify_imp_ideal.
    apply: mono. apply: mono. apply/impP. rewrite meetC.
    exact: adj_unit.
  Qed.

  Lemma sheafifyM (p q : presheaf X) :
    sheafify cov (p ∧ q) = (sheafify cov p ∧ sheafify cov q).
  Proof.
    apply: le_eq. exact: monoM. rewrite/ord_op/=/induced_le adjM sheafify_strong.
    apply: mono. by rewrite meetC sheafify_strong meetC adj_tripleR.
  Qed.

  Global Instance sheafify_is_continuous : is_continuous (sheafify cov).
  Proof.
    apply: mk_is_continuous. exact: sheafifyT. exact: sheafifyM.
  Qed.

  Lemma sheaf_impE (p q : sheaf cov) (x : X) :
    (p → q) x = forall y : X, y ≤ x -> p y -> q y.
  Proof. by rewrite presheaf_of_imp presheaf_impE. Qed.
End SheafFrame.

Structure sieve {A : proType} (x : A) := mk_sieve {
  sievefun :> presheaf A;
  _ : forall y : A, sievefun y -> y ≤ x
}.
Arguments mk_sieve {A x} f fP : rename.

Lemma sieveP {A : proType} {x : A} (U : sieve x) (y : A) :
  U y -> y ≤ x.
Proof.
  case: U => //= f fP. exact: fP.
Qed.

Lemma sieve_eq {A : proType} {x : A} (U V : sieve x) :
  U = V :> presheaf A -> U = V.
Proof.
  move: U V => [U Up] [V Vp] /= eqn. destruct eqn.
  f_equal. exact: pi.
Qed.

Program Definition sieve_top {A : proType} (x : A) : sieve x :=
  mk_sieve (yo x) _.

Program Definition sieve_bot {A : proType} (x : A) : sieve x :=
  mk_sieve (mk_mfun (fun _ => False) _) _.
Next Obligation. by []. Qed.

Program Definition restrict {A : proType} (U : presheaf A) (x : A) : sieve x :=
  mk_sieve (mk_mfun (fun z : A^r => U z /\ (z ≤ x :> A)) _) _.
Next Obligation.
  move=> [u le]. split. apply: presheafP u. exact: H. by rewrite -le.
Qed.

Lemma restrictE {A : proType} {x : A} (U : sieve x) (y : A) :
  restrict U y ≤ U :> presheaf A.
Proof. by move=> z []. Qed.

Lemma restrictP {A : proType} {x : A} (U : sieve x) (y : A) :
  (forall a : A, U a -> a ≤ y) -> restrict U y = U :> presheaf A.
Proof.
  move=> ub. apply: le_eq. exact: restrictE.
  hnf=> z; hnf=> uz. split=> //. exact: ub.
Qed.

Lemma restrict_refl {A : proType} {x : A} (U : sieve x) :
  restrict U x = U.
Proof.
  apply: sieve_eq. apply: le_eq. exact: restrictE.
  hnf=> y; hnf=> uy. split=> //. exact: sieveP uy.
Qed.

Lemma restrict_top {A : proType} (x y : A) :
  x ≤ y -> restrict (sieve_top y) x = sieve_top x.
Proof.
  move=> le_x_y. apply: sieve_eq. apply: le_eq.
  by hnf=>?;hnf=>-[]. hnf=> z /=; hnf=> le_x_z. split=> //. by rewrite -le_x_y.
Qed.

Lemma restrict_restrict {A : proType} (U : {mono A^r -> Prop}) (y z : A) :
  z ≤ y -> restrict (restrict U y) z = restrict U z.
Proof.
  move=> le_z_y. apply: sieve_eq. apply: le_eq.
  by hnf=> a; hnf=> -[[ua _] le_a_z]. hnf=> a; hnf=> -[ua le_a_z]. split=> //.
  split=> //. by rewrite le_a_z.
Qed.

Inductive coverage {X : proType} (cov : basis X) (x : X) : sieve x -> Prop :=
| cover_max : @coverage X cov x (sieve_top x)
| cover_cover (C : Cover X) (U : sieve x) :
    cov x C ->
    (forall y, C y -> @coverage X cov y (restrict U y)) ->
    @coverage X cov x U.

Section Coverage.
  Context {X : proType} (b : basis_pred X).
  Implicit Types (x y z : X).

  (*Lemma cover_gcover C x :
    cover C x -> gcover x (sift C).
  Proof.
    move=> cx. apply: gcover_trans (cx) _ => y cy.
    case: cy => z cz ->. exact: coverE cx cz.
    have->: restrict (sift C) y = yo y. apply: le_eq.
      by move=> a _ le. rewrite yoneda. split=> //. by exists y.
    exact: gcover_max.
  Qed.*)

  Lemma coverage_trans x (U V : sieve x) :
    coverage b U ->
    (forall y, U y -> coverage b (restrict V y)) ->
    coverage b V.
  Proof.
    move=> ux. elim: ux V => {x U}.
    - move=> x V /(_ x le_refl). by rewrite restrict_refl.
    - move=> x C U cx h1 ih V h2. apply: cover_cover (cx) _ => z cz.
      apply: ih => // y [uy le_y_z] //. rewrite restrict_restrict //.
      exact: h2.
  Qed.

  Lemma coverageP x y (U : sieve x) :
    coverage b U -> y ≤ x -> coverage b (restrict U y).
  Proof.
    move=> ux. elim: ux y => {x U}.
    - move=> x y le_y_x. rewrite restrict_top //. exact: cover_max.
    - move=> x C U cx h ih y le_y_x. case: (basisP cx le_y_x).
      move=> C' cy lec. apply: cover_cover (cy) _.
      move=> z cz. case: (lec z cz).
      move=> w cw le_z_w. move: (ih _ cw _ le_z_w).
      rewrite !restrict_restrict //. exact: basisE cy cz.
  Qed.

  Program Definition coverage_sheafify (U : presheaf X) : sheaf b :=
    @mk_sheaf X b
      (mk_mfun (fun (x : X^r) =>
         exists2 C : sieve (x : X), coverage b C & forall y : X, C y -> U y)
      (fun x y le_y_x => _))
      (fun C x cox h => _).
  Next Obligation.
    move=> [C cx h1]. exists (restrict C y). exact: coverageP.
    move=> /= z [cz le_z_y]. exact: h1.
  Qed.
  Next Obligation.
    exists (restrict U x); last by move=> y [].
    apply: cover_cover (cox) _ => y cy.
    rewrite restrict_restrict; last first. exact: basisE cox cy.
    case: (h y cy) => C' coy le. apply: coverage_trans (coy) _ => z cz.
    suff->: restrict (restrict U y) z = sieve_top _. exact: cover_max.
    apply: sieve_eq. apply: le_eq. by hnf=> ?; hnf=> -[].
    hnf=> w /=; hnf=> le_w_z. split=> //. split=> //. move: (le _ cz).
    exact: presheafP. rewrite le_w_z. exact: sieveP cz.
  Qed.

  Lemma coverage_sheafify_inc (U : presheaf X) :
    U ≤ coverage_sheafify U.
  Proof.
    move=> x ux. exists (sieve_top (x : X)). exact: cover_max.
    move=> y /= le_y_x. exact: presheafP ux.
  Qed.

  Lemma sheaf_coverageP (x : X) (V : sieve x) :
    coverage b V -> forall U : sheaf b, (forall y, V y -> U y) -> U x.
  Proof.
    elim=> {x V}.
    - move=> x U. apply. exact: le_refl.
    - move=> x C U cx _ ih V h. apply: sheafP cx _ => y cy.
      apply: ih => // z [uz _]. exact: h.
  Qed.

  Lemma coverage_sheafify_adj :
    is_adjunction coverage_sheafify (@presheaf_of_sheaf X b).
  Proof.
    move=> U B. split. move<-. exact: coverage_sheafify_inc.
    move=> le_u_b x [C cx le]. by apply: sheaf_coverageP cx _ _ => y /le/le_u_b.
  Qed.

  Lemma sheafify_def (p : presheaf X) (x : X) :
    sheafify b p x = exists2 C : sieve x, coverage b C & forall y : X, C y -> p y.
  Proof.
    suff->: sheafify b = coverage_sheafify. by [].
    exact: adj_uniqL coverage_sheafify_adj.
  Qed.

  Lemma sheaf_botE (x : X) :
    (⊥ : sheaf b) x = coverage b (sieve_bot x).
  Proof.
    rewrite sheaf_bot_sheafify sheafify_def. apply: pext.
    - case=> C cx h. suff<-: C = sieve_bot x. by []. apply: sieve_eq.
      apply: le_eq; rewrite presheaf_leE //=. move=> y /h. by rewrite presheaf_botE.
    - move=> cx. exists (sieve_bot x). exact: cx. by [].
  Qed.

  Lemma sheaf_joinE (p q : sheaf b) (x : X) :
    (p ∨ q) x = exists2 C : sieve x, coverage b C & forall y : X, C y -> p y \/ q y.
  Proof.
    rewrite sheaf_join_sheafify sheafify_def.
    f_equal; fext=>*; by rewrite presheaf_joinE.
  Qed.

  Lemma sheaf_exE I (F : I -> sheaf b) (x : X) :
    (∃ i, F i) x =
    exists2 C : sieve x, coverage b C & forall y : X, C y -> exists i, F i y.
  Proof.
    rewrite sheaf_ex_sheafify sheafify_def.
    f_equal; fext=>*; by rewrite presheaf_exE.
  Qed.

  Lemma sheaf_exEc I (P : I -> Prop) (F : I -> sheaf b) (x : X) :
    (∃ i | P i, F i) x =
    exists2 C : sieve x, coverage b C & forall y : X, C y -> exists2 i, P i & F i y.
  Proof.
    rewrite sheaf_exc_sheafify sheafify_def.
    f_equal; fext=> C y cy. rewrite presheaf_exEc.
    apply: pext; by firstorder.
  Qed.

  Lemma sheaf_pureE (P : Prop) x :
    (⌈ P ⌉ : sheaf b) x =
    exists2 C : sieve x, coverage b C & forall y : X, C y -> P.
  Proof.
    rewrite sheaf_exE. f_equal; fext=> C y cy. apply: pext.
      by case. move=> p. by split.
  Qed.

  Lemma embed_def (x y : X) :
    (embed b x) y =
    exists2 C : sieve y, coverage b C & forall z : X, C z -> z ≤ x.
  Proof.
    by rewrite/embed sheafify_def.
  Qed.

  Lemma embed_cov (U : Cover X) (x : X) :
    b x U -> (∃ y | U y, embed b y) = embed b x.
  Proof.
    move=> cx. apply: le_eq.
    - focus=> y uy. apply: mono. exact: basisE cx uy.
    - rewrite embedE. apply: sheafP (cx) _ => y uy.
      apply: sheaf_exIc. exists y => //. exact: embedI.
  Qed.

  Lemma embedM (x y z : X) :
    x ≤ y -> x ≤ z -> (forall w, w ≤ y -> w ≤ z -> w ≤ x) ->
    embed b x = (embed b y ∧ embed b z).
  Proof.
    move=> l1 l2 l3. apply: le_eq. apply: meetI; exact: mono.
    apply/impP. rewrite embedE sheaf_impE => w l4.
    rewrite !embed_def => -[U cu cP]. exists U => // v uv.
    apply: l3. rewrite -l4. exact: sieveP uv. exact: cP.
  Qed.
End Coverage.

Definition is_subcanonical {X : proType} (b : basis X) :=
  forall x : X, is_sheaf b (yo x).
Existing Class is_subcanonical.

Section SubcanonicalCoverage.
  Variable (X : proType) (b : basis X).
  Context {bP : is_subcanonical b}.

  Lemma subcanonical_embedE (x y : X) :
    embed b x y = (y ≤ x).
  Proof.
    apply: le_eq; last by exact: embedI.
    by rewrite/embed sheafify_is_sheaf.
  Qed.

  Lemma embed_embedding (x y : X) :
    embed b x ≤ embed b y -> x ≤ y.
  Proof.
    by rewrite embedE subcanonical_embedE.
  Qed.
End SubcanonicalCoverage.

Section SubcanonicalCoverageOrd.
  Variable (X : ordType) (b : basis X).
  Context {bP : is_subcanonical b}.

  Lemma embed_injective : injective (embed b).
  Proof.
    move=> x y eqn. apply: le_eq; apply: (@embed_embedding X b) => //;
      by rewrite eqn.
  Qed.
End SubcanonicalCoverageOrd.

(*Section EmbedCLat.
  Variables (X : clat) (b : basis_pred X).

  Lemma embed_top : embed b ⊤ = ⊤.
  Proof. apply: embedT => y. exact: topI. Qed.

  Lemma emebd_meet (x y : X) : embed b (x ∧ y) = (embed b x ∧ embed b y).
  Proof. apply: embedM => *; by cauto. Qed.
End EmbedCLat.*)

Section CanonicalCoverage.
  Variables (X : proType).

  Definition canonical (x : X) (p : Cover X) : Prop :=
    (forall y, p y -> y ≤ x) /\
    (forall x y, x ≤ y -> p y -> p x) /\ (* <- not needed? *)
    (forall y z, y ≤ x -> (forall w, p w -> w ≤ y -> w ≤ z) -> y ≤ z).

  Lemma canonicalE (U : Cover X) (x y : X) :
    canonical x U -> U y -> y ≤ x.
  Proof. case=> h _. exact: h. Qed.

  Lemma canonicalP (V : Cover X) (x y : X) :
    canonical y V -> x ≤ y -> exists2 U : Cover X, canonical x U & U ≤ V.
  Proof.
    rewrite/canonical => -[e1 [e2 e3]] le_x_y.
    exists (fun z => V z /\ (z ≤ x)); last first; [|split; [|split]].
    - move=> z [vz le_z_x]. by exists z.
    - move=> z [vz le_z_x]. exact: le_z_x.
    - move=> a b le_a_b [vb le_b_x]. split. exact: e2 vb. by rewrite le_a_b.
    - move=> a b le_a_x h. apply e3. by rewrite le_a_x.
      move=> w vw le_w_a. apply h => //. split=> //. by rewrite le_w_a.
  Qed.

  Canonical canonical_basis : basis_pred X :=
    Eval hnf in @mk_basis_pred X canonical canonicalE canonicalP.

  Global Instance canonical_is_subcanonical : is_subcanonical canonical.
  Proof.
    move=> x U y. rewrite/canonical => -[e1 e2] h /=.
    apply e2 => //. move=> w uw le_w_y. exact: h.
  Qed.
End CanonicalCoverage.

Section CanonicalBasis.
  Variables (X : frame).

  Lemma canonical_sup (x : X) (U : Cover X) :
    canonical x U -> (∃ y | U y, y) = x.
  Proof.
    move=> [e1 [e2 e3]]. apply: le_eq. focus=> y uy. exact: e1.
    apply: e3 => // w uw le_w_x. exact: exIc (w) uw le_refl.
  Qed.

  Lemma sup_canonical (U : Cover X) :
    (forall x y, x ≤ y -> U y -> U x) ->
    canonical (∃ y | U y, y) U.
  Proof.
    move=> h. split; [|split].
    - move=> x ux. exact: exIc ux le_refl.
    - exact: h.
    - move=> y z l1 l2. apply le_meetP in l1. rewrite l1.
      rewrite meetxE. focus=> a. rewrite{1}/supguard meetxE. focus=> ua.
      apply: l2. apply: h ua. cauto. cauto.
  Qed.

  Definition unembed (p : sheaf (@canonical X)) : X := ∃ x : X | p x, x.

  Lemma unembed_embed (x : X) :
    unembed (embed _ x) = x.
  Proof.
    apply: le_eq. rewrite/unembed. focus=> y. by rewrite subcanonical_embedE.
    apply: exIc (x) _ le_refl. rewrite subcanonical_embedE. exact: le_refl.
  Qed.

  Lemma embed_unembed (p : sheaf (@canonical X)) :
    embed _ (unembed p) = p.
  Proof.
    rewrite {2}[p]sheaf_representables /=. symmetry.
    apply: embed_cov. rewrite/unembed. apply sup_canonical.
    exact: presheafP.
  Qed.

  Lemma monotone_unembed : monotone unembed.
  Proof.
    move=> p q le_p_q. rewrite/unembed. focus=> x px.
    apply: exIc (x) _ le_refl. exact: le_p_q.
  Qed.
End CanonicalBasis.