------------------------------------------------------------------------
-- Cyclic groups
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Group.Cyclic
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude as P
  hiding (id; _^_) renaming (_∘_ to _⊚_; _+_ to _⊕_)

open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
open import Equivalence-relation equality-with-J
  using (Is-equivalence-relation)
open import Equivalence equality-with-J using (_≃_)
open import Erased.Cubical eq
open import Function-universe equality-with-J hiding (_∘_)
open import Group equality-with-J as G
  using (Group; Abelian; _≃ᴳ_; Homomorphic)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
open import Integer equality-with-J hiding (suc) renaming (_*_ to _⊛_)
import Nat equality-with-J as Nat
open import Quotient eq as Q using (_/_)

open Homomorphic

private
  module ℤG = Group ℤ-group

private
  variable
    a     : Level
    A     : Type a
    g     : A
    G₁ G₂ : Group g
    n     : ℕ
    i j k : ℤ

------------------------------------------------------------------------
-- Cyclic groups

-- The property of being generated by an element.

Generated-by : (G : Group g) → Group.Carrier G → Type g
Generated-by G g =
  (x : Carrier) → ∥ (∃ λ (i : ℤ) → x ≡ g ^ i) ∥
  where
  open Group G

-- The property of being cyclic.

Cyclic : Group g → Type g
Cyclic G = ∥ ∃ (Generated-by G) ∥

-- Cyclic groups are abelian.

Cyclic→Abelian : (G : Group g) → Cyclic G → Abelian G
Cyclic→Abelian G c x y =
  flip (T.rec Carrier-is-set) c          λ (g , gen-by) →
  flip (T.rec Carrier-is-set) (gen-by x) λ (i , x≡) →
  flip (T.rec Carrier-is-set) (gen-by y) λ (j , y≡) →
    x ∘ y          ≡⟨ cong₂ _∘_ x≡ y≡ ⟩
    g ^ i ∘ g ^ j  ≡⟨ ^∘^ i ⟩
    g ^ (i + j)    ≡⟨ cong (g ^_) $ +-comm i ⟩
    g ^ (j + i)    ≡⟨ sym $ ^∘^ j ⟩
    g ^ j ∘ g ^ i  ≡⟨ sym $ cong₂ _∘_ y≡ x≡ ⟩∎
    y ∘ x          ∎
  where
  open Group G

-- If two groups are isomorphic, and one is generated by g, then the
-- other is generated by the image of g under the isomorphism.

≃ᴳ→Generated-by→Generated-by :
  (G₁≃G₂ : G₁ ≃ᴳ G₂) →
  Generated-by G₁ g →
  Generated-by G₂ (to G₁≃G₂ g)
