\import Category
\import Category.Functor
\import Equiv
\import Function.Meta
\import Meta
\import Paths
\import Paths.Meta

\class RightAdjoint \extends Functor {
  | LAdj : Functor D C
  | eta : NatTrans Id (Comp \this LAdj)
  \field isAdjoint {X : D} {Y : C} : Equiv {Hom (LAdj X) Y} {Hom X (F Y)} (Func __ ∘ eta X)

  \func epsilon : NatTrans (Comp LAdj \this) Id \cowith
    | trans X => isAdjoint.ret (id _)
    | natural f => isAdjoint.isInj $ unfold $ rewrite (Func-o, Func-o, o-assoc, o-assoc, isAdjoint.f_ret, id-right, inv (eta.natural _), inv o-assoc, isAdjoint.f_ret) id-left

  \lemma eta_epsilon-left (Y : C) : Func (epsilon Y) ∘ eta (F Y) = id (F Y)
    => isAdjoint.f_ret _

  \lemma eta_epsilon-right (X : D) : epsilon (LAdj X) ∘ LAdj.Func (eta X) = id (LAdj X)
    => isAdjoint.isInj $ unfold $ rewrite (Func-id, Func-o, o-assoc, inv (eta.natural _), inv o-assoc, isAdjoint.f_ret) idp

  \lemma adjoint_epsilon {X : D} {Y : C} (f : Hom X (F Y)) : isAdjoint.ret f = epsilon Y ∘ LAdj.Func f
    => isAdjoint.isInj $ unfold $ isAdjoint.f_ret _ *> rewrite (Func-o, o-assoc, inv (eta.natural _), inv o-assoc, isAdjoint.f_ret, id-left) idp

  \lemma eta_eps_equiv {X : D} {Y : C} : QEquiv {Hom (LAdj X) Y} {Hom X (F Y)} (Func __ ∘ eta X) (epsilon Y ∘ LAdj.Func __) \cowith
    | ret_f f => inv (adjoint_epsilon _) *> isAdjoint.ret_f _
    | f_sec g => rewriteI adjoint_epsilon (isAdjoint.f_ret _)
} \where {
    \func rightFactor {C D E : Precat} (G1 : FullyFaithfulFunctor D E) (G2 : Functor E D) (adj : RightAdjoint { | Functor => Comp G1 G2 }) : RightAdjoint \cowith
      | Functor => G2
      | LAdj => Comp adj.LAdj G1
      | eta {
        | trans Y => G1.inverse (adj.eta (G1 Y))
        | natural h => run {
            G1.isFullyFaithful.isInj,
            repeat {} (rewrite G1.Func-o),
            repeat {} (rewrite G1.inverse-right),
            adj.eta.natural (G1.Func h)
          }
      }
      | isAdjoint => \new QEquiv {
        | ret h => adj.isAdjoint.ret (G1.Func h)
        | ret_f h => rewrite (G1.Func-o, G1.inverse-right) (adj.isAdjoint.ret_f _)
        | f_sec h => run {
            G1.isFullyFaithful.isInj,
            rewrite (G1.Func-o, G1.inverse-right),
            adj.isAdjoint.f_ret _
          }
      }
  }

\class CatEquiv \extends FullyFaithfulFunctor, RightAdjoint {
  \field eta-iso {X : D} : Iso (eta X)
  \field epsilon-iso {Y : C} : Iso (epsilon Y)
  | isFullyFaithful => TwoOutOfThree.rightFactor _ (symQEquiv isAdjoint) $ transport (QEquiv __) (ext \lam h => inv (adjoint_epsilon _ *> epsilon.natural h)) epsilon-iso.-o_Equiv

  \func op : CatEquiv \cowith
    | Functor => Functor.op
    | LAdj => LAdj.op
    | eta => NatTrans.op {eta.iso eta-iso}
    | isAdjoint {X} {Y} => \new QEquiv {
      | ret g => LAdj.Func g ∘ epsilon-iso.hinv
      | ret_f f => run {
        rewrite LAdj.Func-o,
        rewriteEq (inv (natural {epsilon.iso epsilon-iso} f)),
        inv,
        Iso.adjoint {LAdj.Func-iso eta-iso},
        epsilon-iso.adjoint,
        rewriteEq (eta_epsilon-right X),
        id-left
      }
      | f_sec => unfold \lam g => run {
        rewrite Func-o,
        rewriteEq (natural {eta.iso eta-iso} g),
        inv,
        Iso.adjoint' {Func-iso epsilon-iso},
        eta-iso.adjoint',
        rewriteEq (eta_epsilon-left Y),
        id-right
      }
    }
    | eta-iso => eta-iso.op.reverse
    | epsilon-iso => unfold $ rewrite (LAdj.Func-id,id-left) epsilon-iso.op.reverse

  \func reverse : CatEquiv \cowith
    | Functor => LAdj
    | LAdj => \this
    | eta => epsilon.iso epsilon-iso
    | isAdjoint => \new QEquiv {
      | ret h => eta-iso.hinv ∘ Func h
      | ret_f h => rewrite (Func-o, inv o-assoc, natural {eta.iso eta-iso}, o-assoc) $
                    pmap (h ∘) (pmap (`∘ _) (inv (Iso.adjoint' (eta_epsilon-left _) *> id-left )) *> f_hinv {Functor.Func-iso epsilon-iso}) *> id-right
      | f_sec h => rewrite (LAdj.Func-o, o-assoc, inv (natural {epsilon.iso epsilon-iso} _), inv o-assoc) $
                    pmap (`∘ h) (pmap (_ ∘) (inv (epsilon-iso.adjoint (eta_epsilon-right _) *> id-right)) *> hinv_f {LAdj.Func-iso eta-iso}) *> id-left
    }
    | eta-iso => epsilon-iso.reverse
    | epsilon-iso => unfold $ rewrite (Func-id,id-right) eta-iso.reverse
}