diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
index c859e5f451..18b8e33fff 100644
--- a/Cubical.Algebra.AbGroup.Base.html
+++ b/Cubical.Algebra.AbGroup.Base.html
@@ -76,7 +76,7 @@
open IsAbGroup isAbGroup public
AbGroup : ∀ ℓ → Type (ℓ-suc ℓ)
-AbGroup ℓ = TypeWithStr ℓ AbGroupStr
+AbGroup ℓ = TypeWithStr ℓ AbGroupStr
module _ {G : Type ℓ} {0g : G} {_+_ : G → G → G} { -_ : G → G}
(is-setG : isSet G)
@@ -189,7 +189,7 @@
(m : A → A → A)
(u : A)
(inverse : A → A)
- (e : ⟨ G ⟩ ≃ A)
+ (e : ⟨ G ⟩ ≃ A)
(p+ : ∀ x y → e .fst (G .snd ._+_ x y) ≡ m (e .fst x) (e .fst y))
(pu : e .fst (G .snd .0g) ≡ u)
(pinv : ∀ x → e .fst (G .snd .-_ x) ≡ inverse (e .fst x))
@@ -235,7 +235,7 @@
module _ (G : AbGroup ℓ) {A : Type ℓ}
(m : A → A → A)
- (e : ⟨ G ⟩ ≃ A)
+ (e : ⟨ G ⟩ ≃ A)
(p· : ∀ x y → e .fst (G .snd ._+_ x y) ≡ m (e .fst x) (e .fst y))
where
diff --git a/Cubical.Algebra.Algebra.Base.html b/Cubical.Algebra.Algebra.Base.html
index f3ffa17570..65caba1dd3 100644
--- a/Cubical.Algebra.Algebra.Base.html
+++ b/Cubical.Algebra.Algebra.Base.html
@@ -35,7 +35,7 @@
record IsAlgebra (R : Ring ℓ) {A : Type ℓ'}
(0a 1a : A) (_+_ _·_ : A → A → A) (-_ : A → A)
- (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where
+ (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where
constructor isalgebra
@@ -46,8 +46,8 @@
·IsMonoid : IsMonoid 1a _·_
·DistR+ : (x y z : A) → x · (y + z) ≡ (x · y) + (x · z)
·DistL+ : (x y z : A) → (x + y) · z ≡ (x · z) + (y · z)
- ⋆AssocR : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y)
- ⋆AssocL : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y)
+ ⋆AssocR : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y)
+ ⋆AssocL : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y)
open IsLeftModule +IsLeftModule public
@@ -68,7 +68,7 @@
_+_ : A → A → A
_·_ : A → A → A
-_ : A → A
- _⋆_ : ⟨ R ⟩ → A → A
+ _⋆_ : ⟨ R ⟩ → A → A
isAlgebra : IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_
open IsAlgebra isAlgebra public
@@ -116,7 +116,7 @@
module _ {A : Type ℓ'} {0a 1a : A}
(isSet-A : isSet A)
- {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}
+ {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}
(+Assoc : (x y z : A) → x + (y + z) ≡ (x + y) + z)
(+IdR : (x : A) → x + 0a ≡ x)
(+InvR : (x : A) → x + (- x) ≡ 0a)
@@ -126,12 +126,12 @@
(·IdL : (x : A) → 1a · x ≡ x)
(·DistR+ : (x y z : A) → x · (y + z) ≡ (x · y) + (x · z))
(·DistL+ : (x y z : A) → (x + y) · z ≡ (x · z) + (y · z))
- (⋆Assoc : (r s : ⟨ R ⟩) (x : A) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
- (⋆DistR+ : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
- (⋆DistL+ : (r s : ⟨ R ⟩) (x : A) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
+ (⋆Assoc : (r s : ⟨ R ⟩) (x : A) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
+ (⋆DistR+ : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
+ (⋆DistL+ : (r s : ⟨ R ⟩) (x : A) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
(⋆IdL : (x : A) → 1r ⋆ x ≡ x)
- (⋆AssocR : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y))
- (⋆AssocL : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
+ (⋆AssocR : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y))
+ (⋆AssocL : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
where
makeIsAlgebra : IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_
makeIsAlgebra .IsAlgebra.+IsLeftModule = makeIsLeftModule
@@ -162,7 +162,7 @@
pres+ : (x y : A) → f (x M.+ y) ≡ f x N.+ f y
pres· : (x y : A) → f (x M.· y) ≡ f x N.· f y
pres- : (x : A) → f (M.- x) ≡ N.- (f x)
- pres⋆ : (r : ⟨ R ⟩) (y : A) → f (r M.⋆ y) ≡ r N.⋆ f y
+ pres⋆ : (r : ⟨ R ⟩) (y : A) → f (r M.⋆ y) ≡ r N.⋆ f y
unquoteDecl IsAlgebraHomIsoΣ = declareRecordIsoΣ IsAlgebraHomIsoΣ (quote IsAlgebraHom)
open IsAlgebraHom
@@ -173,7 +173,7 @@
A B : Algebra R ℓ
AlgebraHom : (M : Algebra R ℓ') (N : Algebra R ℓ'') → Type _
-AlgebraHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsAlgebraHom (M .snd) f (N .snd)
+AlgebraHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsAlgebraHom (M .snd) f (N .snd)
IsAlgebraEquiv : {A : Type ℓ'} {B : Type ℓ''}
(M : AlgebraStr R A) (e : A ≃ B) (N : AlgebraStr R B)
@@ -181,9 +181,9 @@
IsAlgebraEquiv M e N = IsAlgebraHom M (e .fst) N
AlgebraEquiv : (M : Algebra R ℓ') (N : Algebra R ℓ'') → Type _
-AlgebraEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsAlgebraEquiv (M .snd) e (N .snd)
+AlgebraEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsAlgebraEquiv (M .snd) e (N .snd)
-_$a_ : AlgebraHom A B → ⟨ A ⟩ → ⟨ B ⟩
+_$a_ : AlgebraHom A B → ⟨ A ⟩ → ⟨ B ⟩
f $a x = fst f x
AlgebraEquiv→AlgebraHom : AlgebraEquiv A B → AlgebraHom A B
@@ -193,7 +193,7 @@
(0a 1a : A)
(_+_ _·_ : A → A → A)
(-_ : A → A)
- (_⋆_ : ⟨ R ⟩ → A → A)
+ (_⋆_ : ⟨ R ⟩ → A → A)
→ isProp (IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_)
isPropIsAlgebra R _ _ _ _ _ _ = let open IsLeftModule in
isOfHLevelRetractFromIso 1 IsAlgebraIsoΣ
@@ -224,7 +224,7 @@
isSetAlgebraHom _ N = isSetΣ (isSetΠ (λ _ → is-set))
λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)
where
- open AlgebraStr (str N)
+ open AlgebraStr (str N)
isSetAlgebraEquiv : (M : Algebra R ℓ') (N : Algebra R ℓ'')
@@ -232,8 +232,8 @@
isSetAlgebraEquiv M N = isSetΣ (isOfHLevel≃ 2 M.is-set N.is-set)
λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)
where
- module M = AlgebraStr (str M)
- module N = AlgebraStr (str N)
+ module M = AlgebraStr (str M)
+ module N = AlgebraStr (str N)
AlgebraHom≡ : {φ ψ : AlgebraHom A B} → fst φ ≡ fst ψ → φ ≡ ψ
AlgebraHom≡ = Σ≡Prop λ f → isPropIsAlgebraHom _ _ f _
@@ -272,7 +272,7 @@
{A : Algebra R ℓ}
{B : Algebra R ℓ'}
- {f : ⟨ A ⟩ → ⟨ B ⟩}
+ {f : ⟨ A ⟩ → ⟨ B ⟩}
where
private
@@ -281,9 +281,9 @@
module _
(p1 : f A.1a ≡ B.1a)
- (p+ : (x y : ⟨ A ⟩) → f (x A.+ y) ≡ f x B.+ f y)
- (p· : (x y : ⟨ A ⟩) → f (x A.· y) ≡ f x B.· f y)
- (p⋆ : (r : ⟨ R ⟩) (x : ⟨ A ⟩) → f (r A.⋆ x) ≡ r B.⋆ f x)
+ (p+ : (x y : ⟨ A ⟩) → f (x A.+ y) ≡ f x B.+ f y)
+ (p· : (x y : ⟨ A ⟩) → f (x A.· y) ≡ f x B.· f y)
+ (p⋆ : (r : ⟨ R ⟩) (x : ⟨ A ⟩) → f (r A.⋆ x) ≡ r B.⋆ f x)
where
open IsAlgebraHom
diff --git a/Cubical.Algebra.Algebra.Properties.html b/Cubical.Algebra.Algebra.Properties.html
index ed7fe459ec..c47c18b018 100644
--- a/Cubical.Algebra.Algebra.Properties.html
+++ b/Cubical.Algebra.Algebra.Properties.html
@@ -40,13 +40,13 @@
open RingStr (snd R) renaming (_+_ to _+r_ ; _·_ to _·r_)
open AlgebraStr (A .snd)
- ⋆AnnihilL : (x : ⟨ A ⟩) → 0r ⋆ x ≡ 0a
+ ⋆AnnihilL : (x : ⟨ A ⟩) → 0r ⋆ x ≡ 0a
⋆AnnihilL = ModuleTheory.⋆AnnihilL R (Algebra→Module A)
- ⋆AnnihilR : (r : ⟨ R ⟩) → r ⋆ 0a ≡ 0a
+ ⋆AnnihilR : (r : ⟨ R ⟩) → r ⋆ 0a ≡ 0a
⋆AnnihilR = ModuleTheory.⋆AnnihilR R (Algebra→Module A)
- ⋆Dist· : (x y : ⟨ R ⟩) (a b : ⟨ A ⟩) → (x ·r y) ⋆ (a · b) ≡ (x ⋆ a) · (y ⋆ b)
+ ⋆Dist· : (x y : ⟨ R ⟩) (a b : ⟨ A ⟩) → (x ·r y) ⋆ (a · b) ≡ (x ⋆ a) · (y ⋆ b)
⋆Dist· x y a b = (x ·r y) ⋆ (a · b) ≡⟨ ⋆AssocR _ _ _ ⟩
a · ((x ·r y) ⋆ b) ≡⟨ cong (a ·_) (⋆Assoc _ _ _) ⟩
a · (x ⋆ (y ⋆ b)) ≡⟨ sym (⋆AssocR _ _ _) ⟩
@@ -67,7 +67,7 @@
pres⋆ (snd (idAlgebraHom A)) r x = refl
compIsAlgebraHom :
- {g : ⟨ B ⟩ → ⟨ C ⟩} {f : ⟨ A ⟩ → ⟨ B ⟩}
+ {g : ⟨ B ⟩ → ⟨ C ⟩} {f : ⟨ A ⟩ → ⟨ B ⟩}
→ IsAlgebraHom (B .snd) g (C .snd)
→ IsAlgebraHom (A .snd) f (B .snd)
→ IsAlgebraHom (A .snd) (g ∘ f) (C .snd)
@@ -153,7 +153,7 @@
r ⋆ (f⁻¹ x) ∎
compIsAlgebraEquiv :
- {g : ⟨ B ⟩ ≃ ⟨ C ⟩} {f : ⟨ A ⟩ ≃ ⟨ B ⟩}
+ {g : ⟨ B ⟩ ≃ ⟨ C ⟩} {f : ⟨ A ⟩ ≃ ⟨ B ⟩}
→ IsAlgebraEquiv (B .snd) g (C .snd)
→ IsAlgebraEquiv (A .snd) f (B .snd)
→ IsAlgebraEquiv (A .snd) (compEquiv f g) (C .snd)
@@ -192,13 +192,13 @@
open AlgebraEquivs
Algebra≡ : (A B : Algebra R ℓ') → (
- Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
+ Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
Σ[ q0 ∈ PathP (λ i → p i) (0a (snd A)) (0a (snd B)) ]
Σ[ q1 ∈ PathP (λ i → p i) (1a (snd A)) (1a (snd B)) ]
Σ[ r+ ∈ PathP (λ i → p i → p i → p i) (_+_ (snd A)) (_+_ (snd B)) ]
Σ[ r· ∈ PathP (λ i → p i → p i → p i) (_·_ (snd A)) (_·_ (snd B)) ]
Σ[ s- ∈ PathP (λ i → p i → p i) (-_ (snd A)) (-_ (snd B)) ]
- Σ[ s⋆ ∈ PathP (λ i → ⟨ R ⟩ → p i → p i) (_⋆_ (snd A)) (_⋆_ (snd B)) ]
+ Σ[ s⋆ ∈ PathP (λ i → ⟨ R ⟩ → p i → p i) (_⋆_ (snd A)) (_⋆_ (snd B)) ]
PathP (λ i → IsAlgebra R (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i)) (isAlgebra (snd A))
(isAlgebra (snd B)))
≃ (A ≡ B)
@@ -208,13 +208,13 @@
theIso : Iso _ _
fun theIso (p , q0 , q1 , r+ , r· , s- , s⋆ , t) i = p i
, algebrastr (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i) (t i)
- inv theIso x = cong ⟨_⟩ x , cong (0a ∘ snd) x , cong (1a ∘ snd) x
+ inv theIso x = cong ⟨_⟩ x , cong (0a ∘ snd) x , cong (1a ∘ snd) x
, cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (_⋆_ ∘ snd) x
, cong (isAlgebra ∘ snd) x
rightInv theIso _ = refl
leftInv theIso _ = refl
- caracAlgebra≡ : (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
+ caracAlgebra≡ : (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
caracAlgebra≡ {A = A} {B = B} p q P =
sym (transportTransport⁻ (ua (Algebra≡ A B)) p)
∙∙ cong (transport (ua (Algebra≡ A B))) helper
@@ -230,14 +230,14 @@
λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd B)) _ _)
λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
λ _ → isOfHLevelPathP 1 (isPropIsAlgebra _ _ _ _ _ _ _) _ _)
- (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))
+ (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))
uaCompAlgebraEquiv : (f : AlgebraEquiv A B) (g : AlgebraEquiv B C)
→ uaAlgebra (compAlgebraEquiv f g) ≡ uaAlgebra f ∙ uaAlgebra g
uaCompAlgebraEquiv f g = caracAlgebra≡ _ _ (
- cong ⟨_⟩ (uaAlgebra (compAlgebraEquiv f g))
+ cong ⟨_⟩ (uaAlgebra (compAlgebraEquiv f g))
≡⟨ uaCompEquiv _ _ ⟩
- cong ⟨_⟩ (uaAlgebra f) ∙ cong ⟨_⟩ (uaAlgebra g)
- ≡⟨ sym (cong-∙ ⟨_⟩ (uaAlgebra f) (uaAlgebra g)) ⟩
- cong ⟨_⟩ (uaAlgebra f ∙ uaAlgebra g) ∎)
+ cong ⟨_⟩ (uaAlgebra f) ∙ cong ⟨_⟩ (uaAlgebra g)
+ ≡⟨ sym (cong-∙ ⟨_⟩ (uaAlgebra f) (uaAlgebra g)) ⟩
+ cong ⟨_⟩ (uaAlgebra f ∙ uaAlgebra g) ∎)