module group-0001 where

open import MLTT.Spartan hiding (_∙_) renaming (_⁻¹ to sym)

open import group-0000
open Group {{...}}

假設元素 h ∈ G 是另一個滿足單位元素條件的元素，那 h = e。

事實上，很酷的事情是甚至不用完全滿足單位元素條件，就如下面的證明所演示的

proposition-1 : {G : 𝓤 ̇} {{_ : Group G}} {h : G} → left-neutral h _∙_ → h ＝ e
proposition-1 {G}{_} {h} h-is-identity =
  h     ＝⟨ sym (neu-r h) ⟩
  h ∙ e ＝⟨ h-is-identity e ⟩
  e ∎

這個命題的重點是單位元素是唯一的，所以英文的話你可以用「the」修飾。

sym 把等式翻面：A ＝ B 變成 B ＝ A k

module group-0002 where

open import MLTT.Spartan hiding (_∙_) renaming (_⁻¹ to sym)

open import group-0000
open Group {{...}}

如果 h₁ and h₂ 的反元素都是 g，那 h₁ = h₂。或者我們會說反元素是唯一的，跟上面的命題的意義類似。

proposition-2 : {G : 𝓤 ̇} {{_ : Group G}} {g h1 h2 : G} → (g ∙ h1 ＝ e) → (g ∙ h2 ＝ e) → h1 ＝ h2
proposition-2 {G}{_} {g}{h1}{h2} fact1 fact2 =
  h1              ＝⟨ sym (neu-l h1) ⟩
  e ∙ h1          ＝⟨ ap (_∙ h1) (sym (cancel .pr₁)) ⟩
  g ⁻¹ ∙ g ∙ h1   ＝⟨ ∙-assoc (g ⁻¹) g h1 ⟩
  g ⁻¹ ∙ (g ∙ h1) ＝⟨ ap (g ⁻¹ ∙_) fact1 ⟩
  g ⁻¹ ∙ e        ＝⟨ ap ((g ⁻¹) ∙_) (sym fact2) ⟩
  g ⁻¹ ∙ (g ∙ h2) ＝⟨ sym (∙-assoc (g ⁻¹) g h2) ⟩
  g ⁻¹ ∙ g ∙ h2   ＝⟨ ap (_∙ h2) (cancel .pr₁) ⟩
  e ∙ h2          ＝⟨ neu-l h2 ⟩
  h2 ∎

ap 把等式裡的 expression 中沒有變化的部分抽出來用的，這樣才能操作其餘要改變的部分

module group-0003 where

open import MLTT.Spartan hiding (_∙_) renaming (_⁻¹ to sym)

open import group-0000
open Group {{...}}

這個命題在說每個元素都可以取消，這是一個非常好用的事實，而且完全不必感到陌生，我等一下再解釋這點。我們先來看它的具體描述

1. 如果 g • a = h • a，則 g = h
2. 如果 a • g = a • h，則 g = h

proposition-3 : {G : 𝓤 ̇} {{_ : Group G}} {g h a : G} → (g ∙ a ＝ h ∙ a → g ＝ h) × (a ∙ g ＝ a ∙ h → g ＝ h)
proposition-3 {G}{_} {g}{h}{a} = I , II
  where
  I : g ∙ a ＝ h ∙ a → g ＝ h
  I fact =
    g              ＝⟨ sym (neu-r g) ⟩
    g ∙ e          ＝⟨ ap (g ∙_) (sym (cancel .pr₂)) ⟩
    g ∙ (a ∙ a ⁻¹) ＝⟨ sym (∙-assoc g a (a ⁻¹)) ⟩
    g ∙ a ∙ a ⁻¹   ＝⟨ ap (_∙ a ⁻¹) fact ⟩
    h ∙ a ∙ a ⁻¹   ＝⟨ ∙-assoc h a (a ⁻¹) ⟩
    h ∙ (a ∙ a ⁻¹) ＝⟨ ap (h ∙_) (cancel .pr₂) ⟩
    h ∙ e          ＝⟨ neu-r h ⟩
    h ∎

  II : a ∙ g ＝ a ∙ h → g ＝ h
  II fact =
    g              ＝⟨ sym (neu-l g) ⟩
    e ∙ g          ＝⟨ ap (_∙ g) (sym (cancel .pr₁)) ⟩
    a ⁻¹ ∙ a ∙ g   ＝⟨ ∙-assoc (a ⁻¹) a g ⟩
    a ⁻¹ ∙ (a ∙ g) ＝⟨ ap (a ⁻¹ ∙_) fact ⟩
    a ⁻¹ ∙ (a ∙ h) ＝⟨ sym (∙-assoc (a ⁻¹) a h) ⟩
    a ⁻¹ ∙ a ∙ h   ＝⟨ ap (_∙ h) (cancel .pr₁) ⟩
    e ∙ h          ＝⟨ neu-l h ⟩
    h ∎

