{-# 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 : ℤ
Generated-by : (G : Group g) → Group.Carrier G → Type g
Generated-by G g =
(x : Carrier) → ∥ (∃ λ (i : ℤ) → x ≡ g ^ i) ∥
where
open Group G
Cyclic : Group g → Type g
Cyclic G = ∥ ∃ (Generated-by G) ∥
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
≃ᴳ→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₂
≃ᴳ→Cyclic→Cyclic : G₁ ≃ᴳ G₂ → Cyclic G₁ → Cyclic G₂
≃ᴳ→Cyclic→Cyclic G₁≃G₂ =
T.∥∥-map λ (_ , gen-by) →
_ , ≃ᴳ→Generated-by→Generated-by G₁≃G₂ gen-by
ℤ-generated-by-1 : Generated-by ℤ-group (+ 1)
ℤ-generated-by-1 i = ∣ i , sym (*-left-identity i) ∣
ℤ-cyclic : Cyclic ℤ-group
ℤ-cyclic = ∣ _ , ℤ-generated-by-1 ∣
ℤ×ℤ-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 ⟩□
⊥ □
ℤ≄ᴳℤ×ℤ : ¬ ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)
ℤ≄ᴳℤ×ℤ =
ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group) ↝⟨ flip ≃ᴳ→Cyclic→Cyclic ℤ-cyclic ⟩
Cyclic (ℤ-group G.× ℤ-group) ↝⟨ ℤ×ℤ-not-cyclic ⟩□
⊥ □
ℤ≢ℤ×ℤ : ℤ-group ≢ (ℤ-group G.× ℤ-group)
ℤ≢ℤ×ℤ =
ℤ-group ≡ (ℤ-group G.× ℤ-group) ↝⟨ flip (subst (ℤ-group ≃ᴳ_)) G.↝ᴳ-refl ⟩
ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group) ↝⟨ ℤ≄ᴳℤ×ℤ ⟩□
⊥ □
infix 4 _≡_mod_
_≡_mod_ : ℤ → ℤ → ℕ → Type
i ≡ j mod n = ∥ (∃ λ k → i ≡ j + k *+ n) ∥
≡-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 ∎)
+-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 ∎)
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 ∎)
*+-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) ∎)
⌊/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 ∎)
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 _ ⟩□
⊥ □
¬⌊+/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 ⟩□
⊥ □
ℤ/[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
ℤ/ℤ-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 ] ∎
ℤ/ℤ-abelian : Abelian ℤ/[1+ n ]ℤ
ℤ/ℤ-abelian = Cyclic→Abelian ℤ/[1+ _ ]ℤ ℤ/ℤ-cyclic
ℤ/ℤ-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 ⟩□
⊥ □
]
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 ∎)
∣