\import Algebra.Meta
\import Category
\import Category.Functor
\import Category.Limit
\import Category.Topos.Presheaf
\import Equiv
\import Function (IsInj)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set.SetCategory
\import Set.SetHom

\func HomLeft.{o,h} {C : Precat.{o,h}} (c : C) : Functor C.op SetCat.{h} \cowith
  | F x => C.Hom x c
  | Func f g => g ∘ f
  | Func-id => exts (\lam _ => id-right)
  | Func-o => exts (\lam _ => inv o-assoc)

\func HomPresheaf.{o,h} {C : Precat.{o,h}} (c : C) : Presheaf C \cowith
  | F => HomLeft c

\func Yoneda-trans.{o,h} {C : Precat.{o,h}} {a : C} {F : Functor C.op SetCat.{h}} (x : F a) : NatTrans (HomLeft a) F \cowith
  | trans _ f => F.Func f x
  | natural f => exts \lam g => path \lam i => F.Func-o i x

\func Yoneda-lemma.{o,h} {C : Precat.{o,h}} {a : C} {F : Functor C.op SetCat.{h}} : QEquiv {NatTrans (HomLeft a) F} {F a} \cowith
  | f nat => nat a id
  | ret => Yoneda-trans
  | ret_f nf => exts \lam _ => exts \lam f => inv (path \lam i => nf.natural f i id) *> unfold (rewrite id-left idp)
  | f_sec x => path \lam i => F.Func-id i x

\lemma Yoneda-apply.{o,h} {C : Precat.{o,h}} {a : C} (S T : Functor C.op SetCat.{h}) (f : NatTrans S T) {x : S a} : f ∘ Yoneda-trans x = Yoneda-trans (f a x)
  => (Yoneda-lemma {C} {a} {T}).adjoint $ pmap (f a) $ path \lam i => S.Func-id i x

\func Yoneda.{o,h} {C : Precat.{o,h}} : FullyFaithfulFunctor C (PresheafCat C) \cowith
  | F => HomPresheaf
  | Func {x y : C} (f : Hom x y) : NatTrans (HomLeft x) (HomLeft y) \cowith {
    | trans _ => \lam g => f ∘ g
    | natural _ => exts (\lam _ => inv $ o-assoc)
  }
  | Func-id => exts (\lam _ => exts (\lam _ => id-left))
  | Func-o => exts (\lam _ => exts (\lam _ => unfold $ o-assoc))
  | isFullyFaithful {X} {Y} => inP \new QEquiv {
    | ret => Yoneda-lemma
    | ret_f _ => id-right
    | f_sec => Yoneda-lemma.ret_f
  }