為什麼不必對這個命題感到陌生呢？因為這其實是我們日常也很容易遇到的算術事實：如果 2x = 2y 那 x = y。

module group-0005 where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)

open import group-0000
open Group {{...}}
open import group-0003
open import group-0004

Group homomorphism 保留單位元素，也就是說 φ(e_G) = e_H。

注意到雖然我們在數學式裡面用下標 _G、_H 區分，但在 Agda 裡面它自己就知道這件事，所以不用特別寫出

proposition-4 : {G H : 𝓤 ̇} {{∈G : Group G}} {{∈H : Group H}}
  → (φ : G → H)
  → IsGroupHomomorphism G H φ
  → φ e ＝ e
proposition-4 φ is-hom = II
  where

證明 φ(e_G) • φ(e_G) = e_H • φ(e_G)

  I : (φ e) ∙ (φ e) ＝ e ∙ (φ e)
  I = (φ e) ∙ (φ e) ＝⟨ sym (is-hom e e) ⟩
      φ (e ∙ e)     ＝⟨ ap φ (neu-l e)  ⟩
      φ e           ＝⟨ sym (neu-l (φ e)) ⟩
      e ∙ φ e ∎

那我們就可以用前面證明過的 [Proposition 3] 任何元素都能取消 得出結論

  II : (φ e) ＝ e
  II = (proposition-3 .pr₁) I

module group-0006 where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)

open import group-0000
open Group {{...}}
open import group-0003
open import group-0004
open import group-0005

Group homomorphism 保留反元素，也就是說 φ(g⁻¹) = φ(g)⁻¹ 對所有 g ∈ G 成立。

proposition-5 : {G H : 𝓤 ̇} {{∈G : Group G}} {{∈H : Group H}}
  → (φ : G → H)
  → IsGroupHomomorphism G H φ
  → (g : G)
  → φ (g ⁻¹) ＝ (φ g) ⁻¹
proposition-5 φ is-hom g = (proposition-3 .pr₁) III
  where

這裡馬上就用到剛剛證明的保留 identity 性質

  I : φ (g ⁻¹) ∙ φ g ＝ e
  I = φ (g ⁻¹) ∙ φ g ＝⟨ sym (is-hom (g ⁻¹) g) ⟩
      φ (g ⁻¹ ∙ g)   ＝⟨ ap φ (cancel .pr₁) ⟩
      φ e            ＝⟨ proposition-4 φ is-hom ⟩
      e ∎

  II : e ＝ (φ g) ⁻¹ ∙ (φ g)
  II = sym (cancel .pr₁)

  III : φ (g ⁻¹) ∙ φ g ＝ (φ g) ⁻¹ ∙ (φ g)
  III = I then II

module group-0008 where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)
open import UF.Subsingletons
open import UF.Subsingletons-Properties

open import group-0000
open Group {{...}}
open import group-0004
open import group-0007

這個命題是說，對所有群都有一個子群是 trivial group。

要證明之前，我們需要看一下什麼是 trivial group，基本上它就是只有一個估拎拎的 e 元素的集合，那因為只有一個元素，能定義的二元運算子也就只有一個，根據這些我們可以定義 trivial group（𝟙 是一個只有單一元素 ⋆ 的型別）