≃ᴳ→Generated-by→Generated-by {G₁} {G₂} {g} G₁≃G₂ gen-by x =
  flip T.∥∥-map (gen-by (_≃_.from (G₁≃G₂ .related) x)) λ (i , x≡) →
    i
  , (x                    ≡⟨ sym $ _≃_.from-to (G₁≃G₂ .related) x≡ ⟩
     to G₁≃G₂ (g G₁.^ i)  ≡⟨ G.→ᴳ-^ G₁≃G₂ g i ⟩∎
     to G₁≃G₂ g G₂.^ i    ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- If two groups are isomorphic, and one is cyclic, then the other one
-- is cyclic.

≃ᴳ→Cyclic→Cyclic : G₁ ≃ᴳ G₂ → Cyclic G₁ → Cyclic G₂
≃ᴳ→Cyclic→Cyclic G₁≃G₂ =
  T.∥∥-map λ (_ , gen-by) →
    _ , ≃ᴳ→Generated-by→Generated-by G₁≃G₂ gen-by

------------------------------------------------------------------------
-- The group of integers is cyclic

-- The group of integers is generated by + 1.

ℤ-generated-by-1 : Generated-by ℤ-group (+ 1)
ℤ-generated-by-1 i = ∣ i , sym (*-left-identity i) ∣

-- The group of integers is cyclic.

ℤ-cyclic : Cyclic ℤ-group
ℤ-cyclic = ∣ _ , ℤ-generated-by-1 ∣

------------------------------------------------------------------------
-- The group ℤ × ℤ is not cyclic

-- The direct product of the group of integers and the group of
-- integers is not cyclic.

ℤ×ℤ-not-cyclic : ¬ Cyclic (ℤ-group G.× ℤ-group)
ℤ×ℤ-not-cyclic =
  T.rec ⊥-propositional λ (g , gen-by) →
  flip (T.rec ⊥-propositional) (gen-by (+ 0 , + 1)) λ (i , 0,1≡) →
  flip (T.rec ⊥-propositional) (gen-by (+ 1 , + 0)) λ (j , 1,0≡) →
  lemma₂ g i j (0,1≡ , 1,0≡)
  where
  module G² = Group (ℤ-group G.× ℤ-group)

  0≡*+→≡0 : ∀ n i → + 0 ≡ i *+ P.suc n → i ≡ + 0
  0≡*+→≡0 n i 0≡ = case -⊎0⊎+ i of λ where
    (inj₁ neg)        → ⊥-elim $ ¬-0 (<0→*+suc<0 i n neg) (sym 0≡)
    (inj₂ (inj₁ ≡0))  → ≡0
    (inj₂ (inj₂ pos)) → ⊥-elim $ ¬+0 (>0→*+suc> i n pos) (sym 0≡)

  1≢0* : ∀ i → + 1 ≢ + 0 ⊛ i
  1≢0* i =
    + 1 ≡ + 0 ⊛ i  ↝⟨ flip trans (ℤG.id^ i) ⟩
    + 1 ≡ + 0      ↝⟨ +[1+]≢- ⟩□
    ⊥              □

  -≡0→≡0 : - i ≡ + 0 → i ≡ + 0
  -≡0→≡0 {i} hyp =
    i      ≡⟨ sym $ ℤG.involutive _ ⟩
    - - i  ≡⟨ cong -_ hyp ⟩
    - + 0  ≡⟨ ℤG.identity ⟩∎
    + 0    ∎

  lemma₁ :
    ∀ g₁ g₂ i j →
    ¬ ((+ 0 ≡ g₁ ⊛ i × + 1 ≡ g₂ ⊛ i) ×
       (+ 1 ≡ g₁ ⊛ j × + 0 ≡ g₂ ⊛ j))
  lemma₁ _ _ (+ zero) _ =
    (_ × + 1 ≡ + 0) × _  ↝⟨ proj₂ ⊚ proj₁ ⟩
    + 1 ≡ + 0            ↝⟨ +[1+]≢- ⟩□
    ⊥                    □

  lemma₁ g₁ g₂ (+ P.suc m) j =
    (+ 0 ≡ g₁ *+ P.suc m × _) × (+ 1 ≡ g₁ ⊛ j × _)  ↝⟨ Σ-map (0≡*+→≡0 m _ ⊚ proj₁) proj₁ ⟩
    g₁ ≡ + 0 × + 1 ≡ g₁ ⊛ j                         ↝⟨ (λ (p , q) → trans q (cong (_⊛ j) p)) ⟩
    + 1 ≡ (+ 0) ⊛ j                                 ↝⟨ 1≢0* j ⟩□
    ⊥                                               □

  lemma₁ g₁ g₂ -[1+ m ] j =
    (+ 0 ≡ (- g₁) *+ P.suc m × _) × (+ 1 ≡ g₁ ⊛ j × _)  ↝⟨ Σ-map (0≡*+→≡0 m _ ⊚ proj₁) proj₁ ⟩
    - g₁ ≡ + 0 × + 1 ≡ g₁ ⊛ j                           ↝⟨ Σ-map -≡0→≡0 P.id ⟩
    g₁ ≡ + 0 × + 1 ≡ g₁ ⊛ j                             ↝⟨ (λ (p , q) → trans q (cong (_⊛ j) p)) ⟩
    + 1 ≡ (+ 0) ⊛ j                                     ↝⟨ 1≢0* j ⟩□
    ⊥                                                   □

  lemma₂ : ∀ g i j → ¬ ((+ 0 , + 1) ≡ g G².^ i × (+ 1 , + 0) ≡ g G².^ j)
  lemma₂ g@(g₁ , g₂) i j =
    (+ 0 , + 1) ≡ g G².^ i × (+ 1 , + 0) ≡ g G².^ j  ↝⟨ Σ-map (flip trans (G.^-× ℤ-group ℤ-group i))
                                                              (flip trans (G.^-× ℤ-group ℤ-group j)) ⟩
    (+ 0 , + 1) ≡ (g₁ ⊛ i , g₂ ⊛ i) ×
    (+ 1 , + 0) ≡ (g₁ ⊛ j , g₂ ⊛ j)                  ↔⟨ inverse $ ≡×≡↔≡ ×-cong ≡×≡↔≡ ⟩

    (+ 0 ≡ g₁ ⊛ i × + 1 ≡ g₂ ⊛ i) ×
    (+ 1 ≡ g₁ ⊛ j × + 0 ≡ g₂ ⊛ j)                    ↝⟨ lemma₁ g₁ g₂ i j ⟩□

    ⊥                                                □

-- The group of integers is not isomorphic to the direct product of
-- the group of integers and the group of integers.

ℤ≄ᴳℤ×ℤ : ¬ ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)
ℤ≄ᴳℤ×ℤ =
  ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)  ↝⟨ flip ≃ᴳ→Cyclic→Cyclic ℤ-cyclic ⟩
  Cyclic (ℤ-group G.× ℤ-group)      ↝⟨ ℤ×ℤ-not-cyclic ⟩□
  ⊥                                 □

