\import Algebra.Meta
\import Category
\import Category.Functor
\import Category.Limit
\import Category.Slice
\import Category.Subcat
\import Category.Topos.Presheaf
\import Category.Topos.Sheaf.Site
\import Category.Topos.Sheaf.SiteHom
\import Equiv
\import Function (IsInj, IsSurj)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice.CompleteLattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.SetCategory
\import Set.Set
\import Topology.Locale
\import Topology.Locale.PreorderSite
\open CompleteLattice

\record MatchingFamily {C D : Precat} (F : Functor C.op D) {J : \Type} (x : C) (P : J -> ObOver x) (d : D)
  | \coerce family (j : J) : Hom d (F (P j).)
  | isMatching {j j' : J} {z : C} {g : Hom z (P j).} {g' : Hom z (P j').} : (P j). ∘ g = (P j'). ∘ g' -> F.Func g ∘ family j = F.Func g' ∘ family j'
  \where {
    \func matchingFamily {C : Precat} {D : Precat} (F : Functor C.op D) {J : \Type} (x : C) (P : J -> ObOver x) (d : D) (h : Hom d (F x)) : MatchingFamily F x P d \cowith
      | family j => Func (P j). ∘ h
      | isMatching gg' => inv o-assoc *> pmap (∘ h) (inv Func-o *> pmap Func (later gg') *> Func-o) *> o-assoc

    \lemma inj-char {C D : Precat} {F : Functor C.op D} {J : \Type} {x : C} {P : J -> ObOver x} {d : D}
      : IsInj (matchingFamily F x P d) <-> ∀ {h h' : Hom d (F x)} (\Pi (j : J) -> F.Func (P j). ∘ h = F.Func (P j). ∘ h') (h = h')
      => (\lam Fs hh' => Fs (exts hh'), \lam Fs hh' => Fs \lam j => pmap {MatchingFamily F x P d} (__ j) hh')

    \func map {C D : Precat} (F : Functor C.op D) {I J : \Type} (f : I -> J) {x : C} (P : J -> ObOver x) (d : D) (mf : MatchingFamily F x P d) : MatchingFamily F x (\lam i => P (f i)) d \cowith
      | family i => mf (f i)
      | isMatching => isMatching
      \where {
        \lemma isEquiv (fs : IsSurj f) : IsEquiv (map F f P d)
          => IsEquiv.fromInjSurj (\lam p => exts \lam j => \case \elim j, fs j \with {
            | _, inP (i,idp) => path (p __ i)
          }) \lam mf =>
            \let t j => TruncP.rec-set {_} {Hom d (F (P j).)} (fs j) (\lam s => Func (C.idtoiso $ pmap (\lam x => (P x).) $ inv s.).f ∘ mf s.)
              \lam s s' => mf.isMatching $ inv (ObOver.unequals (pmap P (inv s.))) *> ObOver.unequals (pmap P (inv s'.))
            \in inP (\new MatchingFamily {
              | family j => (t j).
              | isMatching {j} {j'} gg' => \case (t j)., (t j'). \with {
                | inP (s,sp), inP (s',s'p) =>
                  \have aux => mf.isMatching $ inv o-assoc *> pmap (∘ _) (inv $ ObOver.unequals (pmap P (inv s.))) *> gg' *> pmap (∘ _) (ObOver.unequals (pmap P (inv s'.))) *> o-assoc
                  \in pmap (_ ∘) (inv sp) *> inv o-assoc *> pmap (∘ _) (inv Func-o) *> aux *> pmap (∘ _) Func-o *> o-assoc *> pmap (_ ∘) s'p
              }
            }, exts \lam i => TruncP.rec-set-eval (later (i,idp)) *> pmap (∘ _) (later Func-id) *> id-left)
      }
  }

\func PresieveMatchingFamily {C D : Precat} (F : Functor C.op D) (x : C) (P : Presieve x) (d : D)
  => MatchingFamily F {Given P} x __. d
  \where {
    \func matchingFamily {C D : Precat} (F : Functor C.op D) (x : C) (P : Presieve x) (d : D) (h : Hom d (F x)) : PresieveMatchingFamily F x P d
      => MatchingFamily.matchingFamily F {Given P} x __. d h
  }

