Mercurial > hg > Members > kono > Proof > galois
view src/Fundamental.agda @ 281:803f909fdd17
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 29 Jan 2023 08:19:19 +0900 |
parents | 523adaf1dcec |
children | b70cc2534d2f |
line wrap: on
line source
-- 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 open import Tactic.MonoidSolver using (solve; solve-macro) 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 _/_ : (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 = ? ; 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 y : Group.Carrier A } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ 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} {z} = begin ⟦ n (x w) ∙ n (u w) ⟧ ≈⟨ homo _ _ ⟩ ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧ ≈⟨ ∙-cong x=y u=v ⟩ ⟦ n (y z) ⟧ ∙ ⟦ n (v z) ⟧ ≈⟨ gsym (homo _ _ ) ⟩ ⟦ n (y z) ∙ n (v z) ⟧ ∎ 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 = ? } 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-φ : Group.Carrier (G / K ) → Group.Carrier G inv-φ f = ⟦ n (f ε) ⟧ ⁻¹ 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 = ? cong-i : {f g : Group.Carrier (G / K ) } → ({x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ ) → 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 } → ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧ φ-factor f {x} {y} = begin ⟦ n (f x) ⟧ ≈⟨ ? ⟩ ⟦ n (f x) ⟧ ∙ ε ≈⟨ ? ⟩ ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ⟦ n (f y) ⟧ ⁻¹ ) ≈⟨ cdr ( cdr an07 ) ⟩ ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ( ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ )) ≈⟨ ? ⟩ ⟦ n (f y) ⟧ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ ⟦ n (f y) ⟧ ∙ ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩ ⟦ n (f y) ⟧ ∙ ε ≈⟨ ? ⟩ ⟦ n (f y) ⟧ ∎ where fxy = ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f y) ⟧ fa11 : a (f (x ∙ y ⁻¹ )) ∙ ⟦ n (f (x ∙ y ⁻¹)) ⟧ ≈ x ∙ y ⁻¹ fa11 = aN=x ( f ( x ∙ y ⁻¹ )) fa21 : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε fa21 = aN=x ( f ε) fa22 : {x : Carrier } → a (f (x ⁻¹)) ∙ ⟦ n (f (x ⁻¹)) ⟧ ≈ x ⁻¹ fa22 {x} = aN=x ( f (x ⁻¹)) fa14 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x fa14 = aN=x ( f x) fa13 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y fa13 = aN=x ( f y) fa12 : aN K ( x ∙ y ⁻¹ ) fa12 = f (x ∙ y ⁻¹ ) 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)) an07 : {z w : Carrier} → z ≈ w ∙ ⟦ factor z w ⟧ an07 {z} {w} = gsym ( is-factor z w ) an10 : ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈ ε an10 = begin ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩ ( a (f x) ∙ x ⁻¹ ) ⁻¹ ∙ (a (f y) ∙ y ⁻¹) ≈⟨ ? ⟩ x ∙ a (f x) ⁻¹ ∙ a (f y) ∙ y ⁻¹ ≈⟨ ? ⟩ ε ∎ an08 : ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈ ε an08 = begin ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ ε ∎ an05 : {z : Carrier} → ⟦ n (f z) ⟧ ≈ ⟦ factor z (a (f z)) ⟧ an05 {z} = begin ⟦ n (f z) ⟧ ≈⟨ ? ⟩ ((a (f z) ⁻¹) ∙ a (f z)) ∙ ⟦ n (f z) ⟧ ≈⟨ ? ⟩ (a (f z) ⁻¹) ∙ ( a (f z) ∙ ⟦ n (f z) ⟧) ≈⟨ ∙-cong grefl (aN=x (f z)) ⟩ (a (f z) ⁻¹) ∙ z ≈⟨ ∙-cong grefl ( gsym ( is-factor z (a (f z)))) ⟩ (a (f z) ⁻¹) ∙ (a (f z) ∙ ⟦ factor z (a (f z)) ⟧ ) ≈⟨ ? ⟩ ⟦ factor z ( a ( f z)) ⟧ ∎ an06 : {z : Carrier} → ⟦ factor z z ⟧ ≈ ε an06 {z} = begin ⟦ factor z z ⟧ ≈⟨ ? ⟩ (z ⁻¹ ∙ z ) ∙ ⟦ factor z z ⟧ ≈⟨ ? ⟩ z ⁻¹ ∙ ( z ∙ ⟦ factor z z ⟧ ) ≈⟨ ∙-cong grefl (is-factor z z) ⟩ z ⁻¹ ∙ z ≈⟨ ? ⟩ ε ∎ an03 : ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈ ε an03 = begin ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈⟨ ? ⟩ ⟦ factor y (a (f y)) ⟧ ⁻¹ ∙ ⟦ factor x (a (f x)) ⟧ ≈⟨ ? ⟩ ⟦ factor y (a (f y)) ⟧ ⁻¹ ∙ ⟦ factor x ( x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⟧ ≈⟨ ? ⟩ ⟦ n (f (y ⁻¹ ∙ x)) ⟧ ≈⟨ ? ⟩ ⟦ factor (y ⁻¹ ∙ x) (a (f (y ⁻¹ ∙ x))) ⟧ ≈⟨ ? ⟩ ⟦ n (f ⟦ ε ⟧ ) ⟧ ≈⟨ ? ⟩ ⟦ ε ⟧ ≈⟨ ? ⟩ -- ⟦ n (f x) ⟧ ≡ ⟦ n (g x) ⟧ → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε ε ∎ is-inverse : (f : (x : Carrier) → aN K x ) → {x y : Carrier} → ⟦ n (φ (inv-φ f) x) ⟧ ≈ ⟦ n (f y) ⟧ is-inverse f {x} {y} = begin ⟦ n (φ (inv-φ f) x) ⟧ ≈⟨ grefl ⟩ ⟦ n (φ (⟦ n (f ε) ⟧ ⁻¹) x) ⟧ ≈⟨ grefl ⟩ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ ε ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ (x ∙ x ⁻¹ ) ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ x ∙ ( x ⁻¹ ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ) ≈⟨ ? ⟩ x ∙ ⟦ n (f ε) ⟧ ⁻¹ ≈⟨ ? ⟩ y ∙ ⟦ n (f y) ⟧ ⁻¹ ≈⟨ ? ⟩ ⟦ n (f y) ⟧ ∎ where 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 = ? } 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 = ?