-- The group of integers is not equal to the direct product of the
-- group of integers and the group of integers.

ℤ≢ℤ×ℤ : ℤ-group ≢ (ℤ-group G.× ℤ-group)
ℤ≢ℤ×ℤ =
  ℤ-group ≡ (ℤ-group G.× ℤ-group)   ↝⟨ flip (subst (ℤ-group ≃ᴳ_)) G.↝ᴳ-refl ⟩
  ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)  ↝⟨ ℤ≄ᴳℤ×ℤ ⟩□
  ⊥                                 □

------------------------------------------------------------------------
-- The "equality modulo n" relation

-- Equality modulo n.

infix 4 _≡_mod_

_≡_mod_ : ℤ → ℤ → ℕ → Type
i ≡ j mod n = ∥ (∃ λ k → i ≡ j + k *+ n) ∥

-- The relation _≡_mod n is an equivalence relation.

≡-mod-is-equivalence-relation :
  ∀ n → Is-equivalence-relation (_≡_mod n)
≡-mod-is-equivalence-relation n = λ where
  .Is-equivalence-relation.reflexive {x = i} →
    ∣ + 0
    , (i             ≡⟨ sym +-right-identity ⟩
       i + + 0       ≡⟨ cong (_+_ i) $ sym $ ℤG.id^+ n ⟩∎
       i + + 0 *+ n  ∎)
    ∣
  .Is-equivalence-relation.symmetric {x = i} {y = j} →
    T.∥∥-map λ (k , i≡j+kn) →
        - k
      , (j                        ≡⟨ sym +-right-identity ⟩
         j + + 0                  ≡⟨ cong (_+_ j) $ sym $ +-right-inverse (k *+ n) ⟩
         j + (k *+ n - k *+ n)    ≡⟨ cong (_+_ j) $ cong (_+_ (k *+ n)) $ ℤG.^+⁻¹ n ⟩
         j + (k *+ n + - k *+ n)  ≡⟨ +-assoc j ⟩
         j + k *+ n + - k *+ n    ≡⟨ cong (_+ - k *+ n) $ sym i≡j+kn ⟩∎
         i + - k *+ n             ∎)

  .Is-equivalence-relation.transitive {x = i} {y = j} {z = k} →
    T.rec (Π-closure ext 1 λ _ →
           T.truncation-is-proposition) λ (l₁ , i≡j+l₁n) →
    T.∥∥-map λ (l₂ , j≡k+l₂n) →
        l₂ + l₁
      , (i                        ≡⟨ i≡j+l₁n ⟩
         j + l₁ *+ n              ≡⟨ cong (_+ l₁ *+ n) j≡k+l₂n ⟩
         k + l₂ *+ n + l₁ *+ n    ≡⟨ sym $ +-assoc k ⟩
         k + (l₂ *+ n + l₁ *+ n)  ≡⟨ cong (_+_ k) $ sym $ *+-distrib-+ n ⟩∎
         k + (l₂ + l₁) *+ n       ∎)