trivial-group : Group (𝟙 {𝓤})
trivial-group .size = props-are-sets 𝟙-is-prop
trivial-group ._∙_ = λ _ _ → ⋆
trivial-group .∙-assoc = λ _ _ _ → refl
trivial-group .e = ⋆
trivial-group .neu-l = λ _ → refl
trivial-group .neu-r = λ _ → refl
trivial-group ._⁻¹ = λ _ → ⋆
trivial-group .cancel = refl , refl

現在我們可以回到證明，因為 IsSubgroup 是一個 Sigma 類型，所以我們需要提出一個 map ι，然後證明這個 map 是 inclusion 而且是 group homomorphism。

proposition-6 : {G : 𝓤 ̇} {{∈G : Group G}} {{∈𝟙 : Group 𝟙}}
  → IsSubgroup 𝟙 G
proposition-6 {𝓤} {G} = ι , lc , is-hom
  where

這個 map 在數學上常被稱為 canonical map，用來指示「很明顯」會選這個的意思，這在不同數學領域都會有類似的 canonical 的用法，雖然那個「明顯」可能很不一樣。

  ι : 𝟙 → G
  ι ⋆ = e

它的 inclusion 特性很明顯，甚至都不用到 p，因為只有一個元素

  lc : left-cancellable ι
  lc p = refl

最後要滿足 group homomorphism，下面利用 e 攤開出我們需要的表達式

  is-hom : IsGroupHomomorphism 𝟙 G ι
  is-hom ⋆ ⋆ =
    ι (⋆ ∙ ⋆) ＝⟨by-definition⟩
    e         ＝⟨ sym (neu-l e) ⟩
    e ∙ e     ＝⟨by-definition⟩
    (ι ⋆) ∙ (ι ⋆) ∎

module group-0009 where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)
open import UF.Sets

open import group-0000
open Group {{...}}
open import group-0002
open import group-0004
open import group-0007

這個命題說 H 是 G 的 subgroup 等價於說

H 是 G 的非空子集合，且

a • b⁻¹ ∈ H

下面只證明這個條件可以推出

1. H 是一個群
2. H 是 G 的子群

因為反過來非常明顯：一個群本身當然是封閉的。

跟之前一樣，子集合寫成 inclusion 函數

proposition-7 : {G H : 𝓤 ̇} {{∈G : Group G}}
  → (i : H → G)
  → left-cancellable i
  → is-set H

怎麼表達 H 不是空集呢？只要說存在一個元素就好

  → (h : H)

∀ (a b : G) → Σ y ꞉ H , a ∙ b ⁻¹ ＝ i y 這整個型別要這樣解讀「對所有 a, b ∈ G，存在 y ∈ H 使 a • b⁻¹ = i(y)」。這裡是目前第一次用到 Σ，也就是說 Σ 當命題時，其實就是用來表達「存在某某某滿足什麼什麼條件」的

  → (∀ (a b : G) → Σ y ꞉ H , a ∙ b ⁻¹ ＝ i y)
  → Σ is-grp ꞉ Group H , IsSubgroup {𝓤} H G {{is-grp}}
proposition-7 {𝓤}{G}{H} {{∈G}} i inclusion H-is-set h cond = H-is-group , i , inclusion , is-hom
  where

接下來的證明很大的複雜性都在 H 是群這點上，尤其是因為把 cond 的類型定義成存在 y ∈ H 映射到 a ∙ b ⁻¹ 這點上，會讓接下來很多簡單的東西都藏在定義後面。其實如果可以，技巧上最好是以 G 為類型，滿足某種條件的元素，而不是真的用另一個型別 H，事情會簡單很多