\func IsSeparatedPresheaf {C : Site} {D : Precat} (F : Functor C.op D)
  => ∀ {x : C} ∀ {S : isCover x} {d : F.D} (IsInj {_} {PresieveMatchingFamily F x S d} (PresieveMatchingFamily.matchingFamily F x S d))
  \where {
    \protected \lemma char : IsSeparatedPresheaf F <-> ∀ {x : C} ∀ {S : isCover x} {d : F.D} {h h' : Hom d (F x)} (∀ {y : S} (F.Func y. ∘ h = F.Func y. ∘ h') -> h = h')
      => (\lam Fs Sc hh' => Fs Sc $ exts \lam j => hh' j.,
          \lam Fs {x} {S} Sc {d} hh' => Fs Sc \lam {y} Sy => pmap {PresieveMatchingFamily F x S d} (family {__} (y,Sy)) hh')
  }

\class SeparatedVPresheaf \extends VPresheaf {
  \override C : Site
  | isSeparated : IsSeparatedPresheaf F

  \lemma separated-covering-inj {x : C} {U : Presieve x} (x<=U : Covering x U) {d : D} : IsInj (PresieveMatchingFamily.matchingFamily F x U d) \elim x<=U
    | covering-inj s p ps=id Up => MatchingFamily.inj-char. $ later \lam c => inv id-left *> pmap (∘ _) (inv Func-id *> pmap F.Func (inv ps=id) *> Func-o) *> o-assoc *> pmap (Func s ∘) (c (_,Up)) *> inv o-assoc *> pmap (∘ _) (inv Func-o *> pmap F.Func ps=id *> Func-id) *> id-left
    | covering-trans x<=T T<=U => MatchingFamily.inj-char. $ later \lam c => MatchingFamily.inj-char. (isSeparated x<=T) \lam t =>
      MatchingFamily.inj-char. (separated-covering-inj (T<=U t.)) \lam (z, inP (u,Uu,z>u,z>u_t)) =>
        inv o-assoc *> pmap (∘ _) (inv Func-o *> pmap F.Func (inv z>u_t) *> Func-o) *> o-assoc *> pmap (Func z>u ∘) (c (u,Uu)) *> inv o-assoc *> pmap (∘ _) (inv Func-o *> pmap F.Func z>u_t *> Func-o) *> o-assoc

  \lemma separated-covering {x : C} {U : Presieve x} (x<=U : Covering x U) {d : D} {g g' : Hom d (F x)} (p : ∀ {u : U} (F.Func u. ∘ g = F.Func u. ∘ g')) : g = g'
    => separated-covering-inj x<=U $ exts \lam j => p j.

  \lemma covering-comp {x : C} {d : D} {I : \Type} {P : I -> ObOver x} (Pe : IsEquiv (MatchingFamily.matchingFamily F x P d))
                       {J : I -> \Type} {Q : \Pi {i : I} -> J i -> ObOver (P i).} (Qc : \Pi {i : I} -> Covering (P i). (TSetIm Q))
                       (Qe : \Pi {i : I} -> IsEquiv (MatchingFamily.matchingFamily F (P i). Q d))
    : IsEquiv (MatchingFamily.matchingFamily F {\Sigma (i : I) (J i)} x (\lam s => ((Q s.)., (P s.). ∘ (Q s.).)) d)
    => inP \new QEquiv {
      | ret (mf : MatchingFamily F x _ d) => IsEquiv.ret Pe
        \let smf i => \new MatchingFamily F _ Q d {
          | family j => mf.family (i,j)
          | isMatching gg' => mf.isMatching (o-assoc *> pmap (_ ∘) gg' *> inv o-assoc)
        }
        \in \new MatchingFamily {
          | family i => IsEquiv.ret Qe (smf i)
          | isMatching {i} {i'} {z} {g} {g'} gg' => separated-covering (Covering.covering-stable g Qc) \lam {a} => \case \elim __ \with {
            | inP (_, inP (j,idp), a>qj, a>qj_g) => inv o-assoc *> pmap (∘ _) (inv (pmap F.Func a>qj_g *> Func-o) *> Func-o) *> o-assoc *>
              pmap {MatchingFamily F _ Q d} (_ ∘ family {__} j) (IsEquiv.f_ret Qe) *> separated-covering (Covering.covering-stable (g' ∘ a.) Qc) \lam {b} => \case \elim __ \with {
                | inP (_ ,inP (j',idp), d>qj', d>qj'_g'a) => inv o-assoc *> pmap (∘ _) (inv Func-o) *> later (mf.isMatching $ inv o-assoc *> pmap (∘ _) (o-assoc *> pmap (_ ∘) a>qj_g *> inv o-assoc *> pmap (∘ _) gg' *> o-assoc) *> o-assoc *> pmap (_ ∘) (inv d>qj'_g'a) *> inv o-assoc) *> inv (pmap {MatchingFamily F _ Q d} (_ ∘ family {__} j') (IsEquiv.f_ret Qe)) *> inv o-assoc *> pmap (∘ _) (inv Func-o *> pmap F.Func (d>qj'_g'a *> o-assoc) *> Func-o) *> o-assoc *> pmap (∘ _) Func-o *> o-assoc
              }
          }
        }
      | ret_f h => pmap (IsEquiv.ret Pe) (exts \lam i => pmap (IsEquiv.ret Qe) (exts \lam j => pmap (∘ h) Func-o *> o-assoc) *> IsEquiv.ret_f Qe) *> IsEquiv.ret_f Pe
      | f_sec mf => exts \lam s => pmap (∘ _) Func-o *> o-assoc *> pmap {MatchingFamily F x P d} (_ ∘ family {__} s.) (IsEquiv.f_ret Pe) *> pmap {MatchingFamily F _ Q d} (family {__} s.) (IsEquiv.f_ret Qe)
    }

  \lemma covering-refined {x : C} {I : \Type} {P : I -> ObOver x} (Pc : Covering x (TSetIm P))
    {J : \Type} {Q : J -> ObOver x} (P<=Q : ∀ (i : I) ∃ (j : J) (f : Hom (P i). (Q j).) ((Q j). ∘ f = (P i).))
    {d : D} (e : IsEquiv (MatchingFamily.matchingFamily F x P d)) : IsEquiv (MatchingFamily.matchingFamily F x Q d)
    => split {_} {x} {\Sigma (i : I) (j : J) (f : Hom (P i). (Q j).) ((Q j). ∘ f = (P i).)}
      (Covering.covering-sub Pc \lam t => TSetIm-elim (\lam i => \case P<=Q i \with {
        | inP (j,f,p) => TSetIm-con $ later (i,j,f,p)
      }) t)
      (\lam s => (s.,s.,s.))
      (IsEquiv.trans e $ MatchingFamily.map.isEquiv \lam i => \case P<=Q i \with {
        | inP (j,f,p) => inP $ later ((i,j,f,p),idp)
      })
    \where
      \private \lemma split {x : C} {I : \Type} {P : I -> ObOver x} (Pc : Covering x (TSetIm P))
        {J : \Type} {Q : J -> ObOver x} (P<=Q : ∀ (i : I) Given (j : J) (f : Hom (P i). (Q j).) ((Q j). ∘ f = (P i).))
        {d : D} (e : IsEquiv (MatchingFamily.matchingFamily F x P d)) : IsEquiv (MatchingFamily.matchingFamily F x Q d)
        => \let map (mf : MatchingFamily F x Q d) : MatchingFamily F x P d => \new MatchingFamily {
                  | family i => Func (P<=Q i). ∘ mf (P<=Q i).
                  | isMatching {i} {i'} gg' => inv o-assoc *> pmap (∘ _) (inv Func-o) *> mf.isMatching (inv o-assoc *> pmap (∘ _) (P<=Q i). *> gg' *> pmap (∘ _) (inv (P<=Q i').) *> o-assoc) *> pmap (∘ _) Func-o *> o-assoc
                }
           \in inP \new QEquiv {
             | ret mf => IsEquiv.ret e (map mf)
             | ret_f h => pmap (IsEquiv.ret e) (exts \lam i => inv o-assoc *>  pmap (∘ h) (inv Func-o *> pmap F.Func (P<=Q i).)) *> IsEquiv.ret_f e
             | f_sec mf => exts \lam j => separated-covering (Covering.covering-stable (Q j). Pc) \case \elim __ \with {
               | inP (_, inP (i,idp), f, f_Q) => inv o-assoc *> pmap (∘ _) (inv (pmap F.Func f_Q *> Func-o) *> Func-o) *>
                 o-assoc *> pmap (_ ∘) (pmap {MatchingFamily F x P d} (family {__} i) (IsEquiv.f_ret e {map mf})) *> inv o-assoc *> pmap (∘ _) (inv Func-o) *> mf.isMatching (inv o-assoc *> pmap (∘ f) (P<=Q i). *> f_Q)
             }
           }
} \where {
  \lemma separated-locale {L : Locale} (S : SeparatedVPresheaf { | C => L }) {U : Set L}
    {d : S.D} {f g : Hom d (S (Join U))} (p : ∀ {y : L} (Uy : U y) (S.F.Func (Join-cond Uy) ∘ f = S.F.Func (Join-cond Uy) ∘ g)) : f = g
    => separated-locale_<= S <=-refl \lam Uy zy zU => pmap (∘ f) (pmap S.F.Func prop-pi *> S.F.Func-o) *> o-assoc *>
        pmap (S.F.Func zy ∘) (p Uy) *> inv o-assoc *> pmap (∘ _) (inv S.F.Func-o *> pmap S.F.Func prop-pi)

  \lemma separated-locale_SJoin {L : Locale} (S : SeparatedVPresheaf { | C => L }) {J : \Type} {h : J -> L} {P : J -> \Type}
    (d : S.D) {f g : Hom d (S (SJoin h P))} (p : ∀ {j : J} (Pj : P j) (S.F.Func (SJoin-cond Pj) ∘ f = S.F.Func (SJoin-cond Pj) ∘ g)) : f = g
    => separated-locale_<= S <=-refl \lam {z} => SetIm-elim \lam Pa z<=ha z<=P => later $ pmap (∘ f) (pmap S.F.Func prop-pi *> S.F.Func-o) *> o-assoc *>
        pmap (S.F.Func z<=ha ∘) (p Pa) *> inv o-assoc *> pmap (∘ g) (inv S.F.Func-o *> pmap S.F.Func prop-pi)

  \lemma separated-locale_<= {L : Locale} (S : SeparatedVPresheaf { | C => L }) {x : L} {U : Set L} (x<=U : x <= Join U)
    {d : S.D} {f g : Hom d (S x)} (p : ∀ {z : L} {y : U} (z <= y) (zx : z <= x) (S.F.Func zx ∘ f = S.F.Func zx ∘ g)) : f = g
    => S.separated-covering {x} {\lam z => ∃ (y : U) (z. <= y)} (Covering.covering-basic $
          L.meet-univ <=-refl x<=U <=∘ Join-ldistr>= <=∘ SJoin-univ \lam {a} Ua => Join-cond $ later (L.meet-left, inP (a, Ua, L.meet-right)))
        \lam {u} (inP (y,Uy,u<=y)) => p Uy u<=y u.
}