-- If i and j are equal modulo n, then i + k and j + k are also equal
-- modulo n.

+-cong : ∀ n j → i ≡ j mod n → i + k ≡ j + k mod n
+-cong {i} {k} n j = T.∥∥-map λ (l , i≡j+ln) →
    l
  , (i + k             ≡⟨ cong (_+ k) i≡j+ln ⟩
     j + l *+ n + k    ≡⟨ sym $ +-assoc j ⟩
     j + (l *+ n + k)  ≡⟨ cong (_+_ j) $ +-comm (l *+ n) ⟩
     j + (k + l *+ n)  ≡⟨ +-assoc j ⟩∎
     j + k + l *+ n    ∎)

-- If i and j are equal modulo n, then - i and - j are also equal
-- modulo n.

negate-cong : ∀ n j → i ≡ j mod n → - i ≡ - j mod n
negate-cong {i} n j = T.∥∥-map λ (k , i≡j+kn) →
    - k
  , (- i               ≡⟨ cong -_ i≡j+kn ⟩
     - (j + k *+ n)    ≡⟨ ℤG.∘⁻¹ {p = j} ⟩
     - (k *+ n) + - j  ≡⟨ +-comm (- (k *+ n)) ⟩
     - j + - (k *+ n)  ≡⟨ cong (_+_ (- j)) $ ℤG.^+⁻¹ n ⟩∎
     - j + - k *+ n    ∎)

-- If i and j are equal modulo n, then i *+ m and j *+ m are equal
-- modulo m * n.

*+-cong : ∀ m → i ≡ j mod n → i *+ m ≡ j *+ m mod m * n
*+-cong {i} {j} {n} m = T.∥∥-map λ (k , i≡j+kn) →
    k
  , (i *+ m                 ≡⟨ cong (_*+ m) i≡j+kn ⟩
     (j + k *+ n) *+ m      ≡⟨ ℤG.∘^+≡^+∘^+ (+-comm j) m ⟩
     j *+ m + k *+ n *+ m   ≡⟨ cong (_+_ (j *+ m)) $ ℤG.^+^+≡^+* n ⟩
     j *+ m + k *+ (n * m)  ≡⟨ cong (_+_ (j *+ m)) $ cong (k *+_) $ Nat.*-comm n ⟩∎
     j *+ m + k *+ (m * n)  ∎)

-- If i and j are equal modulo 2 * n, then ⌊ i /2⌋ and ⌊ j /2⌋ are
-- equal modulo n.

⌊/2⌋-cong : ∀ j n → i ≡ j mod 2 * n → ⌊ i /2⌋ ≡ ⌊ j /2⌋ mod n
⌊/2⌋-cong {i} j n = T.∥∥-map λ (k , i≡j+k2n) →
    k
  , (⌊ i /2⌋                  ≡⟨ cong ⌊_/2⌋ i≡j+k2n ⟩
     ⌊ j + k *+ (2 * n) /2⌋   ≡⟨ cong (⌊_/2⌋ ⊚ (_+_ j) ⊚ (k *+_)) $ sym $ Nat.*-comm n ⟩
     ⌊ j + k *+ (n * 2) /2⌋   ≡⟨ cong (⌊_/2⌋ ⊚ (_+_ j)) $ sym $ ℤG.^+^+≡^+* n ⟩
     ⌊ j + (k *+ n) *+ 2 /2⌋  ≡⟨ ⌊+*+2/2⌋≡ j ⟩∎
     ⌊ j /2⌋ + k *+ n         ∎)

-- It is not the case that 0 is equal to 1 modulo n, if n is at least
-- 2.