這裡先定義一些工具，像 I 就在說 H 一定有一個元素可以當單位元，也就是採用前面 inhabited 那個 h : H 然後取 i h ∙ i h ⁻¹ 為單位元（這邊就是技術細節導致的問題，i h ∙ i h ⁻¹ 的類型是 G 不能直接用，還需要取一次 pr₁ 才是 H 的 term）

  I : Σ y ꞉ H , i h ∙ i h ⁻¹ ＝ i y
  I = cond (i h) (i h)
  eH : H
  eH = I .pr₁
  prop-eH : i h ∙ i h ⁻¹ ＝ i eH
  prop-eH = I .pr₂
  eH-is-identity : i eH ＝ e
  eH-is-identity = (sym prop-eH) then (cancel .pr₂)

  II : (a b : H) → Σ y ꞉ H , i a ∙ i b ⁻¹ ⁻¹ ＝ i y
  II a b = cond (i a) (i b ⁻¹)

  III : (a : H) → Σ y ꞉ H , i eH ∙ i a ⁻¹ ＝ i y
  III a = cond (i eH) (i a)

  inv-inv : (a : G) → a ⁻¹ ⁻¹ ＝ a
  inv-inv a = proposition-2 F S
    where
    F : a ⁻¹ ∙ a ⁻¹ ⁻¹ ＝ e
    F = cancel .pr₂
    S : a ⁻¹ ∙ a ＝ e
    S = cancel .pr₁

