\import Category
\import Category.Functor
\import Category.Limit
\import Category.Subcat
\import Equiv
\import Function.Meta
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.SetCategory

-- | Presheaves valued in {D}
\record VPresheaf (D : Precat) (C : Precat) (\coerce F : Functor C.op D) {
  \func toPresheaf.{u} (U : Functor D SetCat.{u}) : Presheaf C \cowith
    | F => Comp U F
} \where {
    \func functor-at-point {D : Cat} {C : Precat} {J : Precat} (G : Functor J (VPresheafCat D C)) (c : C) : Functor J D \cowith
      | F j => G j c
      | Func f => G.Func f c
      | Func-id {X} => rewrite (G.Func-id {X}) idp
      | Func-o => rewrite G.Func-o idp
  }

-- | Presheaves valued in sets
\func Presheaf.{u} (C : Precat) => VPresheaf SetCat.{u} C

\instance VPresheafCat (D : Cat) (C : Precat) : Cat
  => subCat {FunctorCat C.op D} {VPresheaf D C} (\new Embedding {
    | f P => P
    | isEmb _ _ => \new Retraction {
      | sec p => ext p
      | f_sec => idpe
    }
  })

\instance PresheafCat.{u} (C : Precat) : Cat
  => VPresheafCat SetCat.{u} C

\instance VPresheafComplete.{u} (D : CompleteCat.{u}) (C : Precat) : CompleteCat.{u}
  | Cat => VPresheafCat D C
  | limit => limit
  | terminal {
    | apex => terminalPresheaf
    | proj => \case __
    | tupleMap _ => \new NatTrans {
      | trans _ => D.terminalMap
      | natural _ => D.terminal-unique
    }
    | tupleBeta {_} {_} {j} => \case j
    | tupleEq _ => exts \lam a => D.terminal-unique
  }
  | Bprod S T => \new Product {
    | apex => BprodPresheaf S T
    | proj => \case \elim __ \with {
      |  => \new NatTrans {
        | trans a => D.proj1
        | natural f => D.beta1
      }
      |  => \new NatTrans {
        | trans a => D.proj2
        | natural f => D.beta2
      }
    }
    | tupleMap h => \new NatTrans {
      | trans a => D.pair (h  a) (h  a)
      | natural f => D.pair-unique
        (inv o-assoc *> pmap (∘ _) D.beta1 *> (h ).natural f *> pmap (_ ∘) (inv D.beta1) *> inv o-assoc *> pmap (∘ _) (inv D.beta1) *> o-assoc)
        (inv o-assoc *> pmap (∘ _) D.beta2 *> (h ).natural f *> pmap (_ ∘) (inv D.beta2) *> inv o-assoc *> pmap (∘ _) (inv D.beta2) *> o-assoc)
    }
    | tupleBeta {z} {f} {j} => \case \elim j \with {
      |  => exts \lam a => D.beta1
      |  => exts \lam a => D.beta2
    }
    | tupleEq c => exts \lam a => D.pair-unique (path \lam i => c  i a) (path \lam i => c  i a)
  }
  \where {
    \protected \func limit.{u} {D : CompleteCat.{u}} {C : Precat} {J : Precat.{u,u}} (G : Functor J (VPresheafCat D C)) : Limit G \cowith
      | apex => apex
      | coneMap => cone-nat-map
      | coneCoh h => exts \lam _ => coneCoh h
      | limMap => lim-nat-map
      | limBeta {z} z-cone _ => exts \lam X => rewrite (limBeta {L X} (cone-at-point X z z-cone)) idp
      | limUnique j-unique => exts \lam X => limUnique $ \lam j => path (\lam i => j-unique j i X)
      \where {
        \func L (c : C) => D.limit {J} (VPresheaf.functor-at-point G c)

        \func cone {X Y : C} (f : Hom Y X) : Cone (VPresheaf.functor-at-point G Y) \cowith
          | apex => Cone.apex {L X}
          | coneMap j => Func f ∘ coneMap {L X} j
          | coneCoh h => rewriteI (coneCoh {L X} h, o-assoc, o-assoc)
              (rewrite (natural {Func {G} h} f) idp)

        \func apex : VPresheaf D C \cowith
          | F => \new Functor {
            | F c => L c
            | Func f => limMap (cone f)
            | Func-id {X} => limUnique \lam j => limBeta {L X} (cone id) j *> pmap (∘ _) Func-id *> id-left *> inv id-right
            | Func-o {_} {Y} {Z} {g} {f} => limUnique (\lam j => rewrite (limBeta {L Z} (cone (f ∘ g)) j, inv o-assoc,
                                                                          limBeta {L Z} (cone g) j) (unfold coneMap
                (rewrite (Func-o {G j}, o-assoc, o-assoc) (rewrite (limBeta {L Y} (cone f) j) (unfold coneMap idp)))))
          }

        \func cone-nat-map (j : J) : Hom apex (G j) => \new NatTrans {
          | trans c => coneMap {L c} j
          | natural {_} {Y} f => rewrite (limBeta {L Y} (cone f) j) idp
        }

        \func cone-at-point (X : C) (H : VPresheaf D C) (z-cone : Cone {J} G H) : Cone (VPresheaf.functor-at-point G X) (H X) \cowith
          | coneMap j => coneMap {z-cone} j X
          | coneCoh h => path (\lam i => ((coneCoh {z-cone} h) i) X)

        \func lim-nat-map {z : VPresheaf D C} (z-cone : Cone G z) : Hom z apex => \new NatTrans {
          | trans X => limMap $ cone-at-point X z z-cone
          | natural {X} {Y} f => limUnique \lam j =>
            rewrite (inv o-assoc, (L Y).limBeta (cone-at-point Y z z-cone) j,
                     inv o-assoc, (L Y).limBeta (cone f), o-assoc,
                     (L X).limBeta (cone-at-point X z z-cone))
              $ natural {coneMap {z-cone} j} f
        }
      }

    \func terminalPresheaf : VPresheaf D C \cowith
      | F {
        | F _ => terminal
        | Func _ => D.terminalMap
        | Func-id => D.terminal-unique
        | Func-o => D.terminal-unique
      }

    \func BprodPresheaf (S T : VPresheaf D C) : VPresheaf D C \cowith
      | F {
        | F a => Bprod (S a) (T a)
        | Func f => D.prodMap (S.F.Func f) (T.F.Func f)
        | Func-id => pmap2 D.prodMap S.F.Func-id T.F.Func-id *> D.prod-id
        | Func-o => pmap2 D.prodMap S.F.Func-o T.F.Func-o *> inv D.prodMap-comp
      }
  }