0≢1mod2+ : ∀ n → ¬ + 0 ≡ + 1 mod 2 ⊕ n
0≢1mod2+ n = T.rec ⊥-propositional $ uncurry lemma
  where
  lemma : ∀ k → + 0 ≢ + 1 + k *+ (2 ⊕ n)
  lemma (+ 0) =
    + 0 ≡ + 1 + + 0 *+ (2 ⊕ n)  ↝⟨ flip trans (cong (_+_ (+ 1)) $ ℤG.id^+ (2 ⊕ n)) ⟩
    + 0 ≡ + 1 + + 0             ↔⟨⟩
    + 0 ≡ + 1                   ↝⟨ +[1+]≢- ⊚ sym ⟩□
    ⊥                           □
  lemma (+ suc k) =
    + 0 ≡ + 1 + + suc k *+ (2 ⊕ n)         ↝⟨ flip ¬+0 ⊚ sym ⟩
    ¬ Positive (+ 1 + + suc k *+ (2 ⊕ n))  ↝⟨ _⊚ >0→>0→+>0 (+ 1) (+ suc k *+ (2 ⊕ n)) _ ⟩
    ¬ Positive (+ suc k *+ (2 ⊕ n))        ↝⟨ _$ >0→*+suc> (+ suc k) (suc n) _ ⟩□
    ⊥                                      □
  lemma -[1+ zero ] =
    + 0 ≡ + 1 + -[1+ 0 ] *+ (2 ⊕ n)             ↝⟨ flip trans (+-assoc (+ 1) {j = -[1+ 0 ]} {k = -[1+ 0 ] *+ (1 ⊕ n)}) ⟩
    + 0 ≡ + 1 + -[1+ 0 ] + -[1+ 0 ] *+ (1 ⊕ n)  ↝⟨ flip trans +-left-identity ⟩
    + 0 ≡ -[1+ 0 ] *+ (1 ⊕ n)                   ↝⟨ flip ¬-0 ⊚ sym ⟩
    ¬ Negative (-[1+ 0 ] *+ (1 ⊕ n))            ↝⟨ _$ <0→*+suc<0 -[1+ 0 ] n _ ⟩□
    ⊥                                           □
  lemma -[1+ suc k ] =
    + 0 ≡ + 1 + -[1+ suc k ] *+ (2 ⊕ n)                 ↝⟨ flip trans (+-assoc (+ 1) {j = -[1+ suc k ]} {k = -[1+ suc k ] *+ (1 ⊕ n)}) ⟩
    + 0 ≡ + 1 + -[1+ suc k ] + -[1+ suc k ] *+ (1 ⊕ n)  ↔⟨⟩
    + 0 ≡ -[1+ k ] + -[1+ suc k ] *+ (1 ⊕ n)            ↝⟨ flip ¬-0 ⊚ sym ⟩
    ¬ Negative (-[1+ k ] + -[1+ suc k ] *+ (1 ⊕ n))     ↝⟨ _⊚ <0→<0→+<0 -[1+ k ] (-[1+ suc k ] *+ (1 ⊕ n)) _ ⟩
    ¬ Negative (-[1+ suc k ] *+ (1 ⊕ n))                ↝⟨ _$ <0→*+suc<0 -[1+ suc k ] n _ ⟩□
    ⊥                                                   □

-- It is not the case that ⌊_/2⌋ distributes over _+_ modulo 2 ⊕ n
-- (for any n).

¬⌊+/2⌋≡⌊/2⌋+⌊/2⌋mod2+ :
  ¬ (∀ i j → ⌊ i + j /2⌋ ≡ ⌊ i /2⌋ + ⌊ j /2⌋ mod 2 ⊕ n)
¬⌊+/2⌋≡⌊/2⌋+⌊/2⌋mod2+ {n} =
  (∀ i j → ⌊ i + j /2⌋ ≡ ⌊ i /2⌋ + ⌊ j /2⌋ mod 2 ⊕ n)  ↝⟨ (_$ (+ 1)) ⊚ (_$ (+ 1)) ⟩
  + 1 ≡ + 0 mod 2 ⊕ n                                  ↝⟨ ≡-mod-is-equivalence-relation (2 ⊕ n)
                                                            .Is-equivalence-relation.symmetric ⟩
  + 0 ≡ + 1 mod 2 ⊕ n                                  ↝⟨ 0≢1mod2+ n ⟩□
  ⊥                                                    □

