Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typo and consistent names #586

Merged
merged 2 commits into from
Aug 26, 2021
Merged

Typo and consistent names #586

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e392da4
typo and consistent names
HilpAlex Jul 29, 2021
7d61a0e
Merge branch 'master' into consistent-naming
HilpAlex Jul 29, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions Cubical/Algebra/Group/Instances/Bool.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ inverse (isGroup (snd Bool)) true = refl , refl



-- Proof that any Group equivalent to Bool as types is also isomorhic to Bool as groups.
-- Proof that any Group equivalent to Bool as types is also isomorphic to Bool as groups.
open GroupStr renaming (assoc to assocG)

module _ {ℓ : Level} {A : Group ℓ} (e : Iso (fst A) BoolType) where
Expand All @@ -59,8 +59,8 @@ module _ {ℓ : Level} {A : Group ℓ} (e : Iso (fst A) BoolType) where
... | yes p = invIso e
... | no p = compIso notIso (invIso e)

true→0 : Iso.fun IsoABool true ≡ 1g (snd A)
true→0 with (Iso.fun e (1g (snd A))) ≟ true
true→1 : Iso.fun IsoABool true ≡ 1g (snd A)
true→1 with (Iso.fun e (1g (snd A))) ≟ true
... | yes p = sym (cong (Iso.inv e) p) ∙ Iso.leftInv e _
... | no p = sym (cong (Iso.inv e) (¬true→false (Iso.fun e (1g (snd A))) p))
∙ Iso.leftInv e (1g (snd A))
Expand All @@ -71,7 +71,7 @@ module _ {ℓ : Level} {A : Group ℓ} (e : Iso (fst A) BoolType) where
... | yes p | no q = inr (sym (Iso.rightInv IsoABool x) ∙ cong (Iso.fun (IsoABool)) p)
... | no p | no q = inr (⊥-rec (q (sym (Iso.rightInv IsoABool x)
∙∙ cong (Iso.fun IsoABool) (¬false→true _ p)
∙∙ true→0)))
∙∙ true→1)))
... | no p | yes q = inl q

≅Bool : GroupIso Bool A
Expand All @@ -81,14 +81,14 @@ module _ {ℓ : Level} {A : Group ℓ} (e : Iso (fst A) BoolType) where
homHelp : _
homHelp false false with discreteA (Iso.fun IsoABool false) (1g (snd A))
| (decA ((Iso.fun IsoABool false) ·A Iso.fun IsoABool false))
... | yes p | _ = true→0 ∙∙ sym (GroupStr.rid (snd A) (1g (snd A))) ∙∙ cong₂ (_·A_) (sym p) (sym p)
... | no p | inl x = true→0 ∙ sym x
... | no p | inr x = true→0 ∙∙ sym (helper _ x) ∙∙ sym x
... | yes p | _ = true→1 ∙∙ sym (GroupStr.rid (snd A) (1g (snd A))) ∙∙ cong₂ (_·A_) (sym p) (sym p)
... | no p | inl x = true→1 ∙ sym x
... | no p | inr x = true→1 ∙∙ sym (helper _ x) ∙∙ sym x
where
helper : (x : typ A) → x ·A x ≡ x → x ≡ (1g (snd A))
helper x p = sym (GroupStr.rid (snd A) x)
∙∙ cong (x ·A_) (sym (inverse (snd A) x .fst))
∙∙ assocG (snd A) x x (-A x) ∙∙ cong (_·A (-A x)) p
∙∙ inverse (snd A) x .fst
homHelp false true = sym (GroupStr.rid (snd A) _) ∙ cong (Iso.fun IsoABool false ·A_) (sym true→0)
homHelp true y = sym (GroupStr.lid (snd A) _) ∙ cong (_·A (Iso.fun IsoABool y)) (sym true→0)
homHelp false true = sym (GroupStr.rid (snd A) _) ∙ cong (Iso.fun IsoABool false ·A_) (sym true→1)
homHelp true y = sym (GroupStr.lid (snd A) _) ∙ cong (_·A (Iso.fun IsoABool y)) (sym true→1)