\instance PrecategoryOfElements.{s,o,h} {C : Precat.{o,h}} (P : Presheaf.{s} C) : Precat
  | Ob => \Sigma (c : C) (p : P c)
  | Hom x y => \Sigma (u : Hom x. y.) (\property x. = P.F.Func u y.)
  | id => (id, rewrite P.F.Func-id idp)
  | o (u, eq) (u', eq') => (u ∘ u', eq' *> rewrite (eq, P.F.Func-o) idp)
  | id-left => exts id-left
  | id-right => exts id-right
  | o-assoc => exts o-assoc
  \where {
    \func projection.{s,o,h} {C : Precat.{o,h}} (P : Presheaf.{s} C) : Functor (PrecategoryOfElements P) C \cowith
      | F (x, _) => x
      | Func (f, _) => f
      | Func-id => idp
      | Func-o => idp

    \func functorial.{s,o,h} {C : Precat.{o,h}} (P F : Presheaf.{s} C) (nat : Hom P F)
      : Functor (PrecategoryOfElements P) (PrecategoryOfElements F) \cowith
      | F (c, p) => (c, nat c p)
      | Func {(c, p)} {(c', p')} (h, eq) => (h, rewrite eq $ path \lam i => nat.natural h i p')
      | Func-id => exts $ idp
      | Func-o => exts $ idp
  }

\func PresheafColimit.{o,h} {C : Precat.{o,h}} (P : Presheaf.{h} C) : Colimit (Comp Yoneda (PrecategoryOfElements.projection P)) P \cowith
  | coneMap (c, p) => \new NatTrans {
    | trans _ h => P.F.Func h p
    | natural _ => exts (\lam _ => unfold $ rewrite P.F.Func-o idp)
  }
  | coneCoh {(c,p)} {(c', p')} (f , eq) => exts \lam _ => exts \lam _ => unfold $ rewrite eq $ unfold $ rewrite P.F.Func-o idp
  | limMap {G} cone => \new NatTrans {
    | trans X p => Yoneda-lemma (cone.coneMap (X, p))
    | natural {X} {Y} f => exts \lam g =>
      \let | ch => cone.coneCoh {X, g} {Y, Func {P} f g} (f, idp)
           | nat => (cone.coneMap (X, g)).natural f
           | nat-applied => path \lam i => nat i id
      \in run {
        repeat {} unfold,
        rewriteI ch,
        repeat {} unfold,
        rewrite id-right,
        unfold, unfold,
        rewriteI nat-applied,
        unfold, rewrite id-left idp
      }
    }
  | limBeta {Z} _ p0 => \case \elim p0 \with {
    | (Y, p) => (Yoneda-lemma {_} {_} {Z}).isInj $ unfold $ unfold $ rewrite P.F.Func-id idp
  }
  | limUnique eq => exts \lam X => exts \lam p =>
    \let | elem : PrecategoryOfElements P => (X, p)
         | eq-app => eq (X, p)
         | eq' => path (\lam i => (eq-app i) X)
         | eq'' => path (\lam i => (eq' i) id)
    \in repeat {} unfold at eq'' $ (rewriteI (path (\lam i => (Func-id {P} {X}) i p) : Func {P} {X} {X} id p = p)) eq''

\open PrecategoryOfElements

\func YonedaLift.{s,o,h} {C : Precat.{s,s}} {E : CocompletePrecat.{s,o,h}} (A : Functor C E) : Functor (PresheafCat.{s} C) E \cowith
  | F P => ObjLift A P
  | Func {X} {Y} f => Limit.transFuncMap (ObjLift A X) (ObjLift A Y) (functorial X Y f).op (induced-natural f)
  | Func-id {X} => (ObjLift A X).limUniqueBeta {ObjLift A X} \case \elim __ \with {
    | (c, p) => repeat {} unfold $ rewrite (id-right, id-left {_} {_} {ObjLift A X}) $ idp
  }
  | Func-o {X} {Y} {Z} {g} {f} => (ObjLift A X).limUniqueBeta {ObjLift A Z} \case \elim __ \with {
    | (c, p) => repeat {} unfold $ id-right *> rewrite (o-assoc,
      unfold in (ObjLift A X).limBeta (cone-in-induced f) (c, p), id-left,
      unfold in (ObjLift A Y).limBeta (cone-in-induced g) (c, f c p), id-left) idp
  }
  \where {
    \func diagram.{s,o,h} {C : Precat.{s,s}} {E : CocompletePrecat.{s,o,h}} (A : Functor C E) (P : Presheaf.{s} C) : Functor (PrecategoryOfElements P) E
      => Comp A (projection P)

    \func ObjLift.{s,o,h} {C : Precat.{s,s}} {E : CocompletePrecat.{s,o,h}} (A : Functor C E) (P : Presheaf.{s} C)
      => E.colimit (diagram A P)

    \func induced-natural.{s,o,h} {C : Precat.{s,s}} {E : CocompletePrecat.{s,o,h}} {A : Functor C E} {X Y : Presheaf.{s} C} (f : NatTrans X Y)
      : NatTrans (Comp (diagram A Y).op (functorial X Y f).op) (diagram A X).op \cowith
      | trans (q, a) => id
      | natural _ => repeat {} unfold $ rewrite (id-left, id-right) idp

    \func cone-in-induced.{s,o,h} {C : Precat.{s,s}} {E : CocompletePrecat.{s,o,h}} {A : Functor C E} {X Y : Presheaf.{s} C} (f : NatTrans X Y)
      => Limit.transFuncMap.cone {_} {ObjLift A X} {ObjLift A Y} {(functorial X Y f).op} {induced-natural f}
  }

\func YonedaLift_Yoneda.{s,o,h} {C : Precat.{s,s}} {E : CocompletePrecat.{s,o,h}} (A : Functor C E)
  : Iso {FunctorPrecat C E} {A} {Comp (YonedaLift A) Yoneda}
  => nat.iso \lam {X} => nat-iso X
  \where {
    \open YonedaLift

    \protected \func nat : NatTrans A (Comp (YonedaLift A) Yoneda) \cowith
      | trans x => (ObjLift A (HomPresheaf x)).coneMap (x, id)
      | natural {X} {Y} f => inv $ (ObjLift A (HomPresheaf X)).limBeta (cone-in-induced {_} {_} {_} {HomPresheaf X} (Yoneda.Func f)) (X, id) *>
          id-right *> cong id-right *> inv ((ObjLift A (HomPresheaf Y)).coneCoh {Y, id} {X, f} (f, inv id-left))

    \protected \lemma nat-iso (x : C) : Iso (nat x) \cowith
      | hinv => (ObjLift A (HomPresheaf x)).limMap cone
      | hinv_f => (ObjLift A (HomPresheaf x)).limBeta cone _ *> A.Func-id
      | f_hinv => (ObjLift A (HomPresheaf x)).limUnique \lam j => o-assoc *> pmap (_ ∘) ((ObjLift A (HomPresheaf x)).limBeta cone _) *> (ObjLift A (HomPresheaf x)).coneCoh (j., inv id-left) *> inv id-left
      \where {
        \func cone : Cone (diagram A (HomPresheaf x)).op (A x) \cowith
          | coneMap j => A.Func j.
          | coneCoh h => inv $ pmap A.Func h. *> A.Func-o
      }
  }

\lemma presheaf-mono-char.{o,h} {C : Precat.{o,h}} {S T : Presheaf.{h} C} {f : NatTrans S T} : Mono {PresheafCat.{h} C} f <-> ∀ {a} (IsInj (f a))
  => (\lam fm {a} p => (symQEquiv Yoneda-lemma).isInj $ fm.isMono {Yoneda a} $ Yoneda-apply S T f *> pmap Yoneda-trans p *> inv (Yoneda-apply S T f), \lam fi => \new Mono {
        | isMono p => exts \lam a => ext \lam x => fi $ path \lam i => p i a x
      })