-- fundamental homomorphism theorem
--

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

open import Algebra
open import Algebra.Structures
open import Algebra.Definitions
open import Algebra.Core
open import Algebra.Bundles

open import Data.Product
open import Relation.Binary.PropositionalEquality 
open import Gutil0
import Gutil
import Function.Definitions as FunctionDefinitions

import Algebra.Morphism.Definitions as MorphismDefinitions
open import Algebra.Morphism.Structures 

open import Tactic.MonoidSolver using (solve; solve-macro)

--
-- Given two groups G and H and a group homomorphism f : G → H,
-- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K
-- (where G/K is the quotient group of G by K).
-- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.
--     https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms
--
--       f
--    G --→ H
--    |   /
--  φ |  / h
--    ↓ /
--    G/K
--

import Relation.Binary.Reasoning.Setoid as EqReasoning

_<_∙_> :  (m : Group c c )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
m < x ∙ y > =  Group._∙_ m x y

_<_≈_> :  (m : Group c c )  →    (f  g : Group.Carrier m ) → Set c 
m < x ≈ y > =  Group._≈_ m x y

infixr 9 _<_∙_>

--
--  Coset : N : NormalSubGroup →  { a ∙ n | G ∋ a , N ∋ n }
--


open GroupMorphisms

import Axiom.Extensionality.Propositional
postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m

record NormalSubGroup (A : Group c c )  : Set c  where
   open Group A
   field  
       ⟦_⟧ : Group.Carrier A → Group.Carrier A 
       normal :  IsGroupHomomorphism (GR A) (GR A)  ⟦_⟧
       comm : {a b :  Carrier } → b ∙ ⟦ a ⟧  ≈ ⟦ a ⟧  ∙ b 
       -- 
       factor : (a b : Carrier) → Carrier
       is-factor : (a b : Carrier) →  b ∙ ⟦ factor a b ⟧ ≈ a

-- Set of a ∙ ∃ n ∈ N
--
record aN {A : Group c c }  (N : NormalSubGroup A ) (x : Group.Carrier A  ) : Set c where 
    open Group A
    open NormalSubGroup N
    field 
        a n : Group.Carrier A 
        aN=x :  a ∙ ⟦ n ⟧ ≈ x

open import Tactic.MonoidSolver using (solve; solve-macro)