------------------------------------------------------------------------
-- Finite cyclic groups

-- ℤ/[1+ n ]ℤ is the group of integers with addition modulo 1 + n (the
-- finite cyclic group of order 1 + n).

ℤ/[1+_]ℤ : ℕ → Group lzero
ℤ/[1+ n ]ℤ = λ where
    .Group.Carrier        → ℤ / (_≡_mod suc n)
    .Group.Carrier-is-set → Q./-is-set
    .Group._∘_            → _+′_
    .Group.id             → Q.[ + 0 ]
    .Group._⁻¹            → -′_
    .Group.left-identity  → left-identity
    .Group.right-identity → right-identity
    .Group.assoc          → assoc
    .Group.left-inverse   → left-inverse
    .Group.right-inverse  → right-inverse
  where
  _+′_ : ℤ / (_≡_mod suc n) → ℤ / (_≡_mod suc n) → ℤ / (_≡_mod suc n)
  _+′_ = Q.rec λ where
    .Q.[]ʳ i → _+_ i Q./-map λ j₁ j₂ →
      j₁ ≡ j₂ mod suc n            ↝⟨ +-cong (suc n) j₂ ⟩
      j₁ + i ≡ j₂ + i mod suc n    ↝⟨ ≡⇒↝ _ $ cong₂ (_≡_mod suc n) (+-comm j₁) (+-comm j₂) ⟩□
      i + j₁ ≡ i + j₂ mod suc n    □
    .Q.is-setʳ →
      Π-closure ext 2 λ _ →
      Q./-is-set
    .Q.[]-respects-relationʳ {x = i₁} {y = i₂} i₁≡i₂ →
      ⟨ext⟩ $ Q.elim-prop λ where
        .Q.is-propositionʳ _ → Q./-is-set
        .Q.[]ʳ j             →         $⟨ i₁≡i₂ ⟩
          i₁ ≡ i₂ mod suc n            ↝⟨ +-cong (suc n) i₂ ⟩
          i₁ + j ≡ i₂ + j mod suc n    ↝⟨ Q.[]-respects-relation ⟩□
          Q.[ i₁ + j ] ≡ Q.[ i₂ + j ]  □

  -′_ : ℤ / (_≡_mod suc n) → ℤ / (_≡_mod suc n)
  -′_ = -_ Q./-map λ i₁ i₂ →
    i₁ ≡ i₂ mod suc n      ↝⟨ negate-cong (suc n) i₂ ⟩□
    - i₁ ≡ - i₂ mod suc n  □

  left-identity : ∀ i → Q.[ + 0 ] +′ i ≡ i
  left-identity = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ _             → cong Q.[_] +-left-identity

  right-identity : ∀ i → i +′ Q.[ + 0 ] ≡ i
  right-identity = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ _             → cong Q.[_] +-right-identity

  assoc : ∀ i j k → (i +′ (j +′ k)) ≡ ((i +′ j) +′ k)
  assoc = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Π-closure ext 1 λ _ →
                           Π-closure ext 1 λ _ →
                           Q./-is-set
    .Q.[]ʳ i             → Q.elim-prop λ where
      .Q.is-propositionʳ _ → Π-closure ext 1 λ _ →
                             Q./-is-set
      .Q.[]ʳ _             → Q.elim-prop λ where
        .Q.is-propositionʳ _ → Q./-is-set
        .Q.[]ʳ _             → cong Q.[_] $ +-assoc i

  left-inverse : ∀ i → ((-′ i) +′ i) ≡ Q.[ + 0 ]
  left-inverse = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ i             → cong Q.[_] $ +-left-inverse i

  right-inverse : ∀ i → (i +′ (-′ i)) ≡ Q.[ + 0 ]
  right-inverse = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ i             → cong Q.[_] $ +-right-inverse i

-- ℤ/[1+ n ]ℤ is cyclic.

