\import Category
\import Category.Adjoint
\import Category.Comma
\import Category.Functor
\import Category.Limit
\import Equiv
\import Function.Meta
\import HLevel
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\class RightAdjointCounit \extends Functor {
  | LAdj : Functor D C
  | epsilon : NatTrans (Comp LAdj \this) Id
  \field isAdjoint-inv {X : D} {Y : C} : Equiv {Hom X (F Y)} {Hom (LAdj X) Y} (epsilon Y ∘ LAdj.Func __)

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

  \func adjoint-eta  {X : D} {Y : C} (g : Hom (LAdj X) Y) : isAdjoint-inv.ret g = Func g ∘ eta X =>
    isAdjoint-inv.isInj $ unfold $ rewrite (isAdjoint-inv.f_ret _, Func-o {LAdj}) $
                                   rewriteI o-assoc $ rewrite (epsilon.natural, o-assoc, isAdjoint-inv.f_ret _, id-right) idp
} \where {
  \use \coerce fromAdjoint (F : RightAdjoint) : RightAdjointCounit \cowith
    | Functor => F
    | LAdj => F.LAdj
    | epsilon => F.epsilon
    | isAdjoint-inv => \new Equiv {
      | ret => F.isAdjoint
      | ret_f => F.eta_eps_equiv.f_sec
      | sec => F.isAdjoint
      | f_sec => F.eta_eps_equiv.ret_f
    }

  \use \coerce toAdjoint (F : RightAdjointCounit) : RightAdjoint => \new RightAdjoint {
    | Functor => F
    | LAdj => LAdj
    | eta => eta
    | isAdjoint => \new QEquiv {
      | ret => isAdjoint-inv
      | ret_f _ => unfold $ rewriteI (adjoint-eta _ ) $ isAdjoint-inv.f_ret _
      | f_sec _ => isAdjoint-inv.isInj $ unfold $ run {
        rewrite (Func-o {LAdj}),
        rewriteI o-assoc,
        rewrite (epsilon.natural, o-assoc, isAdjoint-inv.f_ret _, id-right) idp
      }
    }
  }
}

\func comma-precat {C D : Precat} (L : Functor D C) (b : C) => commaPrecat {D} {TrivialCat} {C} L (Const b)

\func comma-cat {C : Precat} {D : Cat} (L : Functor D C) (b : C) => commaCat {D} {TrivialCat} {C} L (Const b)