_/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
_/_ A N  = record {
    Carrier  = (x : Group.Carrier A) → aN N x
    ; _≈_      = _=n=_
    ; _∙_      = qadd 
    ; ε        = qid
    ; _⁻¹      = qinv
    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
       isEquivalence = record {refl = grefl   ; trans = ? ; sym = ? }
       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v {w} → qcong {x} {y} {u} {v} x=y u=v {w} }
       ; assoc = ? }
       ; identity =  idL , (λ q → ? )  }
       ; inverse   = ( (λ x → ? ) , (λ x → ? ))  
       ; ⁻¹-cong   = λ i=j → ?
      }
   } where
       open Group A
       open aN
       open NormalSubGroup N
       open IsGroupHomomorphism normal 
       open EqReasoning (Algebra.Group.setoid A)
       open Gutil A
       _=n=_ : (f g : (x : Group.Carrier A  )  → aN N x ) →  Set c
       f =n= g = {x : Group.Carrier A  } → ⟦ n (f x) ⟧  ≈ ⟦ n (g x) ⟧  
       qadd : (f g : (x : Group.Carrier A  )  → aN N x ) → (x : Group.Carrier A  )  → aN N x
       qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where
           q00 : ( x ⁻¹ ∙  a (f x) ∙ a (g x)  ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈ x
           q00 = begin 
              ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩
              x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧  ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩
              x ⁻¹ ∙ (a (f x) ∙ ((a (g x)  ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl ) (∙-cong (grefl ) (∙-cong comm (grefl ) ))  ⟩
              x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧  ∙ a (g x)) ∙ ⟦ n (g x) ⟧ ))  ≈⟨ solve monoid ⟩
              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ )  ≈⟨ ∙-cong (grefl ) (aN=x (g x)  ) ⟩
              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x   ≈⟨ ∙-cong (∙-cong (grefl ) (aN=x (f x))) (grefl )  ⟩
              (x ⁻¹ ∙ x ) ∙ x   ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl )  ⟩
              ε ∙ x  ≈⟨ solve monoid  ⟩
              x ∎ 
       qid : ( x : Carrier ) → aN N x
       qid x = record { a = x  ; n = ε  ; aN=x = qid1 } where
           qid1 : x ∙ ⟦ ε ⟧ ≈ x
           qid1 = begin
              x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩
              x ∙ ε  ≈⟨ solve monoid ⟩
              x ∎ 
       qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x
       qinv f x = record { a = x ∙ ⟦ n (f x) ⟧  ⁻¹  ; n = n (f x)  ; aN=x = qinv1  } where
             qinv1 : x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈ x
             qinv1 = begin
              x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
              x ∙ ⟦ (n (f x)) ⁻¹ ⟧  ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
              x ∙ ⟦ ((n (f x)) ⁻¹ )  ∙ n (f x) ⟧ ≈⟨ ? ⟩
              x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩
              x ∙ ε  ≈⟨ solve monoid ⟩
              x ∎ 
       qcong :  { x y u v : (x₁ : Carrier) → aN N x₁ } → (x=y : x =n= y) ( u=v : u =n= v ) →  qadd x u =n= qadd y v
       qcong {x} {y} {u} {v} x=y u=v {w} = begin
              ⟦ n (x w) ∙ n (u w) ⟧  ≈⟨ homo _ _ ⟩
              ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧  ≈⟨ ∙-cong x=y u=v ⟩
              ⟦ n (y w) ⟧ ∙ ⟦ n (v w) ⟧  ≈⟨ gsym  ( homo _ _) ⟩
              ⟦ n (y w) ∙ n (v w) ⟧  ∎ 
       idL : (f : (x  : Carrier )→  aN N x) → (qadd qid f ) =n= f 
       idL f = ?

-- K ⊂ ker(f)
K⊆ker : (G H : Group c c)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε   where
  open Group H
  open NormalSubGroup K

open import Function.Surjection
open import Function.Equality

