--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/fundamental.agda	Sun May 29 10:09:02 2022 +0900
@@ -0,0 +1,82 @@
+-- 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 
+