\import Category
\import Category.Functor
\import Category.Slice
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Set (Set, ⊆)

\func Presieve {C : Precat} (x : C)
  => Set (ObOver x)
  \where {
    \func Refines (P Q : Presieve x) : \Prop
      => ∀ {y : P} ∃ (z : Q) (f : Hom y. z.) (z. ∘ f = y.)

    \lemma <=_Refines {P Q : Presieve x} (P<=Q : P ⊆ Q) : Refines P Q
      => \lam {y} Py => inP (y, P<=Q Py, id, id-right)

    \protected \func pushforward (F : Functor) {x : F.C} (P : Presieve x) : Presieve (F x)
      => \lam py => ∃ (px : P) (py = (F px., Func px.)) -- (f : Hom py.1 (F px.1)) (py.2 = Func px.2 ∘ f)
  }

\class Site \extends Precat {
  | isCover (x : Ob) : Presieve x -> \Prop
  | cover-stable {x y : Ob} (h : Hom x y) : ∀ {S : isCover y} ∃ (T : isCover x) ∀ {px : T} ∃ (py : S) (f : Hom px. py.) (py. ∘ f = h ∘ px.)

  \func IsCoverFam {J : \Type} {x : Ob} (f : J -> ObOver x) : \Prop
    => isCover x \lam px => ∃ (j : J) (px = f j)

  \func isCover_IsCoverFam {x : Ob} {P : Presieve x} : isCover x P <-> IsCoverFam {_} {Given P} __.
    => <->_=. $ pmap (isCover x) $ ext \lam px => ext (\lam Ppx => inP ((px,Ppx),idp), \lam (inP (j,p)) => transportInv P p j.)
} \where {
  \func pushforwardFam.{o1,h1,o2,h2} {C : Site.{o1,h1}} {D : Site.{o2,h2}} (F : Functor C D) {J : \Type} {x : C} (P : J -> ObOver x) : J -> ObOver (F x)
    => \lam j => (F (P j)., Func (P j).)
}

\truncated \data Covering {C : Site} (x : C) (U : Presieve x) : \Prop
  | covering-inj {y : C} (s : Hom x y) (p : Hom y x) (p ∘ s = id) (U (y,p))
  | covering-trans {T : Presieve x} (isCover x T)
                   (∀ {y : T} (Covering y. \lam z => ∃ (u : U) (f : Hom z. u.) (u. ∘ f = y. ∘ z.)))
  \where {
    \lemma covering-id {x : C} {U : Presieve x} (Uid : U ObOver.id) : Covering x U
      => covering-inj id id id-left Uid

    \lemma covering-basic {x : C} {U : Presieve x} (x<=U : isCover x U) : Covering x U
      => covering-trans x<=U \lam {y} Uy => covering-id $ inP (y, Uy, id, idp)

    \lemma covering-sub {x : C} {V U : Presieve x} (x<=V : Covering x V) (V<=U : V ⊆ U) : Covering x U \elim x<=V
      | covering-inj s p ps=id Vy => covering-inj s p ps=id (V<=U Vy)
      | covering-trans x<=T T<=V => covering-trans x<=T \lam Ty => covering-sub (T<=V Ty) \lam {z} (inP (v,Vv,f,q)) => inP (v, V<=U Vv, f, q)

    \lemma covering-stable {x : C} {y : C} (h : Hom x y) {V : Presieve y} (y<=V : Covering y V)
      : Covering x (\lam px => ∃ (py : V) (f : Hom px. py.) (py. ∘ f = h ∘ px.)) \elim y<=V
      | covering-inj {z} s p ps=id Vp => covering-id $ inP ((z,p), Vp, s ∘ h, inv o-assoc *> pmap (∘ h) ps=id *> id-left *> inv id-right)
      | covering-trans y<=T R => \case cover-stable h y<=T \with {
        | inP (pT,x<=pT,pT<=T) => covering-trans x<=pT \lam {pt} pTpt => \case pT<=T pTpt \with {
          | inP (t,Tt,pt>t,pt>t_h) => covering-sub (covering-stable pt>t (R Tt)) \lam {pz} (inP (z, inP (v,Vv,z>v,z>v_t), pz>z,pz>z_pt>t)) =>
            inP ((pz., pt. ∘ pz.), inP (v, Vv, z>v ∘ pz>z, inv o-assoc *> pmap (∘ _) z>v_t *> o-assoc *> pmap (_ ∘) pz>z_pt>t *> inv o-assoc *> pmap (∘ _) pt>t_h *> o-assoc), id, id-right)
        }
      }

    \lemma covering-stable-retract {x : C} {y : C} (g : Hom y x) (h : Hom x y) (h_g : h ∘ g = id) {V : Presieve y}
      (c : Covering x (\lam px => ∃ (py : V) (f : Hom px. py.) (py. ∘ f = h ∘ px.))) : Covering y V
      => covering-refine (covering-stable g c) \lam {py} (inP (px, inP (v,Vv,px_v,px_v_h), py_px, py_px_g)) =>
        inP (v, Vv, px_v ∘ py_px, inv o-assoc *> pmap (∘ _) px_v_h *> o-assoc *> pmap (h ∘) py_px_g *> inv o-assoc *> pmap (∘ _) h_g *> id-left)

    \lemma covering-refine {x : C} {V U : Presieve x} (x<=V : Covering x V) (V<=U : Presieve.Refines V U) : Covering x U \elim x<=V
      | covering-inj s p ps=id Vp => \case V<=U Vp \with {
        | inP (z,Uz,f,zf=p) => covering-inj (f ∘ s) z. (inv o-assoc *> pmap (∘ s) zf=p *> ps=id) Uz
      }
      | covering-trans x<=T T<=V => covering-trans x<=T \lam Ty => covering-sub (T<=V Ty) \lam {z} (inP (v,Vv,f,c)) => \case V<=U Vv \with {
        | inP (u,Uu,g,d) => inP (u, Uu, g ∘ f, inv o-assoc *> pmap (∘ f) d *> c)
      }

    \lemma covering-trans* {x : C} {U V : Presieve x} (x<=V : Covering x V)
                           (R : ∀ {y : V} (Covering y. \lam z => ∃ (u : U) (f : Hom z. u.) (u. ∘ f = y. ∘ z.)))
      : Covering x U \elim x<=V
      | covering-inj s p ps=id Tp => covering-refine (covering-stable s (R Tp)) \lam {px} (inP (py, inP (u,Uu,py>u,py>u_p), px>py, px>py_s)) =>
        inP (u, Uu, py>u ∘ px>py, inv o-assoc *> pmap (∘ _) py>u_p *> o-assoc *> pmap (p ∘) px>py_s *> inv o-assoc *> pmap (∘ _) ps=id *> id-left)
      | covering-trans x<=T T<=V => covering-trans x<=T \lam {z} Tz => covering-trans* (T<=V Tz) \lam {w} (inP (v,Vv,w>v,w>v_z)) =>
        covering-sub (covering-stable w>v (R Vv)) \lam {a} (inP (b, inP (u,Uu,b>u,b>u_v), a>b, a>b_w>v)) =>
          inP ((a., w. ∘ a.), inP (u, Uu, b>u ∘ a>b, inv o-assoc *> pmap (∘ _) b>u_v *> o-assoc *> pmap (_ ∘) a>b_w>v *> inv o-assoc *> pmap (∘ _) w>v_z *> o-assoc), id, id-right)
  }