\import Category
\import Category.Functor
\import Category.Limit
\import Category.Slice
\import Category.Topos.Sheaf
\import Category.Topos.Sheaf.Site
\import Equiv (ESEquiv, Embedding)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set.Category

\lemma subSheaf {C : Site} {F : Presheaf C} {G : Sheaf C} (e : NatTrans (\suc \lp) F G) (isEmb : \Pi (a : C) {x y : F a} -> e a x = e a y -> x = y)
                (cl : \Pi {a : C} {s : Sieve a} -> isCover a s -> \Pi (x : G a) -> (\Pi {b : C} (f : Hom b a) -> s f -> \Sigma (y : F b) (e b y = G.F.Func f x)) -> ∃ (y : F a) (e a y = x))
  : Sheaf { | Presheaf => F } \cowith
  | isSheaf {a} {s : Sieve} a<s =>
    SetBicat.cone-isLim (Cone.map F s.cone) (\new ESEquiv {
      | Embedding => Embedding.fromInjection \lam {f} {g} p => ext \lam () => isEmb a
          \let | t => limUnique {G.isSheaf a<s} {\Sigma} {\lam _ => e a (f ())} {\lam _ => e a (g ())} \lam j => exts \lam () =>
                      inv (path (\lam i => e.natural j.. i (f ()))) *> pmap (e j..) (path (\lam i => coneMap {p i} j ())) *> path (\lam i => e.natural j.. i (g ()))
          \in path (\lam i => t i ())
      | isSurjMap (c : Cone) =>
        \have | c' : Cone (Comp G s.diagram.op) (\Sigma) => \new Cone {
                  | coneMap j z => e _ (c.coneMap j z)
                  | coneCoh {j} {j'} h => ext \lam z => inv (path (\lam i => e.natural {j..} {j'..} h. i (c.coneMap j z))) *> pmap (e j'..) (path (\lam i => c.coneCoh h i z))
                }
              | s => cl a<s (limMap {G.isSheaf a<s} c' ()) \lam {b} f sf => (c.coneMap ((b,f),sf) (), inv (path (\lam i => limBeta {G.isSheaf a<s} c' ((b,f),sf) i ())))
        \in TruncP.map s \lam (y,p) => (\lam _ => y, exts \lam j => ext \lam () => isEmb j.. $
            path (\lam i => e.natural j.. i y) *> pmap (G.F.Func j..) p *> path (\lam i => limBeta {G.isSheaf a<s} c' j i ()))
    })
  \where {
    \func conv {C : Site} {F G : Sheaf C} (e : NatTrans (\suc \lp) F G) (isEmb : \Pi (a : C) {x y : F a} -> e a x = e a y -> x = y)
      {a : C} {s : Sieve a} (a<s : isCover a s) (x : G a) (c : \Pi {b : C} (f : Hom b a) -> s f -> \Sigma (y : F b) (e b y = G.F.Func f x)) : \Sigma (y : F a) (e a y = x)
      => \let | c' : Cone (Comp F s.diagram.op) (\Sigma) => \new Cone {
                     | coneMap ((b,f),sf) _ => (c f sf).
                     | coneCoh h => ext \lam _ => isEmb _ $ path (\lam i => e.natural h. i _) *> later (rewrite (inv h., G.F.Func-o) $ pmap (G.F.Func h.) (c _ _).) *> inv (c _ _).
                   }
              | x' => limMap {F.isSheaf a<s} c' ()
         \in (x', \have t => limUnique {G.isSheaf a<s} \lam j => ext \lam _ =>
                    inv (path (\lam i => e.natural j.. i x')) *> pmap (e j..) (path (\lam i => limBeta {F.isSheaf a<s} c' j i ())) *> (c j.. j.).
                  \in path (\lam i => t i ()))
  }

\lemma subSheafWithBasis {C : SiteWithBasis} {F : Presheaf C} {G : Sheaf C} (e : NatTrans (\suc \lp) F G) (isEmb : \Pi (a : C) {x y : F a} -> e a x = e a y -> x = y)
                         (cl : \Pi {a : C} {J : \Set} {g : J -> SlicePrecat a} -> isBasicCover a g -> \Pi (x : G a) -> (\Pi (j : J) -> \Sigma (y : F (g j).) (e (g j). y = G.F.Func (g j). x)) -> ∃ (y : F a) (e a y = x))
  : Sheaf { | Presheaf => F }
  => subSheaf e isEmb \lam c x h => \case \elim c \with {
    | inP (J,g,c,sg) => cl c x \lam j => h (g j). (sg j)
  }
  \where {
    \func conv {C : SiteWithBasis} {F G : Sheaf C} (e : NatTrans (\suc \lp) F G) (isEmb : \Pi (a : C) {x y : F a} -> e a x = e a y -> x = y)
               {a : C} {J : \Set} {g : J -> SlicePrecat a} (c : isBasicCover a g) (x : G a) (h : \Pi (j : J) -> \Sigma (y : F (g j).) (e (g j). y = G.F.Func (g j). x)) : \Sigma (y : F a) (e a y = x)
      => subSheaf.conv {C} {F} {G} e isEmb {a} {C.genSieve a g} (unfold $ inP (J, g, c, \lam j => inP (j, id _, id-right))) x \lam {b} f => \scase __ \return \Sigma (y : F b) (e b y = G.F.Func f x) \level \lam p q => ext $ isEmb b (p. *> inv q.) \with {
        | inP t => (F.F.Func t. (h t.)., pmap (__ (h t.).) (e.natural t. ) *> pmap (G.F.Func t.) (h t.). *> pmap (__ x) (inv G.F.Func-o) *> pmap (G.F.Func __ x) t.)
      }
  }