\func IsSheaf {C : Site} {D : Precat} (F : Functor C.op D)
  => ∀ {x : C} ∀ {S : isCover x} {d : D} (SheafCond F S d)
  \where {
    \lemma makeSheaf (p : IsSheaf F) : VSheaf D C F \cowith
      | isSheaf => p

    \func SheafCond {C : Site} {D : Precat} (F : Functor C.op D) {x : C} (S : Presieve x) (d : D) : \Prop
      => IsEquiv {_} {PresieveMatchingFamily F x S d} (PresieveMatchingFamily.matchingFamily F x S d)

    \lemma SetSheafCond.{s} {C : Site} {F : Functor C.op SetCat.{s}} {x : C} (S : Presieve x) (c : SheafCond F S (\Sigma)) {D : \Set s} : SheafCond F S D \elim c
      | inP e =>
        \let mapMF d (mf : PresieveMatchingFamily F x S D) : PresieveMatchingFamily F x S (\Sigma) => \new MatchingFamily {
          | family j _ => mf j d
          | isMatching p => ext \lam _ => path \lam i => mf.isMatching p i d
        } \in inP \new QEquiv {
          | ret mf d => e.ret (mapMF d mf) ()
          | ret_f h => ext \lam d => path \lam i => e.ret_f (\lam _ => h d) i ()
          | f_sec mf => exts \lam j => ext \lam d => path \lam i => e.f_ret (mapMF d mf) i j ()
        }

    \lemma sheaf-lim {x : C} {S : Presieve x} {d : D} : SheafCond F S d <-> IsEquiv (conePullback cone d)
      => \let e => \new QEquiv {PresieveMatchingFamily F x S d} {Cone coneF d} {
        | f mf => \new Cone {
          | coneMap j => Func j. ∘ mf (j.,j.)
          | coneCoh h => inv o-assoc *> pmap (∘ _) (inv Func-o) *> mf.isMatching (inv o-assoc *> h.)
        }
        | ret c => \new MatchingFamily {
          | family j => c.coneMap (j.., j., j., id)
          | isMatching {j} {j'} {z} {g} {g'} p => c.coneCoh {j.., j., j., id} (g, pmap (∘ g) id-right) *> inv id-left *> pmap (∘ _) (inv Func-id) *> c.coneCoh {z, j., j., g} {z, j'., j'., g'} (id, id-right *> p) *> inv (c.coneCoh {j'.., j'., j'., id} (g', pmap (∘ g') id-right))
        }
        | ret_f mf => exts \lam j => pmap (∘ _) Func-id *> id-left
        | f_sec c => exts \lam j => c.coneCoh {j.., j., j., id} (j., pmap (∘ _) id-right)
      } \in (\lam sc => transport IsEquiv (ext \lam h => exts \lam j => inv $ pmap (∘ h) Func-o *> o-assoc) $ IsEquiv.trans sc (inP e),
             \lam lc => transport IsEquiv (ext \lam h => exts \lam j => pmap (Func __ ∘ h) id-right) $ IsEquiv.trans lc $ inP (symQEquiv e))
      \where {
        \func coneJ : Precat \cowith
          | Ob => Given (y : C) (px : S) (Hom y px.)
          | Hom t s => \Sigma (f : Hom s. t.) (t.. ∘ t. ∘ f = s.. ∘ s.)
          | id => (id, id-right)
          | o f g => (g. ∘ f., inv o-assoc *> pmap (∘ _) g. *> f.)
          | id-left => ext id-right
          | id-right => ext id-left
          | o-assoc => ext (inv o-assoc)

        \func coneF : Functor coneJ D \cowith
          | F s => F s.
          | Func f => Func f.
          | Func-id => Func-id
          | Func-o => Func-o

        \func cone : Cone coneF (F x) \cowith
          | coneMap j => Func (j.. ∘ j.)
          | coneCoh h => inv Func-o *> pmap F.Func h.
      }
  }