H 可以用上面定義的工具滿足群的條件

  H-is-group : Group H
  H-is-group .size = H-is-set
  H-is-group ._∙_ a b = II a b .pr₁
  H-is-group .∙-assoc x y z = inclusion VII
    where
    IV : Σ xy ꞉ H , i x ∙ i y ⁻¹ ⁻¹ ＝ i xy
    IV = II x y
    xy = IV .pr₁
    Hxy : i x ∙ i y ⁻¹ ⁻¹ ＝ i xy
    Hxy = IV .pr₂
    V : Σ yz ꞉ H , i y ∙ i z ⁻¹ ⁻¹ ＝ i yz
    V = II y z
    yz = V .pr₁
    Hyz : i y ∙ i z ⁻¹ ⁻¹ ＝ i yz
    Hyz = V .pr₂
    left = II xy z .pr₁
    right = II x yz .pr₁
    help1 = II xy z .pr₂
    help2 = II x yz .pr₂
    mid : i xy ∙ i z ⁻¹ ⁻¹ ＝ i x ∙ i yz ⁻¹ ⁻¹
    mid =
      i xy ∙ i z ⁻¹ ⁻¹        ＝⟨ ap (i xy ∙_) (inv-inv (i z)) ⟩
      i xy ∙ i z              ＝⟨ ap (_∙ i z) (sym Hxy) ⟩
      i x ∙ i y ⁻¹ ⁻¹ ∙ i z   ＝⟨ ap (λ y → i x ∙ y ∙ i z) (inv-inv (i y)) ⟩
      i x ∙ i y ∙ i z         ＝⟨ ap (i x ∙ i y ∙_) (sym (inv-inv (i z))) ⟩
      i x ∙ i y ∙ i z ⁻¹ ⁻¹   ＝⟨ ∙-assoc (i x) (i y) (i z ⁻¹ ⁻¹) ⟩
      i x ∙ (i y ∙ i z ⁻¹ ⁻¹) ＝⟨ ap (i x ∙_) Hyz ⟩
      i x ∙ i yz              ＝⟨ ap (i x ∙_) (sym (inv-inv (i yz))) ⟩
      i x ∙ i yz ⁻¹ ⁻¹ ∎
    VII : i left ＝ i right
    VII = (sym help1) then mid then help2
  H-is-group .e = eH
  H-is-group .neu-l x = inclusion VI
    where
    IV : Σ y ꞉ H , i eH ∙ i x ⁻¹ ⁻¹ ＝ i y
    IV = II eH x
    y = IV .pr₁
    V : i eH ∙ i x ⁻¹ ⁻¹ ＝ i y
    V = IV .pr₂
    VI : i y ＝ i x
    VI =
      i y              ＝⟨ sym V ⟩
      i eH ∙ i x ⁻¹ ⁻¹ ＝⟨ ap (_∙ i x ⁻¹ ⁻¹) eH-is-identity ⟩
      e ∙ i x ⁻¹ ⁻¹    ＝⟨ neu-l (i x ⁻¹ ⁻¹) ⟩
      i x ⁻¹ ⁻¹        ＝⟨ inv-inv (i x) ⟩
      i x ∎
  H-is-group .neu-r x = inclusion VI
    where
    IV : Σ y ꞉ H , i x ∙ i eH ⁻¹ ⁻¹ ＝ i y
    IV = II x eH
    y = IV .pr₁
    V : i x ∙ i eH ⁻¹ ⁻¹ ＝ i y
    V = IV .pr₂
    VI : i y ＝ i x
    VI =
      i y              ＝⟨ sym V ⟩
      i x ∙ i eH ⁻¹ ⁻¹ ＝⟨ ap (i x ∙_) (inv-inv (i eH)) ⟩
      i x ∙ i eH       ＝⟨ ap (i x ∙_) eH-is-identity ⟩
      i x ∙ e          ＝⟨ neu-r (i x) ⟩
      i x ∎
  H-is-group ._⁻¹ x = III x .pr₁
  H-is-group .cancel {x} = left , right
    where
    x' = III x .pr₁
    Hx' : i eH ∙ i x ⁻¹ ＝ i x'
    Hx' = III x .pr₂

    l = II x' x .pr₁
    Hl : i x' ∙ i x ⁻¹ ⁻¹ ＝ i l
    Hl = II x' x .pr₂
    step-left : i x' ∙ i x ⁻¹ ⁻¹ ＝ i eH
    step-left =
      i x' ∙ i x ⁻¹ ⁻¹            ＝⟨ ap (_∙ i x ⁻¹ ⁻¹) (sym Hx') ⟩
      i eH ∙ i x ⁻¹ ∙ i x ⁻¹ ⁻¹   ＝⟨ ∙-assoc (i eH) (i x ⁻¹) (i x ⁻¹ ⁻¹) ⟩
      i eH ∙ (i x ⁻¹ ∙ i x ⁻¹ ⁻¹) ＝⟨ ap (i eH ∙_) (cancel .pr₂) ⟩
      i eH ∙ e                    ＝⟨ neu-r (i eH) ⟩
      i eH ∎

    r = II x x' .pr₁
    Hr : i x ∙ i x' ⁻¹ ⁻¹ ＝ i r
    Hr = II x x' .pr₂
    step-right : i x ∙ i x' ⁻¹ ⁻¹ ＝ i eH
    step-right =
      i x ∙ i x' ⁻¹ ⁻¹      ＝⟨ ap (i x ∙_) (inv-inv (i x')) ⟩
      i x ∙ i x'            ＝⟨ ap (i x ∙_) (sym Hx') ⟩
      i x ∙ (i eH ∙ i x ⁻¹) ＝⟨ ap (i x ∙_) (ap (_∙ i x ⁻¹) eH-is-identity) ⟩
      i x ∙ (e ∙ i x ⁻¹)    ＝⟨ ap (i x ∙_) (neu-l (i x ⁻¹)) ⟩
      i x ∙ i x ⁻¹          ＝⟨ cancel .pr₂ ⟩
      e                     ＝⟨ sym eH-is-identity ⟩
      i eH ∎

    left : (l ＝ eH)
    left = inclusion ((sym Hl) then step-left)
    right : (II x x' .pr₁ ＝ eH)
    right = inclusion ((sym Hr) then step-right)

證明的最後一個部分是推論出這樣的 inclusion map 一定是 group homomorphism

  is-hom : IsGroupHomomorphism H G {{H-is-group}} i
  is-hom x y =
    i (II x y .pr₁) ＝⟨ sym (II x y .pr₂) ⟩
    i x ∙ i y ⁻¹ ⁻¹ ＝⟨ ap (i x ∙_) (inv-inv (i y)) ⟩
    i x ∙ i y ∎

這裡來嘗試第二種編碼方式證明同樣的命題

1. 用 ∈H : G → 𝓤 ̇ 編碼了屬於 H 集合這個前提
2. 規定 ∈H 是 proposition（沒錯，在 HoTT 裡你同樣能問一個類型是不是一個命題）
3. inhabited h : G 且 h ∈H 表示了 H 不是空集合

下面會反覆使用的技術是 to-Σ-＝，這樣就會證明一次 G 中元素在屬於 H 時的等式，隨後要處理一個 transport 問題，但因為上面第二個條件（∈H 是 proposition），使得這個證明是完全由 Agda 可以自動合成的

open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Base

proposition-7' : {G : 𝓤 ̇ } {{∈G : Group G}}
  → (_∈H : G → 𝓤 ̇ )
  → (∀ (a : G) → is-prop (a ∈H))
  → (∀ (a b : G) → a ∙ b ⁻¹ ∈H)
  → (h : G)
  → h ∈H
  → Σ is-grp ꞉ Group (Σ x ꞉ G , x ∈H) , IsSubgroup {𝓤} (Σ x ꞉ G , x ∈H) G {{is-grp}}
proposition-7' {𝓤}{G}{{∈G}} _∈H ∈H-is-prop cond h h∈H = H-is-grp , is-subgroup
  where
  inv-inv : (a : G) → a ⁻¹ ⁻¹ ＝ a
  inv-inv a = proposition-2 F S
    where
    F : a ⁻¹ ∙ a ⁻¹ ⁻¹ ＝ e
    F = cancel .pr₂
    S : a ⁻¹ ∙ a ＝ e
    S = cancel .pr₁

  H-is-grp : Group (Σ x ꞉ G , x ∈H)
  H-is-grp .size = subsets-of-sets-are-sets G _∈H (Group.size ∈G) λ {x = x₁} → ∈H-is-prop x₁
  H-is-grp ._∙_ (a , a∈H) (b , b∈H) = a ∙ b ⁻¹ ⁻¹ , cond a (b ⁻¹)
  H-is-grp .∙-assoc (a , a∈H) (b , b∈H) (c , c∈H) = to-Σ-＝ (elem , ∈H-is-prop (pr₁ ((H-is-grp Group.∙ (a , a∈H)) ((H-is-grp Group.∙ (b , b∈H)) (c , c∈H)))) (transport _∈H elem (pr₂ ((H-is-grp Group.∙ (H-is-grp Group.∙ (a , a∈H)) (b , b∈H)) (c , c∈H)))) (pr₂ ((H-is-grp Group.∙ (a , a∈H)) ((H-is-grp Group.∙ (b , b∈H)) (c , c∈H)))))
    where
    elem : (a ∙ b ⁻¹ ⁻¹) ∙ c ⁻¹ ⁻¹ ＝ a ∙ (b ∙ c ⁻¹ ⁻¹) ⁻¹ ⁻¹
    elem =
      (a ∙ b ⁻¹ ⁻¹) ∙ c ⁻¹ ⁻¹ ＝⟨ ∙-assoc a (b ⁻¹ ⁻¹) (c ⁻¹ ⁻¹) ⟩
      a ∙ (b ⁻¹ ⁻¹ ∙ c ⁻¹ ⁻¹) ＝⟨ ap (λ b → a ∙ (b ∙ c ⁻¹ ⁻¹)) (inv-inv b) ⟩
      a ∙ (b ∙ c ⁻¹ ⁻¹)       ＝⟨ ap (a ∙_) (sym (inv-inv (b ∙ c ⁻¹ ⁻¹))) ⟩
      a ∙ (b ∙ c ⁻¹ ⁻¹) ⁻¹ ⁻¹ ∎
  H-is-grp .e = (h ∙ h ⁻¹) , cond h h
  H-is-grp .neu-l (x , x∈H) = to-Σ-＝ (elem , ∈H-is-prop x (transport _∈H elem (pr₂ ((H-is-grp Group.∙ H-is-grp .Group.e) (x , x∈H)))) x∈H)
    where
    elem : (h ∙ h ⁻¹) ∙ x ⁻¹ ⁻¹ ＝ x
    elem =
      (h ∙ h ⁻¹) ∙ x ⁻¹ ⁻¹ ＝⟨ ap (_∙ (x ⁻¹) ⁻¹) (∈G .cancel .pr₂) ⟩
      e ∙ x ⁻¹ ⁻¹          ＝⟨ neu-l (x ⁻¹ ⁻¹) ⟩
      x ⁻¹ ⁻¹              ＝⟨ inv-inv x ⟩
      x ∎
  H-is-grp .neu-r (x , x∈H) = to-Σ-＝ (elem , ∈H-is-prop x (transport _∈H elem (pr₂ ((H-is-grp Group.∙ (x , x∈H)) (H-is-grp .Group.e)))) x∈H)
    where
    elem : x ∙ (h ∙ h ⁻¹) ⁻¹ ⁻¹ ＝ x
    elem =
      x ∙ (h ∙ h ⁻¹) ⁻¹ ⁻¹ ＝⟨ ap (x ∙_) (inv-inv (h ∙ h ⁻¹)) ⟩
      x ∙ (h ∙ h ⁻¹)       ＝⟨ ap (x ∙_) (∈G .cancel .pr₂) ⟩
      x ∙ e                ＝⟨ neu-r x ⟩
      x ∎
  H-is-grp ._⁻¹ (x , x∈H) = (h ∙ h ⁻¹) ∙ x ⁻¹ , cond (h ∙ h ⁻¹) x
  H-is-grp .cancel {x} =
    to-Σ-＝ (cL , ∈H-is-prop (pr₁ (Group.e H-is-grp))
      (transport _∈H cL
       (pr₂ ((H-is-grp Group.∙ (H-is-grp Group.⁻¹) x) x)))
      (pr₂ (Group.e H-is-grp))) ,
    to-Σ-＝ (cR , ∈H-is-prop (pr₁ (Group.e H-is-grp))
      (transport _∈H cR
       (pr₂ ((H-is-grp Group.∙ x) ((H-is-grp Group.⁻¹) x))))
      (pr₂ (Group.e H-is-grp)))
    where
    k = x .pr₁
    cL : (h ∙ h ⁻¹ ∙ k ⁻¹) ∙ k ⁻¹ ⁻¹ ＝ h ∙ h ⁻¹
    cL =
      (h ∙ h ⁻¹ ∙ k ⁻¹) ∙ k ⁻¹ ⁻¹ ＝⟨ ap (h ∙ h ⁻¹ ∙ k ⁻¹ ∙_) (inv-inv k) ⟩
      (h ∙ h ⁻¹ ∙ k ⁻¹) ∙ k       ＝⟨ ap (_∙ k) (∙-assoc h (h ⁻¹) (k ⁻¹)) ⟩
      h ∙ (h ⁻¹ ∙ k ⁻¹) ∙ k       ＝⟨ ∙-assoc h (h ⁻¹ ∙ k ⁻¹) k ⟩
      h ∙ ((h ⁻¹ ∙ k ⁻¹) ∙ k)     ＝⟨ ap (h ∙_) (∙-assoc (h ⁻¹) (k ⁻¹) k) ⟩
      h ∙ (h ⁻¹ ∙ (k ⁻¹ ∙ k))     ＝⟨ ap (h ∙_) (ap (h ⁻¹ ∙_) (cancel .pr₁)) ⟩
      h ∙ (h ⁻¹ ∙ e)              ＝⟨ ap (h ∙_) (neu-r (h ⁻¹)) ⟩
      h ∙ h ⁻¹ ∎
    cR : k ∙ (h ∙ h ⁻¹ ∙ k ⁻¹) ⁻¹ ⁻¹ ＝ h ∙ h ⁻¹
    cR =
      k ∙ (h ∙ h ⁻¹ ∙ k ⁻¹) ⁻¹ ⁻¹ ＝⟨ ap (k ∙_) (inv-inv (h ∙ h ⁻¹ ∙ k ⁻¹)) ⟩
      k ∙ (h ∙ h ⁻¹ ∙ k ⁻¹)       ＝⟨ ap (k ∙_) (ap (_∙ k ⁻¹) (cancel .pr₂)) ⟩
      k ∙ (e ∙ k ⁻¹)              ＝⟨ ap (k ∙_) (neu-l (k ⁻¹)) ⟩
      k ∙ k ⁻¹                    ＝⟨ cancel .pr₂ ⟩
      e                           ＝⟨ sym (cancel .pr₂) ⟩
      h ∙ h ⁻¹ ∎

  ι : Σ x ꞉ G , x ∈H → G
  ι (x , _) = x
  is-subgroup : IsSubgroup {𝓤} (Σ x ꞉ G , x ∈H) G {{H-is-grp}} {{∈G}}
  is-subgroup = ι , (inj , is-hom)
    where
    inj : left-cancellable ι
    inj {x}{y} P =
      x ＝⟨ to-Σ-＝ (P , ∈H-is-prop (y .pr₁) (transport _∈H P (pr₂ x)) (y .pr₂)) ⟩
      y ∎

    is-hom : IsGroupHomomorphism (Σ x ꞉ G , x ∈H) G {{H-is-grp}} {{∈G}} ι
    is-hom (x , x∈H) (y , y∈H) =
      ι ((x , x∈H) ∙ᴴ (y , y∈H)) ＝⟨by-definition⟩
      x ∙ y ⁻¹ ⁻¹                ＝⟨ ap (x ∙_) (inv-inv y) ⟩
      x ∙ y                      ＝⟨by-definition⟩
      ι (x , x∈H) ∙ ι (y , y∈H) ∎
      where open Group H-is-grp renaming (_∙_ to _∙ᴴ_) hiding (_⁻¹)

module group-000B where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)
open import UF.Base
open import UF.Equiv