\class Coreflection {C D : Precat} (L : Functor D C) (B : C) {
  | \classifying Coreflected : D
  | corefl-map : Hom (L Coreflected) B
  \property isCoreflection {Z : D} : Equiv {Hom Z Coreflected} {Hom (L Z) B} (\lam x => corefl-map ∘ (L.Func x))

  \func to-comma : comma-precat L B => (Coreflected, (), corefl-map)

  \func coreflection-map (x : comma-precat L B) : Hom {comma-precat L B} x to-comma
    | (x, s, d) => (Equiv.ret {isCoreflection} d, id {TrivialCat} s, rewrite id-left $ Equiv.f_ret {isCoreflection} d)

  \func to-comma-terminal  : terminal-obj (comma-precat L B) => terminal-ind {comma-precat L B} to-comma
      (\lam (p, s, q) => Contr.make (coreflection-map (p, s, q))
          (\lam a => exts (inv $ Equiv.adjoint $ a. *> id-left, cases a. \with {
            | Graph.empty p1 => idp
            | Graph.cons e x => absurd e
          }))
      )
}
  \where {
    \func from-comma-terminal {C D : Precat} {L : Functor D C} {b : C} (terminal : terminal-obj (comma-precat L b))
      : Coreflection L b => \new Coreflection {
      | Coreflected => terminal.apex.
      | corefl-map => terminal.apex.
      | isCoreflection {z} => \new QEquiv {
        | ret g => (terminalMap' {comma-precat L b} {terminal} {z, (), g}).
        | f_sec y => (terminalMap' {comma-precat L b} {terminal} {z, (), y}). *> id-left
        | ret_f x =>
          \let x-comma : comma-precat L b => (z, (), terminal.apex. ∘ L.Func x)
               | x-map : Hom {comma-precat L b} x-comma terminal.apex => (x, id {TrivialCat} (), inv id-left)
          \in
            path (\lam i => ((inv $ terminal-unique' {comma-precat L b} {terminal} {x-comma} {x-map}) @ i).)
      }
    }

    \func terminal-in-comma {C D : Precat} (L : Functor D C) (B : C)
      : Section {Coreflection L B} {terminal-obj (comma-precat L B)} => \new Section {
      | f coref => Coreflection.to-comma-terminal {coref}
      | ret => Coreflection.from-comma-terminal
      | ret_f _ => idp
    }
      \where {
        \func to-comma-isInj (x y : Coreflection L B) (eq : Coreflection.to-comma-terminal {x} = Coreflection.to-comma-terminal {y})
          : x = y =>
          inv (ret_f {terminal-in-comma L B} x) *> pmap (ret {terminal-in-comma L B}) eq *> ret_f {terminal-in-comma L B} y
      }

    \use\level isProp {C : Precat} {D : Cat} {L : Functor D C} {B : C}
                      (x y : Coreflection L B) : x = y =>
      \let s : Coreflection.to-comma-terminal {x} = Coreflection.to-comma-terminal {y} => terminal-prop {comma-cat L B} _ _ \in
        terminal-in-comma.to-comma-isInj x y s
  }

\class RightAdjointCoreflection  \extends Functor {
  | L : Functor D C
  \field coreflection (Z : C) : Coreflection {C} {D} L Z
  | F X => coreflection X
  | Func {X} {_} f => Equiv.ret {isCoreflection} (f ∘ corefl-map {coreflection X})
  | Func-id {_} => unfold $ rewrite id-left $ inv $ Equiv.adjoint $ unfold $ rewrite (Func-id {L}, id-right) idp
  | Func-o {_} {Y} {Z} {_} {_} => run {
    unfold,
    inv,
    Equiv.adjoint,
    unfold,
    rewrite (Func-o {L}),
    rewriteI o-assoc ,
    rewrite (Equiv.f_ret {isCoreflection {coreflection Z}}),
    rewrite o-assoc ,
    rewrite (Equiv.f_ret {isCoreflection {coreflection Y}}),
    inv o-assoc
  }

  \func eval-trans : NatTrans (Comp L \this) Id \cowith {
    | trans c => corefl-map {coreflection c}
    | natural _ => unfold $ Equiv.f_ret {isCoreflection} _
  }

  \func is-adjoint-counit {X : D} {Y : C} : Equiv {Hom X (F Y)} {Hom (L X) Y} (eval-trans Y ∘ L.Func __) =>
    isCoreflection
}
  \where {
    \use \coerce toAdjointCounit(F : RightAdjointCoreflection) : RightAdjointCounit
    \cowith {
      | Functor => F
      | LAdj => F.L
      | epsilon => eval-trans
      | isAdjoint-inv => is-adjoint-counit
    }

    \use \coerce fromAdjointCounit (F : RightAdjointCounit) : RightAdjointCoreflection F.C F.D F.LAdj \cowith {
      | coreflection => \lam Z => \new Coreflection {
        | Coreflected => F Z
        | corefl-map => F.epsilon Z
        | isCoreflection => F.isAdjoint-inv
      }}

    \use\level isProp {C : Precat} {D : Cat} (L : Functor D C)
    (adj1 adj2 : RightAdjointCoreflection C D L) : adj1 = adj2
      \elim adj1, adj2
        | (coref1), (coref2) => exts (\lam Z => Coreflection.isProp {C} {D} {L} (coreflection {coref1} Z) (coreflection{coref2} Z))
  }