-- | Sheaves valued in {D}
\class VSheaf \extends SeparatedVPresheaf {
  | isSheaf : IsSheaf F
  | isSeparated Sc {d} => IsEquiv.isInj (isSheaf Sc)

  \lemma sheaf-covering {x : C} {U : Presieve x} (x<=U : Covering x U) {d : D} : IsEquiv (PresieveMatchingFamily.matchingFamily F x U d) \elim x<=U
    | covering-inj s p ps=id Up \as x<=U => IsEquiv.fromInjSurj (separated-covering-inj x<=U) \lam mf => inP (Func s ∘ mf.family (_, Up), exts \lam j =>
      inv o-assoc *> pmap (∘ _) (inv Func-o) *> mf.isMatching (inv o-assoc *> pmap (∘ _) ps=id *> id-left *> inv id-right) *> pmap (∘ _) Func-id *> id-left)
    | covering-trans {T} x<=T T<=U => covering-refined
      (Covering.covering-trans x<=T \lam {t} Tt => Covering.covering-sub (T<=U Tt) \lam {z} r => inP $ later (_, TSetIm-con $ later ((t,Tt),(z,r)), id, id-right))
      (later \lam ((t,Tt), (z, inP (u,Uu,f,f_t))) => inP ((u,Uu),f,f_t)) $
      covering-comp {_} {x} {d} {Given T} {__.} (isSheaf x<=T) {\lam t => Given (z : ObOver t..) ∃ (u : U) (f : Hom z. u.) (u. ∘ f = t.. ∘ z.)} {__.}
        (\lam {t} => Covering.covering-sub (T<=U t.) \lam {z} r => TSetIm-con $ later (z,r))
        (\lam {t} => sheaf-covering (T<=U t.))

  \lemma sheaf-matchingFamily {J : \Type} {x : C} {P : J -> ObOver x} (x<=U : Covering x (TSetIm P)) {d : D} : IsEquiv (MatchingFamily.matchingFamily F x P d)
    => IsEquiv.trans (sheaf-covering x<=U) $ MatchingFamily.map.isEquiv {C} {D} {F} {J} {\Sigma (px : ObOver x) (TSetIm P px)} {\lam j => (P j, inP (j,idp))} \lam (_, inP (j,idp)) => inP (j,idp)

  \sfunc sheaf-matchingFamily-surj {J : \Type} {x : C} {P : J -> ObOver x} (x<=U : Covering x (TSetIm P)) {d : D}
    (mf : MatchingFamily F x P d) : Given (h : Hom d (F x)) ∀ j (F.Func (P j). ∘ h = mf j)
    => \have r => IsEquiv.splitSurj (sheaf-matchingFamily x<=U) mf
       \in (r., \lam j => path \lam i => r. i j)

  \lemma direct_image {C' : Site} (f : SiteHom C' C) : VSheaf D C' (Comp F f.op) \cowith
    | isSheaf {x} {S} xS {d} => IsEquiv.trans (sheaf-covering (f.Func-cover xS)) $
        IsEquiv.trans (MatchingFamily.map.isEquiv {C} {D} {F} {Given S} {Given (py : ObOver (f x)) ∃ (px : S) (py = (f px., Func px.))} {\lam s => (_, inP (s.,s.,idp))} \lam (_, inP (px,Spx,idp)) => inP ((px,Spx),idp)) $
        inP \new QEquiv {
          | f mf => \new MatchingFamily {
            | family => mf.family
            | isMatching {j} {j'} gg' => mf.isMatching $ inv Func-o *> pmap Func gg' *> Func-o
          }
          | ret mf => \new MatchingFamily {
            | family => mf.family
            | isMatching {j} {j'} {z} {g} {g'} gg' => separated-covering (f.Func-flat-pullback gg') \lam {u} (inP (w,w>j,w>j',c,h,hl,hr)) =>
              inv o-assoc *> pmap (∘ _) (inv Func-o) *> pmap (∘ _) (pmap F.Func (inv hl) *> Func-o) *> o-assoc *> pmap (_ ∘) (mf.isMatching c) *> inv o-assoc *> pmap (∘ _) (inv Func-o *> pmap F.Func hr) *> pmap (∘ _) Func-o *> o-assoc
          }
          | ret_f => idpe
          | f_sec => idpe
        }
} \where {
  \func restrict {L : Locale} (a : L) (F : VSheaf { | C => L }) : VSheaf F.D (L.restrict a) \cowith
    | F => Comp F Locale.restrict.functor.op
    | isSheaf {x} {S} x<=S {d} => IsEquiv.trans (F.isSheaf {x.} {\lam px => S ((px., px. <=∘ x.), px.)} (x<=S <=∘ L.SJoin-univ \lam {b} s => Join-cond $ later (s., transport S (ext $ ext idp) s.))) $ inP \new QEquiv {
      | f mf => \new MatchingFamily {
        | family j => mf ((j..., j..), \box transport S (ext $ ext idp) j.)
        | isMatching {j} {j'} _ => mf.isMatching {(j..., j..), _} {(j'..., j'..), _} prop-pi
      }
      | ret mf => \new MatchingFamily {
        | family j => mf (((j.., j.. <=∘ x.), j..), j.)
        | isMatching {j} {j'} {z} {g} {g'} _ => mf.isMatching {_, j.} {_, j'.} {z, g <=∘ j.. <=∘ x.} prop-pi
      }
      | ret_f => idpe
      | f_sec mf => exts \lam j => cong $ ext $ ext (ext idp)
    }

  \lemma direct_image_locale {L L' : Locale} (f : FrameHom L' L) (S : VSheaf { | C => L }) : VSheaf S.D L' (Comp S f.op)
    => S.direct_image f.functor

  \lemma sheaf-locale {L : Locale} (S : VSheaf { | C => L }) {U : Set L} {d : S.D}
    : IsEquiv (PresieveMatchingFamily.matchingFamily S.F (Join U) (\lam x => U x.) d)
    => S.isSheaf (Join-univ \lam Uw => Join-cond (Join-cond Uw, Uw)) {d}

  \lemma sheaf-locale_SJoin {L : Locale} (S : VSheaf { | C => L }) {J : \Type} {f : J -> L} {U : Set J} {d : S.D}
    : IsEquiv (MatchingFamily.matchingFamily S.F {Set.Total U} (SJoin f U) (\lam j => (f j., SJoin-cond j.)) d)
    => IsEquiv.trans (sheaf-locale S) {MatchingFamily.map S (\lam j => later ((f j., SJoin-conde j. j.), SetIm-cone j. j.)) _ d} $
        MatchingFamily.map.isEquiv $ later \lam (x, inP ((j,Uj),fj=x)) => inP ((j,Uj), ext $ ext fj=x)
}

\instance VSheafCat (D : Cat) (C : Site) : Cat
  => subCat {VPresheafCat D C} {VSheaf D C} (\new Embedding {
    | f P => P
    | isEmb _ _ => \new Retraction {
      | sec p => ext VSheaf { | VPresheaf => p }
      | f_sec => idpe
    }
  })
  \where {
    \lemma functor-iso {F G : VSheaf D C} (e : Iso {FunctorCat C.op D} {F} {G}) : Iso {VSheafCat D C} {F} {G} e e.hinv \cowith
      | hinv_f => e.hinv_f
      | f_hinv => e.f_hinv
  }

-- | Sheaves valued in sets
\class Sheaf.{v} \extends VSheaf
  | D => SetCat.{v}

\func IsPreorderSheaf.{s} {C : PreorderSite.{s}} {D : Precat} (F : Functor C.op D)
  => ∀ {x : C} {S : isBasicCover x} (∀ {y : S} (y <= x)) {d : F.D} (SheafCond F x S d)
  \where {
    \func SheafCond.{s} {C : PreorderSite.{s}} {D : Precat} (F : Functor C.op D) (x : C) (S : Set C) (d : D) : \Prop
      => IsEquiv {_} {PresieveMatchingFamily F x _ d} (PresieveMatchingFamily.matchingFamily F x (\lam px => S px.) d)

    \lemma SetSheafCond.{s,v} {C : PreorderSite.{s}} {F : Functor C.op SetCat.{v}} (x : C) (S : Set C) (c : SheafCond F x S (\Sigma)) {D : \Set v} : SheafCond F x S D \elim c
      | inP e =>
        \let mapMF d (mf : PresieveMatchingFamily F x (\lam j => S j.) D) : PresieveMatchingFamily F x (\lam j => S j.) (\Sigma) => \new MatchingFamily {
          | family j _ => mf j d
          | isMatching p => ext \lam _ => path \lam i => mf.isMatching p i d
        } \in inP \new QEquiv {
          | ret mf d => e.ret (mapMF d mf) ()
          | ret_f h => ext \lam d => path \lam i => e.ret_f (\lam _ => h d) i ()
          | f_sec mf => exts \lam j => ext \lam d => path \lam i => e.f_ret (mapMF d mf) i j ()
        }

    \lemma toSheaf (FS : IsPreorderSheaf F) : IsSheaf F
      => \lam {x} {S} x<=S {d} => IsEquiv.trans (FS x<=S \lam s => s.) $ inP \new QEquiv {
        | f mf => \new MatchingFamily {
          | family j => mf (j., (j.., j.))
          | isMatching {j} {j'} => mf.isMatching {j., (j.., j.)} {j'., (j'.., j'.)}
        }
        | ret mf => \new MatchingFamily {
          | family j => mf (j., transport S (ext idp) j..)
          | isMatching {j} {j'} => mf.isMatching {j., transport S (ext idp) j..} {j'., transport S (ext idp) j'..}
        }
        | ret_f mf => exts \lam j => cong (ext idp)
        | f_sec mf => exts \lam j => cong (ext idp)
      }

    \lemma makeSheaf (FS : IsPreorderSheaf F) : VSheaf D C F \cowith
      | isSheaf {x} => toSheaf FS {x}

    \lemma fromSheaf.{s} {C : PreorderSite.{s}} {D : Precat} {F : Functor C.op D} (FS : IsSheaf F) : IsPreorderSheaf F
      => \lam {x} {S} x<=S S<=x => FS {x} {\lam px => S px.} $ transport (isBasicCover x) (ext \lam y => propExt (\lam Sy => (S<=x Sy, Sy)) __.) x<=S

    \sfunc sheaf-map (FS : IsPreorderSheaf F) {a : C} {U : Set C} (a<=U : Cover a U) {B : D} (f : \Pi {b : C} -> U b -> Hom B (F b))
                     (fc : \Pi {c b b' : C} (Ub : U b) (Ub' : U b') (cb : c <= b) (cb' : c <= b') -> F.Func cb ∘ f Ub = F.Func cb' ∘ f Ub')
      : Given (h : Hom B (F a)) ∀ {c d} (Ud : U d) (ca : c <= a) (cd : c <= d) (F.Func ca ∘ h = F.Func cd ∘ f Ud)
      => \have r => (makeSheaf FS).sheaf-matchingFamily-surj {Given (x : C) (y : U) (x <= a) (x <= y)} {a} {\lam s => (s.,s.)}
                    (Cover.Cover_Covering $ Cover.cover-down-sub a<=U \lam {y} {z} Uz yz ya => (ya, TSetIm-con $ later (y,z,Uz,ya,yz))) {B} \new MatchingFamily {
                      | family j => F.Func j. ∘ f j.
                      | isMatching {j} {j'} {z} {z<=j} {z<=j'} _ => inv o-assoc *> pmap (∘ _) (inv F.Func-o) *> fc _ _ _ _ *> pmap (∘ _) F.Func-o *> o-assoc
                    }
         \in (r., \lam {c} {d} Ud ca cd => r. (c,d,Ud,ca,cd))
  }

\lemma sheaf-reflect.{s} {C : Site.{s,s}} {D E : Cat} (G : Functor D E)
                         (G-lim : \Pi {J : Precat.{s,s}} (H : Functor J D) -> ReflectsLimit G H) {F : Functor C.op D} (Fs : IsSheaf (Comp G F)) : IsSheaf F
  => \lam x<=S {d} => IsSheaf.sheaf-lim. $ G-lim {IsSheaf.sheaf-lim.coneJ {C}} _ IsSheaf.sheaf-lim.cone (\lam d => (IsSheaf.sheaf-lim {C} {E} {Comp G F}). (Fs x<=S)) d

\lemma sheaf-preserve.{s} {C : Site.{s,s}} {D E : Cat} (G : Functor D E)
                          (G-lim : \Pi {J : Precat.{s,s}} (H : Functor J D) -> PreservesLimit G H) (F : VSheaf D C) : IsSheaf (Comp G F)
  => \lam x<=S {d} => (IsSheaf.sheaf-lim {C} {E} {Comp G F}). $ G-lim {IsSheaf.sheaf-lim.coneJ {C}} _ IsSheaf.sheaf-lim.cone (\lam d' => IsSheaf.sheaf-lim. (F.isSheaf x<=S)) d