--- a/src/FundamentalHomorphism.agda	Sun Jan 29 21:05:55 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jan 29 21:59:08 2023 +0900
@@ -99,14 +99,14 @@
     ; _≈_      = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧
     ; _∙_      = qadd
     ; ε        = qid 
-    ; _⁻¹      = ?
+    ; _⁻¹      = λ f → record { n = n f ⁻¹ ; is-an = λ x → record { a = an.a (is-an f x) ∙  ⟦ n f ⟧  ∙ ⟦ n f ⟧  ; aN=x = qinv0 f x } } 
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
        isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym }
-       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? }
-       ; assoc = ? }
-       ; identity =  ? , (λ q → ? )  }
-       ; inverse   = ( (λ x → ? ) , (λ x → ? ))
-       ; ⁻¹-cong   = λ i=j → ?
+       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gtrans (homo _ _) ( gtrans (∙-cong x=y u=v)  (gsym (homo _ _) )) }
+       ; assoc = qassoc }
+       ; identity = (λ q →   ⟦⟧-cong (proj₁ identity _) ) , (λ q → ⟦⟧-cong (proj₂ identity _) )  }
+       ; inverse   =  (λ x → ⟦⟧-cong (proj₁ inverse _  )) , (λ x → ⟦⟧-cong (proj₂ inverse _ ) )
+       ; ⁻¹-cong   = λ {x} {y} → i-conv  {x} {y}
       }
    } where
        open Group A
@@ -120,16 +120,21 @@
        qadd f g = record { n = n f ∙ n g  ; is-an = λ x → record { a = x ⁻¹ ∙ ( a (is-an f x) ∙ a (is-an g x))  ; aN=x = qadd0 }  } where
            qadd0 : {x : Carrier} →   x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈ x
            qadd0 {x} = begin
-              x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ ? ⟩
+              x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ solve monoid ⟩
               x ⁻¹ ∙  (a (is-an f x) ∙ a (is-an g x) ∙ ⟦ n f ∙ n g ⟧) ≈⟨ ? ⟩
-              x ⁻¹ ∙  (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧  ∙ ⟦ n g ⟧ )) ≈⟨ ? ⟩
+              x ⁻¹ ∙  (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧  ∙ ⟦ n g ⟧ )) ≈⟨ solve monoid ⟩
               x ⁻¹ ∙  (a (is-an f x) ∙ ( a (is-an g x) ∙  ⟦ n f ⟧)  ∙ ⟦ n g ⟧)  ≈⟨ ? ⟩
               x ⁻¹ ∙  (a (is-an f x) ∙ ( ⟦ n f ⟧ ∙ a (is-an g x) )  ∙ ⟦ n g ⟧)  ≈⟨ ? ⟩
               x ⁻¹ ∙  ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x)   ∙ ⟦ n g ⟧))  ≈⟨ ? ⟩
-              x ⁻¹ ∙  (x ∙ x)  ≈⟨ ? ⟩
+              x ⁻¹ ∙  (x ∙ x)  ≈⟨ solve monoid ⟩
               (x ⁻¹ ∙  x ) ∙ x  ≈⟨ ? ⟩
-              ε ∙ x  ≈⟨ ? ⟩
+              ε ∙ x  ≈⟨ solve monoid ⟩
               x ∎
+       qinv0 : (f : aN N) → (x : Carrier ) → (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈ x
+       qinv0 f x = begin
+          (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈⟨ ? ⟩
+           a (is-an f x) ∙ ⟦ n f ⟧  ≈⟨ an.aN=x (is-an f x) ⟩
+          x ∎
        qid :  aN N
        qid = record { n = ε ; is-an = λ x → record { a = x ; aN=x = qid1 } } where
            qid1 : {x : Carrier } →  x ∙ ⟦ ε ⟧ ≈ x
@@ -137,6 +142,14 @@
              x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong grefl ε-homo ⟩
              x ∙ ε  ≈⟨ proj₂ identity _ ⟩
              x ∎
+       qassoc : (f g h : aN N) → ⟦ n ( qadd (qadd f g) h) ⟧ ≈  ⟦ n( qadd f (qadd g h)) ⟧
+       qassoc f g h = ⟦⟧-cong (assoc  _ _ _ )
+       i-conv : {x y : aN N} → ⟦ n x ⟧ ≈ ⟦ n y ⟧ →  ⟦ n x ⁻¹ ⟧ ≈ ⟦ n y ⁻¹ ⟧ 
+       i-conv {x} {y} nx=ny = begin
+          ⟦ n x ⁻¹ ⟧ ≈⟨ ⁻¹-homo _ ⟩
+          ⟦ n x ⟧ ⁻¹  ≈⟨ ⁻¹-cong nx=ny ⟩
+          ⟦ n y ⟧ ⁻¹  ≈⟨ gsym ( ⁻¹-homo _)  ⟩
+          ⟦ n y ⁻¹ ⟧  ∎
 
 
 -- K ⊂ ker(f)