Sheafification with respect to a Lawvere-Tierney closure in logical form.

sheafify.v

(* The basic theory of Lawvere-Tierney operators and sheafification in logical form.

   This formalization is based on:

   Barbara Veit: A proof of the associated sheaf theorem by means of categorical logic,
   The Journal of Symbolic Logic , Volume 46 , Issue 1 , March 1981 , pp. 45–55
   DOI: https://doi.org/10.2307/2273255
*)

Require Import Utf8.

(* We adopt axioms about [Prop] that are valid in a topos, where [Prop]
   corresponds to a subobject classifier [Ω].
*)

(* Co-inhabited propositions are equal. *)
Axiom propext : ∀ {p q : Prop}, (p → q) → (q → p) → p = q.

(* A proposition has at most one inhabitant. *)
Axiom propeq : ∀ {p : Prop} (u v : p), u = v.

(* Function extensionality is valid in a topos. *)
Axiom funext : ∀ {A : Type} {P : A → Type} (f g : ∀ a, P a), (∀ x, f x = g x) → f = g.

(* A Lawvere-Tierney closure operator (formerly known as a “topology”) on [Prop]
   is the same thing as a monad on Prop qua poset. For the purposes of
   formalization, it is convenient to adopt the terminology arising from the
   monad structure. *)
Structure Closure := {
  close :> Prop → Prop ;
  fmap : ∀ {p q}, (p → q) → close p → close q ; (* monotone *)
  η : ∀ {p}, p → close p ; (* inflationary *)
  μ : ∀ {p}, close (close p) → close p ; (* idempotent *)
}.

Arguments fmap {c} {p q}.
Arguments η {c} {p}.
Arguments μ {c} {p}.

(* The monadic bind. Below this typically used when a goal
   is of the form [j p] and we have an assumption [h : j q].
   Applying [bind h] removes [j] from the assumption [h].
*)
Definition bind {j : Closure} {p q : Prop} : j p → (p → j q) → j q :=
  fun x f => μ (fmap f x).

(* A closure operator preserves conjunctions (is strong qua monad). *)
Theorem Closure_conj (j : Closure) (p q : Prop) : j (p ∧ q) ↔ j p ∧ j q.
Proof.
  split.
  - intro.
    split ; now apply (fmap (p := p ∧ q)).
  - intros [jp jq].
    exact (bind jp (fun x => bind jq (fun y => η (conj x y)))).
Defined.

(* A proposition [p] is said to be [j]-stable when [j p → p]. *)
Structure StableProp (j : Closure) :=
  { _prop :> Prop ;
    stable : j _prop → _prop
  }.

Arguments stable {j} {s}.

