\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Group.Sub
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.MonoidCategory
\import Algebra.Monoid.MonoidHom
\import Algebra.Pointed
\import Algebra.Pointed.PointedCategory
\import Algebra.Pointed.PointedHom
\import Category
\import Category.Functor
\import Category.Meta
\import Category.Subcat
\import Equiv
\import Function (IsInj, IsSurj)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set.SetCategory

\instance GroupCat : Cat Group
  | Hom => GroupHom
  | id _ => GroupHom.id
  | o => GroupHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam f _ => exts (f.func-ide, \lam _ _ => f.func-*, \lam _ => f.func-inverse)
  \where {
    \func ForgetSet : FaithfulFunctor GroupCat SetCat \cowith
      | F G => G
      | Func f => f
      | Func-id => idp
      | Func-o => idp
      | isFaithful => \lam p => ext p

    -- TODO: Prove this more generally for algebraic theories?
    \lemma Iso<->Inj+Surj {G H : Group} (f : GroupHom G H) : Iso {GroupCat} f <-> f.IsIsomorphism
      => (\lam p => SetIso->Inj+Surj (ForgetSet.Func-iso p),
          \lam p => \new Iso {
            | hinv => \new GroupHom {
              | func => inve p
              | func-ide => aux (this_iso p) f.func-ide
              | func-* {x y : H} => rewrite (this_inv_ap p x, this_inv_ap p y,
                                             inv f.func-*, inv $ inv_this_ap p (inve p x G.* inve p y),
                                             inv $ this_inv_ap p x, inv $ this_inv_ap p y ) idp
            }
            | hinv_f => exts \lam e => inv (inv_this_ap p e)
            | f_hinv => exts \lam e => inv (this_inv_ap p e)
          })
      \where \private {
      {- | some  set theoretic lemmas -}

        \lemma this_inv_ap (p : f.IsIsomorphism) (h : H) : h = f (inve p h)
          => inv (path \lam i => (Iso.f_hinv {this_iso p} i) h)

        \lemma inv_this_ap (p : f.IsIsomorphism) (g : G) : g = inve p (f g)
          => inv (path \lam i => (Iso.hinv_f {this_iso p} i) g)

        \func this_iso (p : f.IsIsomorphism) => Inj+Surj->SetIso f p. p.

        \func inve (p : f.IsIsomorphism) => Iso.hinv {this_iso p}

        \lemma aux {A B : \Set} (f : Iso {SetCat} {A} {B}) {a : A} {b : B} (p : f.f a = b) : f.hinv b = a
          => inv $ rewrite (aux' f, p) idp

        \lemma aux' {A B : \Set} (f : Iso {SetCat} {A} {B}) {a : A} : a = f.hinv (f.f a)
          => inv (path (\lam i => (f.hinv_f i) a))

        \lemma aux'' {A B : \Set} (f : Iso {SetCat} {A} {B}) {b : B} : b = f.f (f.hinv b)
          => inv (path (\lam i => (f.f_hinv i) b))

        \lemma SetIso->Inj+Surj(f : Iso {SetCat}) : \Sigma (IsInj f.f) (IsSurj f.f)
          => ((SetIso->Equiv f).isInj, (SetIso->Equiv f).isSurj )

        \lemma Inj+Surj->SetIso {X Y : \Set} (f : X -> Y) (p : IsInj f) (q : IsSurj f) : Iso {SetCat} f
          => Equiv->SetIso (Equiv.fromInjSurj f p q)

        \lemma Equiv->SetIso {X Y : \Set} {f : X -> Y} (eq : Equiv f) : Iso {SetCat} f \cowith
          | hinv => Equiv.ret {eq}
          | hinv_f => ext (Equiv.ret_f {eq})
          | f_hinv => ext (Equiv.f_ret {eq})

        \lemma SetIso->Equiv {X Y : \Set} {f : X -> Y} (p : Iso {SetCat} f) : Equiv f => \new QEquiv {
          | ret => Iso.hinv {p}
          | ret_f x => inv (aux' p {x})
          | f_sec y => inv (aux'' p {y})
        }
      }

    \lemma Iso<->TrivialKer+Surj {G H : Group} (f : GroupHom G H)
      : Iso {GroupCat} f <-> (\Sigma f.TrivialKernel (IsSurj f))
      => <->trans (Iso<->Inj+Surj f) helper
      \where \private \func helper : (\Sigma (IsInj f) (IsSurj f)) <-> (\Sigma f.TrivialKernel (IsSurj f)) =>
        (\lam p => (f.Kernel-injectivity-corrolary p., p.),
         \lam p => (f.Kernel-injectivity-test p., p.))
  }

\func quotient-map {S : Group} {H : NormalSubGroup S} : GroupHom S H.quotient \cowith
  | func (s : S) => NormalSubGroup.quotient-proj-setwise s
  | func-ide => idp
  | func-* => idp

\instance ImageGroup (f : GroupHom) : Group
  | Monoid => ImageMonoid f
  | inverse a => (inverse a., TruncP.map a. \lam s => (inverse s., f.func-inverse *> pmap inverse s.))
  | inverse-left => ext inverse-left
  | inverse-right => ext inverse-right

\func ImageGroupLeftHom (f : GroupHom) : GroupHom f.Dom (ImageGroup f) \cowith
  | MonoidHom => ImageMonoidLeftHom f

\func ImageGroupRightHom (f : GroupHom) : GroupHom (ImageGroup f) f.Cod \cowith
  | MonoidHom => ImageMonoidRightHom f

\func ImageSubGroup (f : GroupHom) : SubGroup f.Cod \cowith
  | contains h => ∃ (g : f.Dom) (f g = h)
  | contains_ide => inP (Group.ide {f.Dom}, f.func-ide)
  | contains_* cont1 cont2 => \case \elim  cont1, \elim  cont2 \with {
    | inP a, inP b => inP (a. * b., rewrite (f.func-*, a., b.) idp)
  }
  | contains_inverse cont1 => \case \elim cont1 \with {
    | inP a => inP (inverse a., rewrite (f.func-inverse, a.) idp)
  }

\instance AddGroupCat : Cat AddGroup
  | Hom G H => AddGroupHom G H
  | id _ => AddGroupHom.id
  | o g f => \new AddGroupHom {
    | func x => g (f x)
    | func-+ => pmap g func-+ *> func-+
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {X} {A} {B} p1 p2 => exts (p1.func-zro, \lam _ _ => p1.func-+, AddGroup.negative-equality A B p1.func-zro p1.func-+)
  \where {
    \func forgetToAddMonoid : Functor AddGroupCat AddMonoidCat \cowith
      | F A => A
      | Func f => f
      | Func-id => idp
      | Func-o => idp

    \func forget : Functor AddGroupCat SetCat \cowith
      | F R => R
      | Func f => f
      | Func-id => idp
      | Func-o => idp
  }

\instance AbGroupCat : Cat AbGroup
=> subCat \new Embedding {AbGroup} {AddGroup} {
  | f A => A
  | isEmb A B => \new Retraction {
    | sec => AbGroup.equals A B
    | f_sec => idpe
  }
} \where {
  \func forgetToAddGroup : Functor AbGroupCat AddGroupCat \cowith
    | F A => A
    | Func f => f
    | Func-id => idp
    | Func-o => idp

  \func forget : Functor AbGroupCat SetCat \cowith
    | F R => R
    | Func f => f
    | Func-id => idp
    | Func-o => idp
}

\instance KerAddGroup (f : AddGroupHom) : AddGroup
  | AddMonoid => KerAddMonoid f
  | negative a => (negative a., f.func-negative *> pmap negative a. *> AddGroup.negative_zro)
  | negative-left => ext negative-left
  | negative-right => ext negative-right

\func KerGroupHom (f : AddGroupHom) : AddGroupHom (KerAddGroup f) f.Dom \cowith
  | AddMonoidHom => KerMonoidHom f

\instance KerAbGroup {A : AbGroup} (f : AddGroupHom A) : AbGroup
  | AddGroup => KerAddGroup f
  | AbMonoid => KerAbMonoid f

\lemma kernel=0<->inj {f : AddGroupHom} : IsInj f <-> (\Pi (x : Kernel f) -> x = )
  => (\lam fi x => ext $ fi $ x. *> inv func-zro,
      \lam c {a} {a'} p => AddGroup.fromZero $ pmap __. (c (a - a', func-+ *> pmap (_ +) f.func-negative *> AddGroup.toZero p)))

\instance ImageAddGroup (f : AddGroupHom) : AddGroup
  | AddMonoid => ImageAddMonoid f
  | negative a => (negative a., TruncP.map a. \lam s => (negative s., f.func-negative *> pmap negative s.))
  | negative-left => ext negative-left
  | negative-right => ext negative-right

\func ImageAddGroupLeftHom (f : AddGroupHom) : AddGroupHom f.Dom (ImageAddGroup f) \cowith
  | AddMonoidHom => ImageAddMonoidLeftHom f

\func ImageAddGroupRightHom (f : AddGroupHom) : AddGroupHom (ImageAddGroup f) f.Cod \cowith
  | AddMonoidHom => ImageAddMonoidRightHom f

\instance ImageAbGroup {A : AddGroup} {B : AbGroup} (f : AddGroupHom A B) : AbGroup
  | AddGroup => ImageAddGroup f
  | AbMonoid => ImageAbMonoid f

\func conjugateHom {E : Group} (g : E) : GroupHom E E \cowith
  | func => conjugate g
  | func-ide => unfold conjugate $ rewrite (E.ide-right, E.inverse-right) idp
  | func-* {x y : E} =>
    \have aux {x y z w t e : E} : x * y * z * (w * t * e) = (x * y) * (z * w) * (t * e) => equation
    \in inv $ rewrite (aux, E.inverse-left, E.ide-right) equation