\import Category
\import Category.Adjoint
\import Category.Functor
\import Category.Limit
\import Equiv
\import Function.Meta
\import Homotopy.Fibration
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\func subPrecat {C : Precat} {X : \Type} (f : X -> C) : Precat X \cowith
  | Hom x y => Hom (f x) (f y)
  | id => id
  | o h g => o h g
  | id-left => id-left
  | id-right => id-right
  | o-assoc => o-assoc
  \where {
    \func embedding {C : Precat} {X : \Type} (f : X -> C) : FullyFaithfulFunctor (subPrecat f) C f \cowith
      | Func h => h
      | Func-id => idp
      | Func-o => idp
      | isFullyFaithful => inP idEquiv

    \func pred {C : Precat} (P : C -> \Prop) => subPrecat (Total.proj P)
      \where
        \func embedding {C : Precat} (P : C -> \Prop) => subPrecat.embedding (Total.proj P)

    \func funcLift {C D : Precat} {X : \Type} (f : X -> D) (g : C -> X) (G : Functor C D) (p : \Pi {a : C} -> Iso {D} {f (g a)} {G a}) : Functor C (subPrecat f) g \cowith
      | Func h => p.hinv ∘ G.Func h ∘ p.f
      | Func-id => rewrite (G.Func-id, id-right) p.hinv_f
      | Func-o => rewrite G.Func-o $ later (rewrite (p.f_hinv, id-left) $ pmap (∘ _) (inv o-assoc) *> o-assoc) *> pmap (_ ∘) (pmap (∘ _) o-assoc *> o-assoc) *> inv o-assoc
  }

\func subCat {C : Cat} {X : \Type} (e : Embedding {X} {C}) : Cat \cowith
  | Precat => subPrecat e
  | univalence => faithful-univalence (subPrecat.embedding e) e
  \where {
    \lemma faithful-univalence {C : Precat} {D : Cat} (F : FaithfulFunctor C D) (e : Embedding F) {a b : C} : IsEquiv (C.idtoiso {a} {b})
      => Cat.makeUnivalence \lam j =>
        \have (t,r) => Cat.univalenceToTransport (F.Func-iso j)
        \in ((e.isEmb j.dom j.cod).sec t, F.isFaithful $ inv id-right *> inv (Functor.transport_Hom-right _ F) *> pmap (transport (Hom (e j.dom)) __ _) ((e.isEmb j.dom j.cod).f_sec t) *> r)

    \lemma faithful-reflects-iso {C : Precat} {D : Cat} (F : FaithfulFunctor C D) (e : Embedding F) {a b : C} {f : Hom a b} (fi : Iso (F.Func f)) : Iso f
      => \let | coh => Jl (\lam b p => F.Func (C.=_hom p) = D.=_hom (pmap e p)) F.Func-id
              | p => (e.isEmb a b).sec (D.isotoid fi)
         \in transport (Iso __) (F.isFaithful $ coh p *> pmap D.=_hom ((e.isEmb a b).f_sec (D.isotoid fi)) *> D.idtoiso_isotoid) (C.idtoiso p)
  }

\lemma subCat-iso {C : Precat} {X : \Type} {f : X -> C} (e : Iso {subPrecat f}) : Iso {C} {f e.dom} {f e.cod} e \cowith
  | hinv => e.hinv
  | hinv_f => e.hinv_f
  | f_hinv => e.f_hinv
  \where {
    \protected \lemma conv {C : Precat} {X : \Type} {f : X -> C} {x x' : X} (e : Iso {C} {f x} {f x'}) : Iso {subPrecat f} {x} {x'} e \cowith
      | hinv => e.hinv
      | hinv_f => e.hinv_f
      | f_hinv => e.f_hinv
  }

\class ReflectiveSubPrecat \extends FullyFaithfulFunctor {
  | reflector : D -> C
  | reflectorMap (X : D) : Hom X (F (reflector X))
  \field isReflective {X : D} {Y : C} : QEquiv {Hom (reflector X) Y} {Hom X (F Y)} (Func __ ∘ reflectorMap X)

  \func toAdjunction : Adjunction.FromReflector D C \this \cowith
    | LOb => reflector
    | etaMap => reflectorMap _
    | eta-adjoint => inP isReflective
} \where {
  \func fromAdjunction (A : Adjunction) {ff : \Pi {X Y : A.D} -> IsEquiv (RAdj.Func {X} {Y})} : ReflectiveSubPrecat \cowith
    | Functor => A.RAdj
    | isFullyFaithful => ff
    | reflector => A.LAdj
    | reflectorMap => A.eta
    | isReflective => A.eta_epsilon-equiv
}

\func reflectiveSubPrecatColimit {J : Precat} (I : ReflectiveSubPrecat) (F : Functor J I.C) (c : Colimit (Comp I F)) : Limit F.op \cowith
  | apex => I.reflector c.apex
  | coneMap j => I.inverse (reflectorMap _ ∘ c.coneMap j)
  | coneCoh h => I.isFaithful $ run {
    rewrite I.Func-o,
    repeat {} (rewrite I.inverse-right),
    rewrite o-assoc,
    pmap (_ ∘) (c.coneCoh h)
  }
  | limMap {z} c' => I.isReflective.ret (c.limMap (Cone.map I.op {J.op} c'))
  | limBeta c' j => IsEquiv.isInj I.isFullyFaithful $ Func-o *> pmap (_ ∘) I.inverse-right *> inv o-assoc *> pmap (∘ _) (I.isReflective.f_ret _) *> c.limBeta (Cone.map I.op {J.op} c') j
  | limUnique {z} {f} {g} p => inv (I.isReflective.ret_f f) *> pmap I.isReflective.ret (c.limUnique \lam j => o-assoc *> (rewrite I.inverse-right in inv I.Func-o *> pmap I.Func (p j) *> I.Func-o) *> inv o-assoc) *> I.isReflective.ret_f g