{-# OPTIONS --without-K --rewriting --overlapping-instances #-}

open import lib.Basics
open import lib.NType2
open import lib.types.Group
open import lib.types.List
open import lib.types.Pi
open import lib.types.SetQuotient
open import lib.types.Word
open import lib.groups.GeneratedGroup
open import lib.groups.Homomorphism

module lib.groups.GeneratedAbelianGroup {i} {m} where

module GeneratedAbelianGroup (A : Type i) (R : Rel (Word A) m) where

  data AbGroupRel : Word A  Word A  Type (lmax i m) where
    agr-commutes :  l₁ l₂  AbGroupRel (l₁ ++ l₂) (l₂ ++ l₁)
    agr-rel :  {l₁ l₂}  R l₁ l₂  AbGroupRel l₁ l₂

    module Gen = GeneratedGroup A AbGroupRel
  open Gen hiding (module HomomorphismEquiv; rel-holds) public

  agr-reverse : (w : Word A)  QuotWordRel (reverse w) w
  agr-reverse nil = qwr-refl idp
  agr-reverse (x :: w) =
    reverse w ++ (x :: nil)
      qwr⟨ qwr-rel (agr-commutes (reverse w) (x :: nil)) 
    x :: reverse w
      qwr⟨ qwr-cong-r (x :: nil) (agr-reverse w) 
    x :: w qwr∎

  GenAbGroup : AbGroup (lmax i m)
  GenAbGroup = grp , grp-is-abelian
    grp : Group (lmax i m)
    grp = GenGroup
    module grp = Group grp
    grp-is-abelian : is-abelian grp
    grp-is-abelian =
      QuotWord-elim {P = λ a   b  grp.comp a b == grp.comp b a}
          QuotWord-elim {P = λ b  grp.comp qw[ la ] b == grp.comp b qw[ la ]}
             lb  quot-rel (qwr-rel (agr-commutes la lb)))
             _  prop-has-all-paths-↓))
         _  prop-has-all-paths-↓ {{Π-level  _  ⟨⟩)}})

  rel-holds :  {w₁} {w₂} (r : R w₁ w₂)  qw[ w₁ ] == qw[ w₂ ]
  rel-holds r = Gen.rel-holds (agr-rel r)

  module GenAbGroup = AbGroup GenAbGroup

  {- Universal Properties -}
  module HomomorphismEquiv {j} (G : AbGroup j) where

      module G = AbGroup G
      module R-RFs = RelationRespectingFunctions A R G.grp
      module AbGroupRel-RFs = RelationRespectingFunctions A AbGroupRel G.grp

    open R-RFs public

      legal-functions-equiv : R-RFs.RelationRespectingFunction
      legal-functions-equiv =
        equiv to from
               lf  AbGroupRel-RFs.RelationRespectingFunction= idp)
               lf  R-RFs.RelationRespectingFunction= idp)
        to : R-RFs.RelationRespectingFunction  AbGroupRel-RFs.RelationRespectingFunction
        to (R-RFs.rel-res-fun f respects-R) =
          AbGroupRel-RFs.rel-res-fun f respects-AbGroupRel
          respects-AbGroupRel : AbGroupRel-RFs.respects-rel f
          respects-AbGroupRel (agr-commutes l₁ l₂) =
            Word-extendᴳ G.grp f (l₁ ++ l₂)
              =⟨ Word-extendᴳ-++ G.grp f l₁ l₂ 
            G.comp (Word-extendᴳ G.grp f l₁) (Word-extendᴳ G.grp f l₂)
              =⟨ G.comm (Word-extendᴳ G.grp f l₁) (Word-extendᴳ G.grp f l₂) 
            G.comp (Word-extendᴳ G.grp f l₂) (Word-extendᴳ G.grp f l₁)
              =⟨ ! (Word-extendᴳ-++ G.grp f l₂ l₁) 
            Word-extendᴳ G.grp f (l₂ ++ l₁) =∎
          respects-AbGroupRel (agr-rel r) = respects-R r
        from : AbGroupRel-RFs.RelationRespectingFunction  R-RFs.RelationRespectingFunction
        from (AbGroupRel-RFs.rel-res-fun f respects-AbGroupRel) =
          R-RFs.rel-res-fun f respects-R
          respects-R : R-RFs.respects-rel f
          respects-R r = respects-AbGroupRel (agr-rel r)

    extend-equiv : R-RFs.RelationRespectingFunction  (GenAbGroup.grp →ᴳ G.grp)
    extend-equiv =
      Gen.HomomorphismEquiv.extend-equiv G.grp ∘e legal-functions-equiv

    extend : R-RFs.RelationRespectingFunction  (GenAbGroup.grp →ᴳ G.grp)
    extend = –> extend-equiv