open import group-0000
open Group {{...}}
open import group-0004
open import group-0005
open import group-000A

這個命題是說，如果 group homomorphism i : H → G 是 inclusion，那 Kernel 的元素其實只有單位元素 e_H。

proposition-8 : {H G : 𝓤 ̇} {{∈H : Group H}} {{∈G : Group G}}
  (i : H → G) → (is-hom : IsGroupHomomorphism H G i)
  → left-cancellable i
  → ((y : Ker H G i is-hom) → e ＝ y .pr₁)
proposition-8 {𝓤} {H}{G}{{∈H}}{{∈G}} i is-hom inclusion (h , p) = inclusion I
  where
  I : i e ＝ i h
  I = (proposition-4 i is-hom) then (sym p)

這也順便說明了，用 Propopsition 4 就已經知道 Ker i 最少最少也有一個 e_H，因此任何 Kernel 都不是空集合。 事實上這還可以說成，這樣 Kernel 就會跟 𝟙 同構，因為只有一個元素，這也表示這時候 Kernel 是 trivial group。

proposition-8' : {H G : 𝓤 ̇} {{∈H : Group H}} {{∈G : Group G}}
  (i : H → G) → (is-hom : IsGroupHomomorphism H G i)
  → left-cancellable i
  → Ker H G i is-hom ≃ 𝟙 {𝓤}
proposition-8' {𝓤} {H}{G}{{∈H}}{{∈G}} i is-hom inclusion =
  ι , (ρ , λ x → refl) , ρ , final
  where
  ι : Ker H G i is-hom → 𝟙
  ι _ = ⋆
  P4 = proposition-4 i is-hom
  ρ : 𝟙 → Ker H G i is-hom
  ρ ⋆ = e , P4

  final : (x : Ker H G i is-hom) → ρ ⋆ ＝ x
  final (k , hk) =
    ρ ⋆    ＝⟨by-definition⟩
    e , P4 ＝⟨ to-Σ-＝ (I , size (transport (λ h → i h ＝ e) I P4) hk) ⟩
    k , hk ∎
    where
    I : e ＝ k
    I = inclusion (i e ＝⟨ P4 ⟩
                   e   ＝⟨ sym hk ⟩
                   i k ∎)