module _ (G : Group c c) (K : NormalSubGroup G) where
    open Group G
    open aN
    open NormalSubGroup K
    open IsGroupHomomorphism normal 
    open EqReasoning (Algebra.Group.setoid G)
    open Gutil G

    φ : Group.Carrier G → Group.Carrier (G / K )
    φ g x = record { a = g  ; n = factor x g ; aN=x = is-factor x g  } 

    φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ 
    φ-homo = record {⁻¹-homo = λ g → ?  ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
       record { cong = ? } }}}

    φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
    φe = record { _⟨$⟩_ = φ ; cong = φ-cong  }  where
           φ-cong : {f g : Carrier } → f ≈ g  → {x : Carrier } →  ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ 
           φ-cong = ?

    -- inverse ofφ
    --  f = λ x → record { a = af ; n = fn ; aN=x = x ≈ af ∙ ⟦ fn ⟧  )   = (af)K  , fn ≡ factor x af , af ≡ a (f x)
    --        (inv-φ f)K ≡ (af)K
    --           φ (inv-φ f) x → f (h0 x)
    --           f x → φ (inv-φ f) (h1 x)
    --
    --  inv-φ f ≡ a (f ε)  -- not af ≡ a (f x)
    --  φ (inv-φ f)  returns ( λ x → record { a = a (f ε) ; n = factor x (a (f ε)) ; is-factor x (a (f ε)) )
    --          it should be ( λ x → record { a =      af ; n = factor x af        ; is-factor x af
    --          it should be ( λ x → record { a =      af ; n = fn                 ; is-factor x af
    --      ⟦ n (φ (inv-φ f) x)  ⟧ ≈ ⟦ n (f x) ⟧ ≈ ⟦ fn ⟧
    --      ⟦ factor x (a (f ε)) ⟧ ≈ ⟦ n (f x) ⟧ ≈ ⟦ fn ⟧ ≈ ⟦ factor x g ⟧ 
    --      g ∙ ⟦ factor y (a (f ε)) ⟧ ≈ x 
    --            factor x g
    --      g ∙ ⟦ factor y g ⟧ ≈ y 

    inv-φ : Group.Carrier (G / K ) → Group.Carrier G
    inv-φ f = a (f ε)

    _∋_ : (f : Group.Carrier (G / K)) (x : Carrier ) → Set c
    _∋_  f x = a (f x) ∙ ⟦ n (f x) ⟧ ≈ x  

    an02 : (f : Group.Carrier (G / K)) → {x : Carrier } → a (f x) ≈ x ∙ ⟦ n (f x) ⟧ ⁻¹
    an02 f {x} = begin
        a (f x ) ≈⟨ gsym  ( proj₂ identity _) ⟩
        a (f x ) ∙ ε  ≈⟨ ∙-cong (grefl ) (gsym  (proj₂ inverse _)) ⟩
        a (f x ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹)  ≈⟨ solve monoid ⟩
        (a (f x ) ∙  ⟦ n (f x) ⟧) ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ ∙-cong (aN=x (f x)) (grefl ) ⟩
        x ∙ ⟦ n (f x) ⟧ ⁻¹ ∎

    aNeqε : {f g : Group.Carrier (G / K)} →  (G / K)  < f ≈ g >
       →  {x : Carrier } → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε
    aNeqε {f} {g} f=g {x} = begin
           ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩
          ε ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩
          (a (f x)  ⁻¹ ∙  a (f x)) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧   ≈⟨ solve monoid ⟩
           a (f x)  ⁻¹ ∙ (a (f x)  ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ) ≈⟨ ? ⟩
           a (f x)  ⁻¹ ∙ a (g x) ≈⟨ ∙-cong (⁻¹-cong (an02 f) )  (an02 g) ⟩
           (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x  ∙ ⟦ n (g x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
           (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
           ( ⟦ n (f x) ⟧ ∙  x ⁻¹ ) ∙ (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
           ⟦ n (f x) ⟧ ∙  ( x ⁻¹  ∙ x ) ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ ? ⟩
           ⟦ n (f x) ⟧ ∙  ε ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ solve monoid ⟩
           ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ proj₂ inverse _ ⟩
           ε ∎  where
               an01 : a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ a (g x)
               an01 = is-factor (a (g x)) (a (f x))
               an03 : {f : Group.Carrier (G / K)} → {x : Carrier } → a (f x) ⁻¹ ≈ x ∙ ⟦ n (f x) ⟧ 
               an03 = ?

    f≈g→g⊆f : {f g : Group.Carrier (G / K)} → (G / K)  < f ≈ g > → {x : Carrier} → f ∋ x → g ∋ x
    f≈g→g⊆f {f} {g} f=g {x} fnx = begin
       a (g x) ∙ ⟦ n (g x) ⟧ ≈⟨ ∙-cong (gsym  (an01 (fgf ⁻¹ ∙ a (f x)))) (gsym  f=g) ⟩
       (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (⟦ factor (a (g x)) (a (f x)) ⟧ ⁻¹ ∙ a (f x)) ⟧  ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
       (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (ε ⁻¹ ∙ a (f x)) ⟧  ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
       (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧  ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
       (a (f x) ∙ fgf ⁻¹ ) ∙ ( ⟦ factor (a (g x)) (a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ) ≈⟨ solve monoid ⟩
       a (f x) ∙ (fgf ⁻¹  ∙  ⟦ factor (a (g x)) (a (f x)) ⟧) ∙ ⟦ n (f x) ⟧  ≈⟨ ? ⟩
       a (f x) ∙ ε ∙ ⟦ n (f x) ⟧  ≈⟨ ? ⟩
       a (f x) ∙ ⟦ n (f x) ⟧ ≈⟨ fnx ⟩
       x ∎  where
           fgf = ⟦ factor (a (g x)) (a (f x)) ⟧ 
           an01 : (y : Carrier) → y ∙ ⟦ factor (a (g x)) y ⟧ ≈ a (g x)
           an01 y = is-factor (a (g x)) y
           an03 : ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε
           an03 = ?

    f≈g→f=g : {f g : Group.Carrier (G / K)} →  (G / K)  < f ≈ g >
       →  ( {x : Carrier  } → f ∋  x → g ∋ x ) × ( {x : Carrier  } → g ∋  x → f ∋ x ) 
    f≈g→f=g {f} {g} f=g = f≈g→g⊆f {f} {g} f=g , f≈g→g⊆f {g} {f} (gsym  f=g) 

    cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
    cong-i = ?

    factor=nf : (f : (x : Carrier) → aN K x ) {y : Carrier} → ⟦ factor y ((a (f y)) ⁻¹ ) ⟧ ≈ ⟦ n (f y) ⟧
    factor=nf f {y} with f y
    ... | record { a = fa ; n = fn ; aN=x = faN=x } = begin
       ⟦ factor y z ⟧ ≈⟨ ? ⟩ 
       z ⁻¹ ∙ ( z ∙ ⟦ factor y z ⟧ ) ≈⟨ ? ⟩ 
       z ⁻¹ ∙ y  ≈⟨ ∙-cong (grefl ) (gsym  faN=x )  ⟩ 
       z ⁻¹ ∙ ( fa  ∙ ⟦ fn ⟧ )  ≈⟨ ? ⟩ 
       (z ⁻¹ ∙ fa ) ∙ ⟦ fn ⟧   ≈⟨ ? ⟩ 
       ε ∙ ⟦ fn ⟧   ≈⟨ solve monoid ⟩ 
       ⟦ fn ⟧ ∎ where
          z = fa ⁻¹

    φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → f ∋ x → f ∋ y →  ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧
    φ-factor f {x} {y} gx gy = begin
       ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
       (a (f x))  ⁻¹  ∙ x ≈⟨ ? ⟩ 
       (((a (f y))  ⁻¹  ∙ y ) ∙ ((a (f y))  ⁻¹  ∙ y ))  ⁻¹ ∙ ( (a (f x))  ⁻¹  ∙ x ) ≈⟨ ? ⟩ 
       ((a (f y))  ⁻¹  ∙ y ) ∙ (((a (f y))  ⁻¹  ∙ y )  ⁻¹ ∙ ( (a (f x))  ⁻¹  ∙ x )) ≈⟨ ? ⟩ 
       ((a (f y))  ⁻¹  ∙ y ) ∙ (⟦ n (f y) ⟧  ⁻¹ ∙ ⟦ n (f x) ⟧) ≈⟨ ? ⟩ 
       ((a (f y))  ⁻¹  ∙ y ) ∙ (⟦ n (f y) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧) ≈⟨ ? ⟩ 
       ((a (f y))  ⁻¹  ∙ y ) ∙ (⟦ n (f y) ⁻¹ ∙ n (f x) ⟧) ≈⟨ ? ⟩ 
       ((a (f y))  ⁻¹  ∙ y ) ∙ ε  ≈⟨ ? ⟩ 
       (a (f y))  ⁻¹  ∙ y ≈⟨ ? ⟩ 
       ⟦ n (f y) ⟧ ∎ where
          fa00 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x
          fa00 = gx
          fa01 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y
          fa01 = gy
          an01 : (y : Carrier) → y ∙ ⟦ factor (a (f x)) y ⟧ ≈ a (f x)
          an01 y = is-factor (a (f x)) y
          an04 : a (f y) ∙ ⟦ factor (a (f x)) (a (f y)) ⟧ ≈ a (f x)
          an04 = is-factor (a (f x)) (a (f y))
          an03 : ⟦ n (f y) ⁻¹  ∙ n (f x) ⟧ ≈ ε 
          an03 = begin
              ⟦ n (f y) ⁻¹  ∙ n (f x) ⟧ ≈⟨ ? ⟩ 
              ⟦ n (f y) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
              ⟦ n (f y) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
              ⟦ n (f y) ⟧ ⁻¹ ∙ (a (f x) ∙ x  ⁻¹ )  ≈⟨ ? ⟩ 
              ε  ∎

    is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧
    is-inverse f {y} = begin
       ⟦ n (φ (inv-φ f) y) ⟧  ≈⟨ grefl  ⟩
       ⟦ n (φ (a (f ε)) y) ⟧  ≈⟨ grefl  ⟩
       ⟦ factor y (a (f ε))  ⟧  ≈⟨ ? ⟩                 --  a (f ε) ∙ ⟦ factor y ( a (f ε)) ⟧ ≈ y 
       ⟦ factor y ((a (f y)) ⁻¹) ⟧  ≈⟨ factor=nf f ⟩   --  a (f y) ∙ ⟦ factor y ( a (f y)) ⟧ ≈ y 
       ⟦ n (f y) ⟧ ∎ where                             --  a (f y) ∙ ⟦ n (f y) ⟧ ≈ y 
           afn : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε
           afn = aN=x (f ε)
           afn' = (a (f y)) ⁻¹
           f00 : ⟦ n (f ε) ⟧ ≈ (a (f y)) ⁻¹
           f00 = begin
              ⟦ n (f ε) ⟧ ≈⟨ ? ⟩ 
              (a (f ε)) ⁻¹ ∙ a (f ε) ∙ ⟦ n (f ε) ⟧ ≈⟨ ? ⟩
              (a (f ε)) ⁻¹ ∙ ε ≈⟨ ? ⟩
              ⟦ n (f y) ⟧ ∙ y ⁻¹  ≈⟨ ? ⟩
              (a (f y)) ⁻¹ ∙ ( a (f y) ∙ ⟦ n (f y) ⟧ ∙ y ⁻¹ ) ≈⟨ ? ⟩
              (a (f y)) ⁻¹ ∎

    φ-surjective : Surjective φe 
    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } 
 
record FundamentalHomomorphism (G H : Group c c )
    (f : Group.Carrier G → Group.Carrier H ) 
    (homo : IsGroupHomomorphism (GR G) (GR H) f ) 
    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set c where
  open Group H
  field
    h : Group.Carrier (G / K ) → Group.Carrier H
    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → 
       ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )

FundamentalHomomorphismTheorm : (G H : Group c c)
    (f : Group.Carrier G → Group.Carrier H )
    (homo : IsGroupHomomorphism (GR G) (GR H) f )
    (K : NormalSubGroup G ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
FundamentalHomomorphismTheorm G H f homo K kf = record {
     h = h
   ; h-homo = h-homo
   ; is-solution = is-solution
   ; unique = unique
  } where
    open Group H
    h : Group.Carrier (G / K ) → Group.Carrier H
    h r = f ( aN.n (r (Group.ε G )  ))
    h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
    h03 x y = {!!}
    h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
    h-homo = record {
     isMonoidHomomorphism = record {
          isMagmaHomomorphism = record {
             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 
           ; homo = h03 }
        ; ε-homo = {!!} }
       ; ⁻¹-homo = {!!} }
    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
    is-solution x = begin
         f x ≈⟨ ? ⟩
         ? ≈⟨ ? ⟩
         f ( aN.n (( φ G K x ) (Group.ε G )  )) ≈⟨ ?  ⟩
         h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → 
       ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
    unique = ?