Section Sheafification.

  (* Let [j] be a Lawvere-Tierney closure operator. *)
  Parameter j : Closure.

  (* An abbreviation for [j] that maps to [StableProp j] instead of [Prop]. *)
  Let j' (p : Prop) : StableProp j :=
    {| _prop := j p ; stable := μ |}.

  (* Propositional extensionality for [j]-stable propositions. *)
  Lemma propjext {p q : StableProp j} : (p → q) → (q → p) → p = q.
  Proof.
    destruct p as [p ps].
    destruct q as [q qs].
    simpl.
    intros pq qp.
    destruct (propext pq qp).
    destruct (funext ps qs (fun h => propeq (ps h) (qs h))).
    reflexivity.
  Qed.

  (* The object of [j]-stable predicates on [A]. *)
  Definition powj (A : Type) := A → StableProp j.

  Definition is_stable_eq (A : Type) := ∀ (a a' : A), j (a = a') -> a = a'.

  Theorem StableProp_separated : is_stable_eq (StableProp j).
  Proof.
    intros a a' je.
    apply propjext.
    - intro.
      apply stable, (bind je).
      intros [].
      now apply η.
    - intro.
      apply stable, (bind je).
      intros e.
      destruct (eq_sym e).
      now apply η.
  Qed.

  (* The [j]-dense predicates on a set. *)
  Structure dense (A : Type) :=
    { dense_map :> A → Prop ;
      is_dense : ∀ a, j (dense_map a)
    }.

  Structure denseMono (A B : Type) :=
    { dm_map :> A → B ;
      dm_injective : ∀ a a', dm_map a = dm_map a' → a = a' ;
      dm_dense : ∀ b, j (∃ a, dm_map a = b)
    }.

  Arguments dm_injective {A} {B} (d) {a} {a'}.
  Arguments dm_dense {A} {B}.

  (* The sheaf structure on a type [F]. *)
  Class Sheaf (F : Type) :=
    { extend : ∀ {A B : Type} (m : denseMono A B), (A → F) → (B → F) ;
      is_extension : ∀ {A B : Type} (m : denseMono A B) f a, extend m f (m a) = f a ;
      unique_extension : ∀ {A B : Type} (m : denseMono A B) (f : A → F) (g h : B → F),
        (∀ a, g (m a) = f a) →
        (∀ a, h (m a) = f a) →
        (∀ a, g a = h a)
    }.

  (* A convenience extensionality principle for subsets. Is this in the
     standard library somewhere? *)
  Lemma sigext {A : Type} {p : A → Prop} (u v : sig p) :
    proj1_sig u = proj1_sig v -> u = v.
  Proof.
    intro e.
    destruct u as [x px].
    destruct v as [y py].
    simpl in e.
    destruct e.
    destruct (propeq px py).
    reflexivity.
  Qed.

  (* (* If [m : A → B] is a mono, then the evident map *)
  (*    [A → {b : B | j (∃ a . m a = b)}] is a dense mono. *) *)
  (* Definition close_mono {A B : Type} (m : A → B) : *)
  (*   (∀ a a', m a = m a' → a = a') → denseMono A { b : B | j (∃ a, m a = b) }. *)
  (* Proof. *)
  (*   intro minj. *)
  (*   pose (m' := fun a => exist (fun b => j (∃ a, m a = b)) (m a) (η (ex_intro _ a eq_refl))). *)
  (*   exists m'. *)
  (*   - intros a a' eq. *)
  (*     apply minj. *)
  (*     exact (f_equal (fun b => proj1_sig b) eq). *)
  (*   - intros [b jmab]. *)
  (*     apply (bind jmab). *)
  (*     intros [a mab]. *)
  (*     apply η. *)
  (*     exists a. *)
  (*     unfold m'. *)
  (*     now apply sigext. *)
  (* Defined. *)

  Definition Δ (A : Type) := { u : A * A | fst u = snd u }.

  Definition Δj (A : Type) := { u : A * A | j (fst u = snd u) }.

  Definition close_diag (A : Type) : denseMono (Δ A) (Δj A).
  Proof.
    exists (fun (u : Δ A) => exist _ (proj1_sig u) (η (proj2_sig u))).
    - intros [u ?] [v ?] eq.
      apply sigext.
      simpl.
      exact (f_equal (fun b => proj1_sig b) eq).
    - intros [[a b] jab].
      apply (bind jab).
      intros eq.
      apply η.
      exists (exist _ (a, b) eq).
      now apply sigext.
  Defined.

  (* A sheaf has stable equality. *)
  Theorem sheaf_stable_eq {F : Type} `{Sheaf F}: is_stable_eq F.
  Proof.
    intros x y jxy.
    pose (f := fun (v : Δ F) => fst (proj1_sig v)).
    pose (g := fun (u : Δj F) => fst (proj1_sig u)).
    pose (h := fun (u : Δj F) => snd (proj1_sig u)).
    assert (gext : ∀ a, g (close_diag F a) = f a).
    { intros [[? ?] ?]. reflexivity. }
    assert (hext : ∀ a, h (close_diag F a) = f a).
    { intros [[? ?] ξ]. symmetry. exact ξ. }
    exact (unique_extension (close_diag F) f g h gext hext (exist _ (x,y) jxy)).
  Qed.

  (* The j-stable powerset as a sheaf. *)
  Instance powj_sheaf {A : Type} : Sheaf (powj A).
  Proof.
    exists (fun {B} {C} (m : denseMono B C) (f : B → powj A) (c : C) (a : A) =>
              j' (∃ b, m b = c ∧ f b a)).
    - intros B C m f b.
      apply funext.
      intro a.
      apply propjext.
      + intro H.
        apply stable.
        apply (bind H).
        intros [b' [eq fba]].
        destruct (dm_injective m eq).
        now apply η.
      + intro fba.
        apply η.
        now exists b.
    - intros B C m f g h gext hext c.
      apply funext ; intro a.
      apply (StableProp_separated).
      apply (bind (dm_dense m c)).
      intros [b mbc].
      rewrite <- mbc.
      rewrite gext.
      rewrite hext.
      apply η.
      reflexivity.
  Qed.

  Definition extend_closed {F : Type} `{Sheaf F} (p : F → StableProp j)
    (A B : Type) (m : denseMono A B) :
    (A → sig p) → (B → sig p).
  Proof.
    intros f b.
    pose (f' := fun a => proj1_sig (f a)).
    exists (extend m f' b).
    apply stable.
    apply (bind (dm_dense m b)).
    intros [a mab].
    apply η.
    rewrite <- mab.
    rewrite (is_extension m f' a).
    exact (proj2_sig (f a)).
  Defined.

  Lemma sig_is_stable_eq {A : Type} {p : A → StableProp j} :
    is_stable_eq A → is_stable_eq (sig p).
  Proof.
    intros sepA x y jxy.
    apply sigext.
    apply sepA.
    apply (bind jxy).
    intros [].
    apply η.
    reflexivity.
  Qed.

  (* A j-stable subset of a sheaf is a sheaf. *)
  Definition stable_sheaf {F : Type} `{Sheaf F} (p : F → StableProp j) : Sheaf (sig p).
  Proof.
    exists (extend_closed p).
    - intros A B m f a.
      apply sigext.
      exact (is_extension m (fun xp => proj1_sig (f xp)) a).
    - intros A B m f g h gext hext b.
      apply sig_is_stable_eq.
      + now apply sheaf_stable_eq.
      + apply (bind (dm_dense m b)). intros [a mab].
        apply η.
        rewrite <- mab.
        transitivity (f a).
        * apply gext.
        * symmetry ; apply hext.
  Defined.

  (* The j-closure of a singleton. *)
  Definition jsing {A : Type} (a : A) : powj A := fun b => j' (a = b).

  (* Shifification of a type. *)
  Definition sheafify (A : Type) := { p : A → StableProp j | j' (∃ a, p = jsing a) }.

  (* Sheafification yields a shief. *)
  Instance sheafify_sheaf {A : Type} : Sheaf (sheafify A).
  Proof.
    apply (stable_sheaf (fun p => j' (∃ a, p = jsing a))).
  Defined.

  (* TODO: sheafification is a reflection. *)

  (* TODO: sheafification preserves finite limits. *)

End Sheafification.