ℤ/ℤ-cyclic : Cyclic ℤ/[1+ n ]ℤ
ℤ/ℤ-cyclic {n} =
  ∣ Q.[ + 1 ]
  , (Q.elim-prop λ where
       .Q.is-propositionʳ _ → T.truncation-is-proposition
       .Q.[]ʳ i             →
         ∣ i
         , (Q.[ i ]           ≡⟨ cong Q.[_] $ sym $ *-left-identity i ⟩
            Q.[ + 1 ⊛ i ]     ≡⟨ lemma i ⟩∎
            Q.[ + 1 ] ℤ/.^ i  ∎)
         ∣)
  ∣
  where
  module ℤ/ = Group ℤ/[1+ n ]ℤ

  *+-lemma : ∀ n → Q.[ + 1 *+ n ] ≡ Q.[ + 1 ] ℤ/.^+ n
  *+-lemma zero    = refl _
  *+-lemma (suc n) =
    Q.[ + 1 *+ suc n ]                ≡⟨⟩
    Q.[ + 1 ] ℤ/.∘ Q.[ + 1 *+ n ]     ≡⟨ cong (Q.[ + 1 ] ℤ/.∘_) $ *+-lemma n ⟩∎
    Q.[ + 1 ] ℤ/.∘ Q.[ + 1 ] ℤ/.^+ n  ∎

  lemma : ∀ i → Q.[ + 1 ⊛ i ] ≡ Q.[ + 1 ] ℤ/.^ i
  lemma (+ n)    = *+-lemma n
  lemma -[1+ n ] =
    Q.[ + 1 ⊛ -[1+ n ] ]           ≡⟨⟩
    Q.[ -[ 1 ] *+ suc n ]          ≡⟨ cong Q.[_] $ sym $ ℤG.^+⁻¹ {p = + 1} (suc n) ⟩
    Q.[ - (+ 1 *+ suc n) ]         ≡⟨⟩
    Q.[ + 1 *+ suc n ] ℤ/.⁻¹       ≡⟨ cong ℤ/._⁻¹ $ *+-lemma (suc n) ⟩
    (Q.[ + 1 ] ℤ/.^+ suc n) ℤ/.⁻¹  ≡⟨ ℤ/.^+⁻¹ {p = Q.[ + 1 ]} (suc n) ⟩
    (Q.[ + 1 ] ℤ/.⁻¹) ℤ/.^+ suc n  ≡⟨⟩
    Q.[ + 1 ] ℤ/.^ -[1+ n ]        ∎

-- ℤ/[1+ n ]ℤ is abelian.

ℤ/ℤ-abelian : Abelian ℤ/[1+ n ]ℤ
ℤ/ℤ-abelian = Cyclic→Abelian ℤ/[1+ _ ]ℤ ℤ/ℤ-cyclic

-- For finite cyclic groups of order at least 2 the number 0 is not
-- equal to 1.
--
-- The proof uses propositional extensionality.

ℤ/ℤ-0≢1 :
  ∀ n →
  _≢_ {A = Group.Carrier ℤ/[1+ suc n ]ℤ}
    Q.[ + 0 ] Q.[ + 1 ]
ℤ/ℤ-0≢1 n =
  Stable-¬
    [ Q.[ + 0 ] ≡ Q.[ + 1 ]  ↔⟨ inverse $
                                Q.related≃[equal]
                                  prop-ext
                                  (≡-mod-is-equivalence-relation (2 P.+ n))
                                  T.truncation-is-proposition ⟩
      (+ 0 ≡ + 1 mod 2 ⊕ n)  ↝⟨ 0≢1mod2+ n ⟩□
      ⊥                      □
    ]

-- If any element in ℤ/2ℤ is added to itself we get 0.

private
  module ℤ/2ℤ = Group ℤ/[1+ 1 ]ℤ

ℤ/2ℤ-+≡0 : ∀ i → i ℤ/2ℤ.∘ i ≡ ℤ/2ℤ.id
ℤ/2ℤ-+≡0 = Q.elim-prop λ where
  .Q.is-propositionʳ _ → Q./-is-set
  .Q.[]ʳ i → Q.[]-respects-relation
    ∣ i
    , (i + i          ≡⟨ cong (_+_ i) $ sym +-right-identity ⟩
       i + (i + + 0)  ≡⟨⟩
       i *+ 2         ≡⟨ sym +-left-identity ⟩∎
       + 0 + i *+ 2   ∎)
    ∣