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

\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) => (isCoreflection.ret d, id {TrivialCat} s, rewrite id-left $ isCoreflection.f_ret d)

  \func to-comma-terminal  : terminal-obj (comma-precat L B) => isTerminal {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
      }

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

\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
  }

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

  \use \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 toAdjoint (F : RightAdjointCoreflection) : RightAdjointCounit \cowith
      | Functor => F
      | LAdj => F.L
      | epsilon => F.eval-trans
      | epsilon-adjoint => F.is-adjoint-counit

    \use \coerce fromAdjoint (F : RightAdjoint) : RightAdjointCoreflection F.C F.D F.LAdj \cowith
      | coreflection Z => \new Coreflection {
        | Coreflected => F Z
        | corefl-map => F.epsilon Z
        | isCoreflection => symQEquiv F.eta_epsilon-equiv
      }

    \sfunc 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 (coreflection {coref1} Z) (coreflection {coref2} Z))
  }