diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
index 497a56efcc..eb8d149706 100644
--- a/Cubical.Algebra.AbGroup.Base.html
+++ b/Cubical.Algebra.AbGroup.Base.html
@@ -88,7 +88,7 @@
makeIsAbGroup : IsAbGroup 0g _+_ -_
makeIsAbGroup .IsAbGroup.isGroup =
- makeIsGroup is-setG +Assoc +IdR
+ makeIsGroup is-setG +Assoc +IdR
(λ x → +Comm _ _ ∙ +IdR x)
+InvR
(λ x → +Comm _ _ ∙ +InvR x)
@@ -140,218 +140,218 @@
AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.·Comm = IsAbGroup.+Comm GisGroup
isSetAbGroup : (A : AbGroup ℓ) → isSet ⟨ A ⟩
-isSetAbGroup A = isSetGroup (AbGroup→Group A)
-
-AbGroupHom : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
-AbGroupHom G H = GroupHom (AbGroup→Group G) (AbGroup→Group H)
-
-AbGroupIso : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
-AbGroupIso G H = GroupIso (AbGroup→Group G) (AbGroup→Group H)
-
-IsAbGroupEquiv : {A : Type ℓ} {B : Type ℓ'}
- (G : AbGroupStr A) (e : A ≃ B) (H : AbGroupStr B) → Type (ℓ-max ℓ ℓ')
-IsAbGroupEquiv G e H = IsGroupHom (AbGroupStr→GroupStr G) (e .fst) (AbGroupStr→GroupStr H)
-
-AbGroupEquiv : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
-AbGroupEquiv G H = Σ[ e ∈ (G .fst ≃ H .fst) ] IsAbGroupEquiv (G .snd) e (H .snd)
-
-isPropIsAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
- → isProp (IsAbGroup 0g _+_ (-_))
-isPropIsAbGroup 0g _+_ -_ =
- isOfHLevelRetractFromIso 1 IsAbGroupIsoΣ
- (isPropΣ (isPropIsGroup 0g _+_ (-_))
- (λ grp → isPropΠ2 (λ _ _ → grp .is-set _ _)))
- where
- open IsGroup
-
-
-𝒮ᴰ-AbGroup : DUARel (𝒮-Univ ℓ) AbGroupStr ℓ
-𝒮ᴰ-AbGroup =
- 𝒮ᴰ-Record (𝒮-Univ _) IsAbGroupEquiv
- (fields:
- data[ _+_ ∣ autoDUARel _ _ ∣ pres· ]
- data[ 0g ∣ autoDUARel _ _ ∣ pres1 ]
- data[ -_ ∣ autoDUARel _ _ ∣ presinv ]
- prop[ isAbGroup ∣ (λ _ _ → isPropIsAbGroup _ _ _) ])
- where
- open AbGroupStr
- open IsGroupHom
-
-
-AbGroupPath : (G H : AbGroup ℓ) → (AbGroupEquiv G H) ≃ (G ≡ H)
-AbGroupPath = ∫ 𝒮ᴰ-AbGroup .UARel.ua
-
-
-
-
-
-
-
-
-module _ (G : AbGroup ℓ) {A : Type ℓ}
- (m : A → A → A)
- (u : A)
- (inverse : A → 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))
- where
-
- private
- module G = AbGroupStr (G .snd)
-
- BaseΣ : Type (ℓ-suc ℓ)
- BaseΣ = Σ[ B ∈ Type ℓ ] (B → B → B) × B × (B → B)
-
- FamilyΣ : BaseΣ → Type ℓ
- FamilyΣ (B , m , u , i) = IsAbGroup u m i
-
- inducedΣ : FamilyΣ (A , m , u , inverse)
- inducedΣ =
- subst FamilyΣ
- (UARel.≅→≡ (autoUARel BaseΣ) (e , p+ , pu , pinv))
- G.isAbGroup
-
- InducedAbGroup : AbGroup ℓ
- InducedAbGroup .fst = A
- InducedAbGroup .snd ._+_ = m
- InducedAbGroup .snd .0g = u
- InducedAbGroup .snd .-_ = inverse
- InducedAbGroup .snd .isAbGroup = inducedΣ
-
- InducedAbGroupEquiv : AbGroupEquiv G InducedAbGroup
- fst InducedAbGroupEquiv = e
- snd InducedAbGroupEquiv = makeIsGroupHom p+
-
- InducedAbGroupPath : G ≡ InducedAbGroup
- InducedAbGroupPath = AbGroupPath _ _ .fst InducedAbGroupEquiv
-
-
-
-
-
-
-
-
-
-
-module _ (G : AbGroup ℓ) {A : Type ℓ}
- (m : A → A → A)
- (e : ⟨ G ⟩ ≃ A)
- (p· : ∀ x y → e .fst (G .snd ._+_ x y) ≡ m (e .fst x) (e .fst y))
- where
-
- private
- module G = AbGroupStr (G .snd)
-
- FamilyΣ : Σ[ B ∈ Type ℓ ] (B → B → B) → Type ℓ
- FamilyΣ (B , n) = Σ[ e ∈ B ] Σ[ i ∈ (B → B) ] IsAbGroup e n i
-
- inducedΣ : FamilyΣ (A , m)
- inducedΣ =
- subst FamilyΣ
- (UARel.≅→≡ (autoUARel (Σ[ B ∈ Type ℓ ] (B → B → B))) (e , p·))
- (G.0g , G.-_ , G.isAbGroup)
-
- InducedAbGroupFromPres· : AbGroup ℓ
- InducedAbGroupFromPres· .fst = A
- InducedAbGroupFromPres· .snd ._+_ = m
- InducedAbGroupFromPres· .snd .0g = inducedΣ .fst
- InducedAbGroupFromPres· .snd .-_ = inducedΣ .snd .fst
- InducedAbGroupFromPres· .snd .isAbGroup = inducedΣ .snd .snd
-
- InducedAbGroupEquivFromPres· : AbGroupEquiv G InducedAbGroupFromPres·
- fst InducedAbGroupEquivFromPres· = e
- snd InducedAbGroupEquivFromPres· = makeIsGroupHom p·
-
- InducedAbGroupPathFromPres· : G ≡ InducedAbGroupFromPres·
- InducedAbGroupPathFromPres· = AbGroupPath _ _ .fst InducedAbGroupEquivFromPres·
-
-
-dirProdAb : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
-dirProdAb A B =
- Group→AbGroup (DirProd (AbGroup→Group A) (AbGroup→Group B))
- λ p q → ΣPathP (+Comm (isAbGroup (snd A)) _ _
- , +Comm (isAbGroup (snd B)) _ _)
-
-trivialAbGroup : ∀ {ℓ} → AbGroup ℓ
-fst trivialAbGroup = Unit*
-0g (snd trivialAbGroup) = tt*
-_+_ (snd trivialAbGroup) _ _ = tt*
-(- snd trivialAbGroup) _ = tt*
-isAbGroup (snd trivialAbGroup) = makeIsAbGroup
- (isProp→isSet isPropUnit*)
- (λ _ _ _ → refl)
- (λ _ → refl)
- (λ _ → refl)
- (λ _ _ → refl)
-
-
-
-move4 : ∀ {ℓ} {A : Type ℓ} (x y z w : A) (_+_ : A → A → A)
- → ((x y z : A) → x + (y + z) ≡ (x + y) + z)
- → ((x y : A) → x + y ≡ y + x)
- → (x + y) + (z + w) ≡ ((x + z) + (y + w))
-move4 x y z w _+_ assoc +Comm =
- sym (assoc x y (z + w))
- ∙∙ cong (x +_) (assoc y z w ∙∙ cong (_+ w) (+Comm y z) ∙∙ sym (assoc z y w))
- ∙∙ assoc x z (y + w)
-
-
-module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where
- private
- strA = snd AGr
- strB = snd BGr
-
- _* = AbGroup→Group
-
- A = fst AGr
- B = fst BGr
- open IsGroupHom
-
- open AbGroupStr strB
- renaming (_+_ to _+B_ ; -_ to -B_ ; 0g to 0B
- ; +IdR to +IdRB ; +IdL to +IdLB
- ; +Assoc to +AssocB ; +Comm to +CommB
- ; +InvR to +InvRB ; +InvL to +InvLB)
- open GroupStr strA
- renaming (_·_ to _∙A_ ; inv to -A_
- ; 1g to 1A ; ·IdR to ·IdRA)
-
- trivGroupHom : GroupHom AGr (BGr *)
- fst trivGroupHom x = 0B
- snd trivGroupHom = makeIsGroupHom λ _ _ → sym (+IdRB 0B)
-
- compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
- fst (compHom f g) x = fst f x +B fst g x
- snd (compHom f g) =
- makeIsGroupHom λ x y
- → cong₂ _+B_ (pres· (snd f) x y) (pres· (snd g) x y)
- ∙ move4 (fst f x) (fst f y) (fst g x) (fst g y)
- _+B_ +AssocB +CommB
-
- invHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
- fst (invHom (f , p)) x = -B f x
- snd (invHom (f , p)) =
- makeIsGroupHom
- λ x y → cong -B_ (pres· p x y)
- ∙∙ GroupTheory.invDistr (BGr *) (f x) (f y)
- ∙∙ +CommB _ _
-
- open AbGroupStr
-
- HomGroup : AbGroup (ℓ-max ℓ ℓ')
- fst HomGroup = GroupHom AGr (BGr *)
- 0g (snd HomGroup) = trivGroupHom
- _+_ (snd HomGroup) = compHom
- - snd HomGroup = invHom
- isAbGroup (snd HomGroup) =
- makeIsAbGroup
- isSetGroupHom
- (λ { (f , p) (g , q) (h , r) → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
- (funExt λ x → +AssocB _ _ _) })
- (λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +IdRB _)})
- ((λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +InvRB _)}))
- (λ { (f , p) (g , q) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → +CommB _ _)})
+isSetAbGroup A = is-set (str A)
+
+AbGroupHom : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
+AbGroupHom G H = GroupHom (AbGroup→Group G) (AbGroup→Group H)
+
+AbGroupIso : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
+AbGroupIso G H = GroupIso (AbGroup→Group G) (AbGroup→Group H)
+
+IsAbGroupEquiv : {A : Type ℓ} {B : Type ℓ'}
+ (G : AbGroupStr A) (e : A ≃ B) (H : AbGroupStr B) → Type (ℓ-max ℓ ℓ')
+IsAbGroupEquiv G e H = IsGroupHom (AbGroupStr→GroupStr G) (e .fst) (AbGroupStr→GroupStr H)
+
+AbGroupEquiv : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
+AbGroupEquiv G H = Σ[ e ∈ (G .fst ≃ H .fst) ] IsAbGroupEquiv (G .snd) e (H .snd)
+
+isPropIsAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
+ → isProp (IsAbGroup 0g _+_ (-_))
+isPropIsAbGroup 0g _+_ -_ =
+ isOfHLevelRetractFromIso 1 IsAbGroupIsoΣ
+ (isPropΣ (isPropIsGroup 0g _+_ (-_))
+ (λ grp → isPropΠ2 (λ _ _ → grp .is-set _ _)))
+ where
+ open IsGroup
+
+
+𝒮ᴰ-AbGroup : DUARel (𝒮-Univ ℓ) AbGroupStr ℓ
+𝒮ᴰ-AbGroup =
+ 𝒮ᴰ-Record (𝒮-Univ _) IsAbGroupEquiv
+ (fields:
+ data[ _+_ ∣ autoDUARel _ _ ∣ pres· ]
+ data[ 0g ∣ autoDUARel _ _ ∣ pres1 ]
+ data[ -_ ∣ autoDUARel _ _ ∣ presinv ]
+ prop[ isAbGroup ∣ (λ _ _ → isPropIsAbGroup _ _ _) ])
+ where
+ open AbGroupStr
+ open IsGroupHom
+
+
+AbGroupPath : (G H : AbGroup ℓ) → (AbGroupEquiv G H) ≃ (G ≡ H)
+AbGroupPath = ∫ 𝒮ᴰ-AbGroup .UARel.ua
+
+
+
+
+
+
+
+
+module _ (G : AbGroup ℓ) {A : Type ℓ}
+ (m : A → A → A)
+ (u : A)
+ (inverse : A → 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))
+ where
+
+ private
+ module G = AbGroupStr (G .snd)
+
+ BaseΣ : Type (ℓ-suc ℓ)
+ BaseΣ = Σ[ B ∈ Type ℓ ] (B → B → B) × B × (B → B)
+
+ FamilyΣ : BaseΣ → Type ℓ
+ FamilyΣ (B , m , u , i) = IsAbGroup u m i
+
+ inducedΣ : FamilyΣ (A , m , u , inverse)
+ inducedΣ =
+ subst FamilyΣ
+ (UARel.≅→≡ (autoUARel BaseΣ) (e , p+ , pu , pinv))
+ G.isAbGroup
+
+ InducedAbGroup : AbGroup ℓ
+ InducedAbGroup .fst = A
+ InducedAbGroup .snd ._+_ = m
+ InducedAbGroup .snd .0g = u
+ InducedAbGroup .snd .-_ = inverse
+ InducedAbGroup .snd .isAbGroup = inducedΣ
+
+ InducedAbGroupEquiv : AbGroupEquiv G InducedAbGroup
+ fst InducedAbGroupEquiv = e
+ snd InducedAbGroupEquiv = makeIsGroupHom p+
+
+ InducedAbGroupPath : G ≡ InducedAbGroup
+ InducedAbGroupPath = AbGroupPath _ _ .fst InducedAbGroupEquiv
+
+
+
+
+
+
+
+
+
+
+module _ (G : AbGroup ℓ) {A : Type ℓ}
+ (m : A → A → A)
+ (e : ⟨ G ⟩ ≃ A)
+ (p· : ∀ x y → e .fst (G .snd ._+_ x y) ≡ m (e .fst x) (e .fst y))
+ where
+
+ private
+ module G = AbGroupStr (G .snd)
+
+ FamilyΣ : Σ[ B ∈ Type ℓ ] (B → B → B) → Type ℓ
+ FamilyΣ (B , n) = Σ[ e ∈ B ] Σ[ i ∈ (B → B) ] IsAbGroup e n i
+
+ inducedΣ : FamilyΣ (A , m)
+ inducedΣ =
+ subst FamilyΣ
+ (UARel.≅→≡ (autoUARel (Σ[ B ∈ Type ℓ ] (B → B → B))) (e , p·))
+ (G.0g , G.-_ , G.isAbGroup)
+
+ InducedAbGroupFromPres· : AbGroup ℓ
+ InducedAbGroupFromPres· .fst = A
+ InducedAbGroupFromPres· .snd ._+_ = m
+ InducedAbGroupFromPres· .snd .0g = inducedΣ .fst
+ InducedAbGroupFromPres· .snd .-_ = inducedΣ .snd .fst
+ InducedAbGroupFromPres· .snd .isAbGroup = inducedΣ .snd .snd
+
+ InducedAbGroupEquivFromPres· : AbGroupEquiv G InducedAbGroupFromPres·
+ fst InducedAbGroupEquivFromPres· = e
+ snd InducedAbGroupEquivFromPres· = makeIsGroupHom p·
+
+ InducedAbGroupPathFromPres· : G ≡ InducedAbGroupFromPres·
+ InducedAbGroupPathFromPres· = AbGroupPath _ _ .fst InducedAbGroupEquivFromPres·
+
+
+dirProdAb : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
+dirProdAb A B =
+ Group→AbGroup (DirProd (AbGroup→Group A) (AbGroup→Group B))
+ λ p q → ΣPathP (+Comm (isAbGroup (snd A)) _ _
+ , +Comm (isAbGroup (snd B)) _ _)
+
+trivialAbGroup : ∀ {ℓ} → AbGroup ℓ
+fst trivialAbGroup = Unit*
+0g (snd trivialAbGroup) = tt*
+_+_ (snd trivialAbGroup) _ _ = tt*
+(- snd trivialAbGroup) _ = tt*
+isAbGroup (snd trivialAbGroup) = makeIsAbGroup
+ (isProp→isSet isPropUnit*)
+ (λ _ _ _ → refl)
+ (λ _ → refl)
+ (λ _ → refl)
+ (λ _ _ → refl)
+
+
+
+move4 : ∀ {ℓ} {A : Type ℓ} (x y z w : A) (_+_ : A → A → A)
+ → ((x y z : A) → x + (y + z) ≡ (x + y) + z)
+ → ((x y : A) → x + y ≡ y + x)
+ → (x + y) + (z + w) ≡ ((x + z) + (y + w))
+move4 x y z w _+_ assoc +Comm =
+ sym (assoc x y (z + w))
+ ∙∙ cong (x +_) (assoc y z w ∙∙ cong (_+ w) (+Comm y z) ∙∙ sym (assoc z y w))
+ ∙∙ assoc x z (y + w)
+
+
+module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where
+ private
+ strA = snd AGr
+ strB = snd BGr
+
+ _* = AbGroup→Group
+
+ A = fst AGr
+ B = fst BGr
+ open IsGroupHom
+
+ open AbGroupStr strB
+ renaming (_+_ to _+B_ ; -_ to -B_ ; 0g to 0B
+ ; +IdR to +IdRB ; +IdL to +IdLB
+ ; +Assoc to +AssocB ; +Comm to +CommB
+ ; +InvR to +InvRB ; +InvL to +InvLB)
+ open GroupStr strA
+ renaming (_·_ to _∙A_ ; inv to -A_
+ ; 1g to 1A ; ·IdR to ·IdRA)
+
+ trivGroupHom : GroupHom AGr (BGr *)
+ fst trivGroupHom x = 0B
+ snd trivGroupHom = makeIsGroupHom λ _ _ → sym (+IdRB 0B)
+
+ compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
+ fst (compHom f g) x = fst f x +B fst g x
+ snd (compHom f g) =
+ makeIsGroupHom λ x y
+ → cong₂ _+B_ (pres· (snd f) x y) (pres· (snd g) x y)
+ ∙ move4 (fst f x) (fst f y) (fst g x) (fst g y)
+ _+B_ +AssocB +CommB
+
+ invHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
+ fst (invHom (f , p)) x = -B f x
+ snd (invHom (f , p)) =
+ makeIsGroupHom
+ λ x y → cong -B_ (pres· p x y)
+ ∙∙ GroupTheory.invDistr (BGr *) (f x) (f y)
+ ∙∙ +CommB _ _
+
+ open AbGroupStr
+
+ HomGroup : AbGroup (ℓ-max ℓ ℓ')
+ fst HomGroup = GroupHom AGr (BGr *)
+ 0g (snd HomGroup) = trivGroupHom
+ _+_ (snd HomGroup) = compHom
+ - snd HomGroup = invHom
+ isAbGroup (snd HomGroup) =
+ makeIsAbGroup
+ isSetGroupHom
+ (λ { (f , p) (g , q) (h , r) → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+ (funExt λ x → +AssocB _ _ _) })
+ (λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +IdRB _)})
+ ((λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +InvRB _)}))
+ (λ { (f , p) (g , q) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → +CommB _ _)})