\import Category
\import Category.Comma
\import Category.Functor
\import Category.Limit
\import Function.Meta
\import Meta
\import Paths
\import Paths.Meta

\func LeftKanExt.{s,o} {C : Precat.{s,s}} {C' : Precat.{o,s}} {D : CocompletePrecat.{s}} (p : Functor C C') (F : Functor C D) : Functor C' D
  => Functor.op {RightKanExt D.op p.op F.op}

\func RightKanExt.{s,o} {C : Precat.{s,s}} {C' : Precat.{o,s}} (D : CompletePrecat.{s}) (p : Functor C C') (F : Functor C D) : Functor C' D \cowith
   | F c' => lim _ F c'
   | Func {x} {y} f => limMap {lim p F y} (Cone.premap (commaFunctor f) (lim p F x))
   | Func-id {x} => limUniqueBeta {lim p F x} {lim p F x} \lam j => path (\lam i => coneMap {lim p F x} (j., j., (id-right *> id-left) @ i)) *> inv id-right
   | Func-o {x} {y} {z} {g} {f} => limUniqueBeta {lim p F z} {lim p F x} \lam j => inv (pmap (∘ _) (limBeta {lim p F z} (Cone.premap (commaFunctor g) (lim p F y)) j) *>
       limBeta {lim p F y} (Cone.premap (commaFunctor f) (lim p F x)) (j., j., id ∘ j. ∘ g) *> path (\lam i => coneMap {lim p F x} (j., j., (pmap (∘ _) id-left *> o-assoc) @ i))) *> o-assoc
  \where {
    \open Limit

    \func lim.{s,o} {C : Precat.{s,s}} {C' : Precat.{o,s}} {D : CompletePrecat.{s}} (p : Functor C C') (F : Functor C D) (b : C')
      => D.limit (Comp F (commaPrecat.rightForget (Const {TrivialCat} b) p))

    \func commaFunctor {C C' : Precat} {p : Functor C C'} {x y : C'} (f : Hom y x)
      => commaPrecat.functor (Const {TrivialCat} x) (Const y) p p (Const.natTrans f) id

    -- | A limit of the form `lim_{j : J} (LeftKanExt.op D p F (G j))` is a double limit and can be expressed as a single limit of {F} over the comma category `G|p`.
    \class DoubleLimit.{s,o} \noclassifying {J C : Precat.{s,s}} {C' : Precat.{o,s}} {D : CompletePrecat.{s}} (p : Functor C C') (F : Functor C D) (G : Functor J C') {
      \lemma map_iso (c : Cone G) (e : Iso (lim'.limMap (map_cone c))) : Iso (limMap {D.limit (Comp (RightKanExt D p F) G)} (Cone.map (RightKanExt D p F) c))
        => Iso.rightFactor _ iso $ transport (Iso __) (lim'.limUniqueBeta {_} {map_cone c} \lam k => inv (pmap (∘ _) (lim'.limBeta cone k) *> o-assoc *> pmap (_ ∘) (limBeta (Cone.map (RightKanExt D p F) c) _) *>
              limBeta {limit (Comp F (commaPrecat.rightForget (Const {TrivialCat} (G k.)) p))} (Cone.premap (commaFunctor (c.coneMap k.)) (lim p F c)) ((), k., k.) *> repeat {} unfold (rewrite id-left idp)) *> o-assoc) e

      \func map_cone (c : Cone G) : Cone (Comp F (commaPrecat.rightForget G p)) \cowith
        | apex => RightKanExt D p F c
        | coneMap (j,z,f) => coneMap $ later ((), z, f ∘ c.coneMap j)
        | coneCoh {w} {w'} (h1,h2,h3) =>
          coneCoh {D.limit (Comp F (commaPrecat.rightForget (Const {TrivialCat} c) p))} {(), w., w. ∘ c.coneMap w.} {(), w'., w'. ∘ c.coneMap w'.}
            (Graph.empty idp, h2, id-right *> pmap (w'. ∘) (inv (c.coneCoh h1)) *> inv o-assoc *> pmap (∘ _) h3 *> o-assoc)

      \func iso : Iso {D} {D.limit (Comp (RightKanExt D p F) G)} {lim'} \cowith
        | f => lim'.limMap cone
        | hinv => limMap cone'
        | hinv_f => limUnique \lam j => inv o-assoc *> pmap (∘ _) (limBeta cone' j) *> limUnique (\lam w => inv o-assoc *> pmap (∘ _) (limBeta {lim p F (G j)} (cone'' j) w) *> lim'.limBeta cone (j, w., w.)) *> inv id-right
        | f_hinv => limUnique \lam w => inv o-assoc *> pmap (∘ _) (lim'.limBeta cone w) *> o-assoc *> pmap (_ ∘) (limBeta {D.limit (Comp (RightKanExt D p F) G)} cone' w.) *> limBeta {lim p F (G w.)} (cone'' w.) ((), w., w.) *> inv id-right

      \func lim' : Limit => D.limit (Comp F (commaPrecat.rightForget G p))

      \func cone : Cone (Comp F (commaPrecat.rightForget G p)) (D.limit (Comp (RightKanExt D p F) G)) \cowith
        | coneMap w => later (coneMap $ later ((), w., w.)) ∘ coneMap (commaPrecat.leftForget G p w)
        | coneCoh {w} {w'} h => inv o-assoc *> pmap (∘ _) (coneCoh {lim p F (G w.)} {(), w., w.} {(), w'., id ∘ w'. ∘ G.Func h.} (TrivialCat.id, h., id-right *> o-assoc *> id-left *> h.) *>
                                                            inv (limBeta {lim p F (G w'.)} (Cone.premap (commaFunctor (G.Func h.)) (lim p F (G w.))) ((), w'., w'.) )) *>
                                    o-assoc *> pmap (_ ∘) (coneCoh {D.limit (Comp (RightKanExt D p F) G)} h.)

      \func cone'' (j : J) : Cone (Comp F (commaPrecat.rightForget (Const {TrivialCat} (G j)) p)) lim' \cowith
        | coneMap y => coneMap $ later (j, y., y.)
        | coneCoh {y} {y'} h => lim'.coneCoh {j, y., y.} {j, y'., y'.} (id, h., pmap (y'. ∘) (later Func-id) *> h.)

      \func cone' : Cone (Comp (RightKanExt D p F) G) lim' \cowith
        | coneMap j => limMap {lim p F (G j)} (cone'' j)
        | coneCoh {j} {j'} h => limUnique \lam w => inv o-assoc *> pmap (∘ _) (limBeta {lim p F (G j')} (Cone.premap (commaFunctor (G.Func h)) (lim p F (G j))) w) *>
                                                      limBeta {lim p F (G j)} (cone'' j) (w., w., id ∘ w. ∘ G.Func h) *> inv (pmap (∘ _) Func-id *> id-left) *>
                                                      lim'.coneCoh {j, w., id ∘ w. ∘ G.Func h} {j', w., w.} (h, id, inv $ pmap (∘ _) Func-id *> id-left *> o-assoc *> id-left) *>
                                                      inv (limBeta {lim p F (G j')} (cone'' j') w)
    }
  }