-- fundamental homomorphism theorem
--

open import Level hiding ( suc ; zero )
module fundamental (c l : Level) where

open import Algebra
open import Algebra.Structures
open import Algebra.Definitions
open import Data.Product
-- open import Function hiding (id ; flip)
-- open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
-- open import Function.LeftInverse  using ( _LeftInverseOf_ )
-- open import Function.Equality using (Π)
open import Relation.Binary.PropositionalEquality 
open import Algebra.Morphism.Structures
open GroupMorphisms

Group→Raw : Group c l → RawGroup c l
Group→Raw G = record {
     Carrier        = Carrier G
     ; _≈_          = _≈_ G
     ; _∙_          = _∙_ G
     ; ε            = ε G
     ; _⁻¹          = _⁻¹ G
  } where open Group

-- record Kernel {G H : Group } (f : Carrier G → Carrier H ) : Set ( c Level.⊔ l ) where
--   field
--      kernel :  Carrier H → Carrier G
--      isKernel : (x : Carrier H ) → kernel x ∙

record NormalSubGroup ( G : Group c l ) : Set ( c  Level.⊔  l ) where
  open Group G
  field
     sub : Carrier → Carrier 
     subgroup  : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub
     normal : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g

-- open RawGroup G₁ renaming
--     (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
-- open RawGroup G₂ renaming
--     (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)

data Coset (G : Group c l)  (NS : NormalSubGroup G) :  Group.Carrier G → Set c where
    coset : (a b : Group.Carrier G ) → Coset G NS ( Group._∙_ G a (NormalSubGroup.sub NS b) )

record CosetCarrier (G : Group c l)  (NS : NormalSubGroup G) :  Set ( c  Level.⊔  l ) where  
  field
    r :  Group.Carrier G
    isCoset : Coset G NS r

φ :   {G : Group c l} →  {NS : NormalSubGroup G} → Group.Carrier G → CosetCarrier G NS
φ {G} {NS} x = record { r = NormalSubGroup.sub NS x ; isCoset = p1 } where
   p1 :  Coset G NS (NormalSubGroup.sub NS x)
   p1 = subst (λ k →  Coset G NS k ) {!!} (coset {!!} {!!} )

Quotient : (G : Group c l)  (NS : NormalSubGroup G) → Group ( c  Level.⊔  l ) l
Quotient G NS = record {
     Carrier        = CosetCarrier G NS
     ; _≈_          = {!!}
     ; _∙_          = {!!}
     ; ε            = {!!}
     ; _⁻¹          = {!!}
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
       isEquivalence = {!!}
       ; ∙-cong = {!!} }
       ; assoc = {!!} }
       ; identity = {!!} }
       ; inverse   = {!!} 
       ; ⁻¹-cong   = {!!}
      } 
   } where 
      open Group G

record Fundamental (G H : Group c l)  
    (f : Group.Carrier G → Group.Carrier H ) 
    (homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f ) 
    (N : NormalSubGroup G ) :  Set ( c  Level.⊔  l ) where
  field
    h : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f