{-
-- the proof of this should be completely analogues to the CompleteCat (VPresheafCat) instance.
-- For example, it could be proven with a transport along the equality [C, D]^op = [C^op, D^op].
\instance VPresheafCocomplete.{s,o2,h2,o1,h1} (D : CocompleteCat.{s,o2,h2}) (C : Precat.{o1,h1}) : CocompleteCat.{s} (VPresheafCat D C)
  => {?}

\instance VPresheafCatBicomplete.{u} (D : BicompleteCat.{u}) (C : Precat) : BicompleteCat.{u} (VPresheafCat D C)
  | Cat => VPresheafCat D C
  | limit => limit {VPresheafComplete D C}
  | colimit => colimit {VPresheafCocomplete D C}

\func PresheafCatBicomplete.{u} (C : Precat) : BicompleteCat.{u} (PresheafCat.{u} C)
  => VPresheafCatBicomplete SetBicat.{u} C
-}

--\open PrecatWithBprod

--\instance PresheafCartesianClosed (C : SmallPrecat) : CartesianClosedPrecat
--  | CartesianPrecat => PresheafCatComplete C
--  | exp P => RightAdjointCoreflection.toAdjointCounit (\new RightAdjointCoreflection {
--    | C => PresheafCatComplete C
--    | D => PresheafCatComplete C
--    | L => bprodFunctorRight P
--    | coreflection Q => \new Coreflection {
--      | Coreflected => coreflected P Q
--      | corefl-map => \new NatTrans {
--        | trans c p => {?}
--        | natural => {?}
--      }
--      | isCoreflection => {?}
--    }
--  })
--\where {
--  \func coreflected (P Q : PresheafCatComplete C) : PresheafCat C =>
--      \new VPresheaf {
--        | F => Comp (VPresheaf.F {hom-presheaf Q}) (Functor.op {Comp (bprodFunctorRight P) (YonedaEmbedding {C})})
--      }
--}

--\instance PresheafTopos (C : SmallPrecat) : ToposPrecat
--  | FinCompletePrecat => PresheafCatBicomplete C
--  | CartesianClosedPrecat => PresheafCartesianClosed C
--  | subobj-classifier => {?}
--  | true-map => {?}
--  | char-map => {?}
--  | char-pullback => {?}
--  | char-unique => {?}