diff --git a/Cubical.Algebra.CommMonoid.GrothendieckGroup.html b/Cubical.Algebra.CommMonoid.GrothendieckGroup.html
index 8a48a1547d..7d024609db 100644
--- a/Cubical.Algebra.CommMonoid.GrothendieckGroup.html
+++ b/Cubical.Algebra.CommMonoid.GrothendieckGroup.html
@@ -29,7 +29,7 @@
module _ (M : CommMonoid ℓ) where
- open BinaryRelation
+ open BinaryRelation
M² : CommMonoid _
M² = CommMonoidProd M M
@@ -53,7 +53,7 @@
_+/_ : M²/R → M²/R → M²/R
x +/ y = setQuotBinOp isReflR isReflR _·_ isCongR x y
where
- isReflR : isRefl R
+ isReflR : isRefl R
isReflR (a , b) = ε , cong (ε ·_) (·Comm a b)
isCongR : ∀ u u' v v' → R u u' → R v v' → R (u · v) (u' · v')
diff --git a/Cubical.Algebra.CommRing.Localisation.Base.html b/Cubical.Algebra.CommRing.Localisation.Base.html
index f6df6cd542..260b04b328 100644
--- a/Cubical.Algebra.CommRing.Localisation.Base.html
+++ b/Cubical.Algebra.CommRing.Localisation.Base.html
@@ -67,15 +67,15 @@
S⁻¹R = (R × S) / _≈_
- open BinaryRelation
+ open BinaryRelation
- locRefl : isRefl _≈_
+ locRefl : isRefl _≈_
locRefl _ = (1r , SMultClosedSubset .containsOne) , refl
- locSym : isSym _≈_
+ locSym : isSym _≈_
locSym (r , s , s∈S') (r' , s' , s'∈S') (u , p) = u , sym p
- locTrans : isTrans _≈_
+ locTrans : isTrans _≈_
locTrans (r , s , s∈S') (r' , s' , s'∈S') (r'' , s'' , s''∈S') ((u , u∈S') , p) ((v , v∈S') , q) =
((u · v · s') , SMultClosedSubset .multClosed (SMultClosedSubset .multClosed u∈S' v∈S') s'∈S')
, path
@@ -89,10 +89,10 @@
u · s · (v · r'' · s') ≡⟨ solve! R' ⟩
u · v · s' · r'' · s ∎
- locIsEquivRel : isEquivRel _≈_
- isEquivRel.reflexive locIsEquivRel = locRefl
- isEquivRel.symmetric locIsEquivRel = locSym
- isEquivRel.transitive locIsEquivRel = locTrans
+ locIsEquivRel : isEquivRel _≈_
+ isEquivRel.reflexive locIsEquivRel = locRefl
+ isEquivRel.symmetric locIsEquivRel = locSym
+ isEquivRel.transitive locIsEquivRel = locTrans
_+ₗ_ : S⁻¹R → S⁻¹R → S⁻¹R
_+ₗ_ = setQuotSymmBinOp locRefl locTrans _+ₚ_
diff --git a/Cubical.Algebra.Group.QuotientGroup.html b/Cubical.Algebra.Group.QuotientGroup.html
index a69c77073b..135eb2a79f 100644
--- a/Cubical.Algebra.Group.QuotientGroup.html
+++ b/Cubical.Algebra.Group.QuotientGroup.html
@@ -30,7 +30,7 @@
module _ (G' : Group ℓ) (H' : Subgroup G') (Hnormal : isNormal H') where
- open BinaryRelation
+ open BinaryRelation
open isSubgroup (snd H')
open GroupStr (snd G')
open GroupTheory G'
@@ -40,7 +40,7 @@
_~_ : G → G → Type ℓ
x ~ y = x · inv y ∈ ⟪ H' ⟫
- isRefl~ : isRefl _~_
+ isRefl~ : isRefl _~_
isRefl~ x = subst-∈ ⟪ H' ⟫ (sym (·InvR x)) id-closed
G/H : Type ℓ
diff --git a/Cubical.Algebra.IntegerMatrix.Base.html b/Cubical.Algebra.IntegerMatrix.Base.html
index 04ba82c0c0..98c4c4926f 100644
--- a/Cubical.Algebra.IntegerMatrix.Base.html
+++ b/Cubical.Algebra.IntegerMatrix.Base.html
@@ -41,7 +41,7 @@
Norm : ℤ → Type
-Norm n = Acc _<_ (abs n)
+Norm n = Acc _<_ (abs n)
diff --git a/Cubical.Algebra.IntegerMatrix.Diagonalization.html b/Cubical.Algebra.IntegerMatrix.Diagonalization.html
index f78a1b7baf..e6ca910f6a 100644
--- a/Cubical.Algebra.IntegerMatrix.Diagonalization.html
+++ b/Cubical.Algebra.IntegerMatrix.Diagonalization.html
@@ -181,19 +181,19 @@
→ (p : ¬ M zero zero ≡ 0)(h : Norm (M zero zero))
→ (div? : DivStatus (M zero zero) M)
→ DiagStep M
- diagStep-helper M p (acc ind) (badCol i q) =
+ diagStep-helper M p (acc ind) (badCol i q) =
let improved = improveRows M p
normIneq =
ind _ (stDivIneq p q (improved .div zero) (improved .div (suc i)))
in simDiagStep (improved .sim)
(diagStep-helper _ (improved .nonZero) normIneq (divStatus _ _))
- diagStep-helper M p (acc ind) (badRow j q) =
+ diagStep-helper M p (acc ind) (badRow j q) =
let improved = improveCols M p
normIneq =
ind _ (stDivIneq p q (improved .div zero) (improved .div (suc j)))
in simDiagStep (improved .sim)
(diagStep-helper _ (improved .nonZero) normIneq (divStatus _ _))
- diagStep-helper M p (acc ind) (allDone div₁ div₂) =
+ diagStep-helper M p (acc ind) (allDone div₁ div₂) =
let improveColM = improveCols M p
invCol = bézoutRows-inv _ p div₂
divCol = (λ i → transport (λ t → invCol t zero ∣ invCol t (suc i)) (div₁ i))
diff --git a/Cubical.Algebra.IntegerMatrix.Smith.Normalization.html b/Cubical.Algebra.IntegerMatrix.Smith.Normalization.html
index 22ac86afb6..a6367440b6 100644
--- a/Cubical.Algebra.IntegerMatrix.Smith.Normalization.html
+++ b/Cubical.Algebra.IntegerMatrix.Smith.Normalization.html
@@ -151,7 +151,7 @@
Empty.rec (q (∣-refl refl))
reducePivot-helper M _ _ cst (pivot (suc i) zero q) =
Empty.rec (q (subst (λ a → (M zero zero) ∣ a) (sym (cst i)) (∣-refl refl)))
- reducePivot-helper M p (acc ind) _ (pivot zero (suc j) q) =
+ reducePivot-helper M p (acc ind) _ (pivot zero (suc j) q) =
let helperM = reducePivot-induction-helper M p j q
reduceM =
reducePivot-helper
@@ -160,7 +160,7 @@
(ind _ (helperM .normIneq))
(helperM .improved .const) (findPivot _ _)
in simPivotReduced (helperM .improved .sim) reduceM
- reducePivot-helper M p (acc ind) cst (pivot (suc i) (suc j) q) =
+ reducePivot-helper M p (acc ind) cst (pivot (suc i) (suc j) q) =
let swapM = swapFirstRow i M
swapNonZero = (λ r → p (sym (cst i) ∙ (swapM .swapEq zero) ∙ r))
swapDiv =
diff --git a/Cubical.Algebra.Ring.Quotient.html b/Cubical.Algebra.Ring.Quotient.html
index 33deb8773e..6ef88899da 100644
--- a/Cubical.Algebra.Ring.Quotient.html
+++ b/Cubical.Algebra.Ring.Quotient.html
@@ -267,7 +267,7 @@
module idealIsKernel {R : Ring ℓ} (I : IdealsIn R) where
open RingStr (snd R)
open isIdeal (snd I)
- open BinaryRelation.isEquivRel
+ open BinaryRelation.isEquivRel
private
π = quotientHom R I
@@ -281,10 +281,10 @@
I⊆ker x x∈I = eq/ _ _ (subst (_∈ fst I) (sym (x-0≡x x)) x∈I)
private
- _~_ : Rel ⟨ R ⟩ ⟨ R ⟩ ℓ
+ _~_ : Rel ⟨ R ⟩ ⟨ R ⟩ ℓ
x ~ y = x - y ∈ fst I
- ~IsPropValued : BinaryRelation.isPropValued _~_
+ ~IsPropValued : BinaryRelation.isPropValued _~_
~IsPropValued x y = snd (fst I (x - y))
@@ -306,10 +306,10 @@
(x + 0r) + - z ≡⟨ cong (_+ - z) (+IdR _) ⟩
x - z ∎
- ~IsEquivRel : BinaryRelation.isEquivRel _~_
- reflexive ~IsEquivRel x = subst (_∈ fst I) (sym (+InvR x)) 0r-closed
- symmetric ~IsEquivRel x y x~y = subst (_∈ fst I) -[x-y]≡y-x (-closed x~y)
- transitive ~IsEquivRel x y z x~y y~z = subst (_∈ fst I) x-y+y-z≡x-z (+-closed x~y y~z)
+ ~IsEquivRel : BinaryRelation.isEquivRel _~_
+ reflexive ~IsEquivRel x = subst (_∈ fst I) (sym (+InvR x)) 0r-closed
+ symmetric ~IsEquivRel x y x~y = subst (_∈ fst I) -[x-y]≡y-x (-closed x~y)
+ transitive ~IsEquivRel x y z x~y y~z = subst (_∈ fst I) x-y+y-z≡x-z (+-closed x~y y~z)
ker⊆I : kernel π ⊆ fst I
ker⊆I x x∈ker = subst (_∈ fst I) (x-0≡x x) x-0∈I
diff --git a/Cubical.Algebra.ZariskiLattice.Base.html b/Cubical.Algebra.ZariskiLattice.Base.html
index 6188fb254d..f5bcaf525f 100644
--- a/Cubical.Algebra.ZariskiLattice.Base.html
+++ b/Cubical.Algebra.ZariskiLattice.Base.html
@@ -42,8 +42,8 @@
open import Cubical.HITs.SetQuotients as SQ
open Iso
-open BinaryRelation
-open isEquivRel
+open BinaryRelation
+open isEquivRel
private
variable
@@ -83,14 +83,14 @@
_∼_ : A → A → Type ℓ
α ∼ β = (α ≼ β) × (β ≼ α)
- ∼PropValued : isPropValued (_∼_)
+ ∼PropValued : isPropValued (_∼_)
∼PropValued (_ , α) (_ , β) = isProp× (isPropΠ (λ i → √ ⟨ β ⟩ .fst (α i) .snd))
(isPropΠ (λ i → √ ⟨ α ⟩ .fst (β i) .snd))
- ∼EquivRel : isEquivRel (_∼_)
- reflexive ∼EquivRel _ = isRefl≼ , isRefl≼
- symmetric ∼EquivRel _ _ = Σ-swap-Iso .fun
- transitive ∼EquivRel _ _ _ a∼b b∼c = isTrans≼ (fst a∼b) (fst b∼c) , isTrans≼ (snd b∼c) (snd a∼b)
+ ∼EquivRel : isEquivRel (_∼_)
+ reflexive ∼EquivRel _ = isRefl≼ , isRefl≼
+ symmetric ∼EquivRel _ _ = Σ-swap-Iso .fun
+ transitive ∼EquivRel _ _ _ a∼b b∼c = isTrans≼ (fst a∼b) (fst b∼c) , isTrans≼ (snd b∼c) (snd a∼b)
ZL : Type ℓ
@@ -118,7 +118,7 @@
1z = [ 1 , (replicateFinVec 1 1r) ]
_∨z_ : ZL → ZL → ZL
- _∨z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
+ _∨z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
(λ (_ , α) (_ , β) → (_ , α ++Fin β))
(λ (_ , α) (_ , β) → ≡→∼ (cong √
(FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α))))
@@ -131,7 +131,7 @@
√ ⟨ β ++Fin γ ⟩ ∎)
_∧z_ : ZL → ZL → ZL
- _∧z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
+ _∧z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
(λ (_ , α) (_ , β) → (_ , α ··Fin β))
(λ (_ , α) (_ , β) → ≡→∼ (cong √
(FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α))))
@@ -154,7 +154,7 @@
(≡→∼ (cong √ (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α))))
∨zLid : ∀ (𝔞 : ZL) → 0z ∨z 𝔞 ≡ 𝔞
- ∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → eq/ _ _ (reflexive ∼EquivRel _)
+ ∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → eq/ _ _ (reflexive ∼EquivRel _)
∨zRid : ∀ (𝔞 : ZL) → 𝔞 ∨z 0z ≡ 𝔞
∨zRid _ = ∨zComm _ _ ∙ ∨zLid _
diff --git a/Cubical.Algebra.ZariskiLattice.StructureSheaf.html b/Cubical.Algebra.ZariskiLattice.StructureSheaf.html
index ba09ff90ae..18d4d91899 100644
--- a/Cubical.Algebra.ZariskiLattice.StructureSheaf.html
+++ b/Cubical.Algebra.ZariskiLattice.StructureSheaf.html
@@ -80,8 +80,8 @@
open import Cubical.HITs.PropositionalTruncation as PT
open Iso
-open BinaryRelation
-open isEquivRel
+open BinaryRelation
+open isEquivRel
module _ {ℓ : Level} (R' : CommRing ℓ) where
diff --git a/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html b/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html
index c880172a26..68ba26bb55 100644
--- a/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html
+++ b/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html
@@ -76,8 +76,8 @@
open import Cubical.HITs.PropositionalTruncation as PT
open Iso
-open BinaryRelation
-open isEquivRel
+open BinaryRelation
+open isEquivRel
private
variable
diff --git a/Cubical.Categories.Category.Path.html b/Cubical.Categories.Category.Path.html
index d7f9ab9988..69f02cd7c3 100644
--- a/Cubical.Categories.Category.Path.html
+++ b/Cubical.Categories.Category.Path.html
@@ -36,8 +36,8 @@
field
ob≡ : C .ob ≡ C' .ob
Hom≡ : PathP (λ i → ob≡ i → ob≡ i → Type ℓ') (C .Hom[_,_]) (C' .Hom[_,_])
- id≡ : PathP (λ i → BinaryRelation.isRefl' (Hom≡ i)) (C .id) (C' .id)
- ⋆≡ : PathP (λ i → BinaryRelation.isTrans' (Hom≡ i)) (C ._⋆_) (C' ._⋆_)
+ id≡ : PathP (λ i → BinaryRelation.isRefl' (Hom≡ i)) (C .id) (C' .id)
+ ⋆≡ : PathP (λ i → BinaryRelation.isTrans' (Hom≡ i)) (C ._⋆_) (C' ._⋆_)
isSetHom≡ : PathP (λ i → ∀ {x y} → isSet (Hom≡ i x y))
@@ -129,14 +129,14 @@
Hom≡ (CategoryPath≡ _ _ p≡ h≡ i) = h≡ i
id≡ (CategoryPath≡ cp cp' p≡ h≡ i) j {x} = isSet→SquareP
(λ i j → isProp→PathP (λ i →
- isPropIsSet {A = BinaryRelation.isRefl' (h≡ i j)})
+ isPropIsSet {A = BinaryRelation.isRefl' (h≡ i j)})
(isSetImplicitΠ λ x → isSetHom≡ cp j {x} {x})
(isSetImplicitΠ λ x → isSetHom≡ cp' j {x} {x}) i)
(id≡ cp) (id≡ cp') (λ _ → C .id) (λ _ → C' .id)
i j {x}
⋆≡ (CategoryPath≡ cp cp' p≡ h≡ i) j {x} {y} {z} = isSet→SquareP
(λ i j → isProp→PathP (λ i →
- isPropIsSet {A = BinaryRelation.isTrans' (h≡ i j)})
+ isPropIsSet {A = BinaryRelation.isTrans' (h≡ i j)})
(isSetImplicitΠ3 (λ x _ z → isSetΠ2 λ _ _ → isSetHom≡ cp j {x} {z}))
(isSetImplicitΠ3 (λ x _ z → isSetΠ2 λ _ _ → isSetHom≡ cp' j {x} {z})) i)
(⋆≡ cp) (⋆≡ cp') (λ _ → C ._⋆_) (λ _ → C' ._⋆_)
diff --git a/Cubical.Categories.Equivalence.WeakEquivalence.html b/Cubical.Categories.Equivalence.WeakEquivalence.html
index e9169cad99..6bacd6b930 100644
--- a/Cubical.Categories.Equivalence.WeakEquivalence.html
+++ b/Cubical.Categories.Equivalence.WeakEquivalence.html
@@ -147,10 +147,10 @@
(λ _ x i → glue (λ {(i = i0) → _ ; (i = i1) → _ }) (x i)) _ _ Hom≃ (C .id) (F-id F)
⋆≡ WeakEquivlance→CategoryPath = EquivJRel {_∻_ = C' [_,_]}
- (λ Ob e H[_,_] h[_,_] → (⋆* : BinaryRelation.isTrans' H[_,_]) →
+ (λ Ob e H[_,_] h[_,_] → (⋆* : BinaryRelation.isTrans' H[_,_]) →
(∀ {x y z : Ob} f g → (h[ x , z ] ≃$ (⋆* f g)) ≡
C' ._⋆_ (h[ x , _ ] ≃$ f) (h[ y , _ ] ≃$ g) )
- → PathP (λ i → BinaryRelation.isTrans' (RelPathP e h[_,_] i))
+ → PathP (λ i → BinaryRelation.isTrans' (RelPathP e h[_,_] i))
⋆* (λ {x y z} → C' ._⋆_ {x} {y} {z}))
(λ _ x i f g → glue (λ {(i = i0) → _ ; (i = i1) → _ })
(x (unglue (i ∨ ~ i) f) (unglue (i ∨ ~ i) g) i ))
diff --git a/Cubical.Cohomology.Base.html b/Cubical.Cohomology.Base.html
index f6386c7f7d..8255c680e7 100644
--- a/Cubical.Cohomology.Base.html
+++ b/Cubical.Cohomology.Base.html
@@ -33,7 +33,7 @@
open import Cubical.Data.Nat.Base using (ℕ)
open import Cubical.Data.Sigma
open import Cubical.Homotopy.Group.Base
-open import Cubical.HITs.SetTruncation hiding (map)
+open import Cubical.HITs.SetTruncation hiding (map)
open import Cubical.Homotopy.Spectrum
open import Cubical.Homotopy.Loopspace renaming (EH to isCommΩ)
@@ -92,7 +92,7 @@
open GroupStr (snd CohomAsGroup)
isComm : (a b : fst CohomAsGroup) → a · b ≡ b · a
- isComm = elim2 (λ _ _ → isSetPathImplicit)
+ isComm = elim2 (λ _ _ → isSetPathImplicit)
λ a b → ∣ a ∙ b ∣₂ ≡⟨ cong ∣_∣₂ (isCommΩ 0 a b) ⟩
∣ b ∙ a ∣₂ ∎
diff --git a/Cubical.Cohomology.EilenbergMacLane.Base.html b/Cubical.Cohomology.EilenbergMacLane.Base.html
index 6a557998ec..99053d70fb 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Base.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Base.html
@@ -37,7 +37,7 @@
open import Cubical.Algebra.AbGroup.Properties
open import Cubical.HITs.SetTruncation as ST
- hiding (rec ; map ; elim ; elim2 ; elim3)
+ hiding (rec ; map ; elim ; elim2 ; elim3)
private
variable
@@ -56,13 +56,13 @@
module _ {n : ℕ} {G : AbGroup ℓ} {A : Type ℓ'} where
_+ₕ_ : coHom n G A → coHom n G A → coHom n G A
- _+ₕ_ = ST.rec2 squash₂ λ f g → ∣ (λ x → f x +ₖ g x) ∣₂
+ _+ₕ_ = ST.rec2 squash₂ λ f g → ∣ (λ x → f x +ₖ g x) ∣₂
-ₕ_ : coHom n G A → coHom n G A
- -ₕ_ = ST.map λ f x → -ₖ f x
+ -ₕ_ = ST.map λ f x → -ₖ f x
_-ₕ_ : coHom n G A → coHom n G A → coHom n G A
- _-ₕ_ = ST.rec2 squash₂ λ f g → ∣ (λ x → f x -ₖ g x) ∣₂
+ _-ₕ_ = ST.rec2 squash₂ λ f g → ∣ (λ x → f x -ₖ g x) ∣₂
module _ (n : ℕ) {G : AbGroup ℓ} {A : Type ℓ'} where
+ₕ-syntax : coHom n G A → coHom n G A → coHom n G A
@@ -83,27 +83,27 @@
0ₕ = ∣ (λ _ → 0ₖ n) ∣₂
rUnitₕ : (x : coHom n G A) → x +ₕ 0ₕ ≡ x
- rUnitₕ = ST.elim (λ _ → isSetPathImplicit)
+ rUnitₕ = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → rUnitₖ n (f x))
lUnitₕ : (x : coHom n G A) → 0ₕ +[ n ]ₕ x ≡ x
- lUnitₕ = ST.elim (λ _ → isSetPathImplicit)
+ lUnitₕ = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → lUnitₖ n (f x))
commₕ : (x y : coHom n G A) → x +ₕ y ≡ y +ₕ x
- commₕ = ST.elim2 (λ _ _ → isSetPathImplicit)
+ commₕ = ST.elim2 (λ _ _ → isSetPathImplicit)
λ f g → cong ∣_∣₂ (funExt λ x → commₖ n (f x) (g x))
assocₕ : (x y z : coHom n G A) → x +ₕ (y +ₕ z) ≡ (x +ₕ y) +ₕ z
- assocₕ = ST.elim3 (λ _ _ _ → isSetPathImplicit)
+ assocₕ = ST.elim3 (λ _ _ _ → isSetPathImplicit)
λ f g h → cong ∣_∣₂ (funExt λ x → assocₖ n (f x) (g x) (h x))
rCancelₕ : (x : coHom n G A) → x +ₕ (-ₕ x) ≡ 0ₕ
- rCancelₕ = ST.elim (λ _ → isSetPathImplicit)
+ rCancelₕ = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → rCancelₖ n (f x))
lCancelₕ : (x : coHom n G A) → (-ₕ x) +ₕ x ≡ 0ₕ
- lCancelₕ = ST.elim (λ _ → isSetPathImplicit)
+ lCancelₕ = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → lCancelₖ n (f x))
coHomGr : (n : ℕ) (G : AbGroup ℓ) (A : Type ℓ') → AbGroup (ℓ-max ℓ ℓ')
@@ -129,12 +129,12 @@
module _ {n : ℕ} {G : AbGroup ℓ} {A : Pointed ℓ'} where
_+ₕ∙_ : coHomRed n G A → coHomRed n G A → coHomRed n G A
- _+ₕ∙_ = ST.rec2 squash₂
+ _+ₕ∙_ = ST.rec2 squash₂
λ f g → ∣ (λ x → fst f x +ₖ fst g x)
, cong₂ _+ₖ_ (snd f) (snd g) ∙ rUnitₖ n (0ₖ n) ∣₂
-ₕ∙_ : coHomRed n G A → coHomRed n G A
- -ₕ∙_ = ST.map λ f → (λ x → -ₖ (fst f x))
+ -ₕ∙_ = ST.map λ f → (λ x → -ₖ (fst f x))
, cong -ₖ_ (snd f)
∙ -0ₖ n
@@ -144,7 +144,7 @@
module coHomRedAxioms (n : ℕ) {G : AbGroup ℓ} {A : Pointed ℓ'} where
commₕ∙ : (x y : coHomRed n G A) → x +ₕ∙ y ≡ y +ₕ∙ x
commₕ∙ =
- ST.elim2 (λ _ _ → isSetPathImplicit)
+ ST.elim2 (λ _ _ → isSetPathImplicit)
λ f g → cong ∣_∣₂ (ΣPathP (funExt (λ x → commₖ n (fst f x) (fst g x))
, help n _ (sym (snd f)) _ (sym (snd g))))
where
@@ -160,7 +160,7 @@
rCancelₕ∙ : (x : coHomRed n G A) → (x +ₕ∙ (-ₕ∙ x)) ≡ 0ₕ∙ n
rCancelₕ∙ =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (ΣPathP ((funExt (λ x → rCancelₖ n (fst f x)))
, help n _ (sym (snd f))))
where
@@ -177,7 +177,7 @@
lCancelₕ∙ x = commₕ∙ (-ₕ∙ x) x ∙ rCancelₕ∙ x
rUnitₕ∙ : (x : coHomRed n G A) → (x +ₕ∙ 0ₕ∙ n) ≡ x
- rUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
+ rUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (ΣPathP ((funExt λ x → rUnitₖ n (fst f x))
, help n _ (sym (snd f))))
where
@@ -190,7 +190,7 @@
help (suc (suc n)) = J> sym (rUnit refl)
lUnitₕ∙ : (x : coHomRed n G A) → (0ₕ∙ n +ₕ∙ x) ≡ x
- lUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
+ lUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (ΣPathP ((funExt (λ x → lUnitₖ n (fst f x)))
, help n _ (sym (snd f))))
where
@@ -204,7 +204,7 @@
assocₕ∙ : (x y z : coHomRed n G A) → x +ₕ∙ (y +ₕ∙ z) ≡ (x +ₕ∙ y) +ₕ∙ z
assocₕ∙ =
- ST.elim3 (λ _ _ _ → isSetPathImplicit)
+ ST.elim3 (λ _ _ _ → isSetPathImplicit)
λ f g h → cong ∣_∣₂
(ΣPathP ((funExt (λ x → assocₖ n (fst f x) (fst g x) (fst h x)))
, help n _ (sym (snd f)) _ (sym (snd g)) _ (sym (snd h))))
@@ -258,23 +258,23 @@
∣ EM-raw'→EM∙ G (suc n) ∣₁)
main : GroupIso _ _
- Iso.fun (fst main) = ST.map fst
- Iso.inv (fst main) = ST.map λ f → (λ x → f x -ₖ f (pt A))
+ Iso.fun (fst main) = ST.map fst
+ Iso.inv (fst main) = ST.map λ f → (λ x → f x -ₖ f (pt A))
, rCancelₖ (suc n) (f (pt A))
Iso.rightInv (fst main) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → PT.rec (squash₂ _ _)
(λ p → cong ∣_∣₂
(funExt λ x → cong (λ z → f x +ₖ z)
(cong -ₖ_ p ∙ -0ₖ (suc n)) ∙ rUnitₖ (suc n) (f x)))
(con-lem n (f (pt A)))
Iso.leftInv (fst main) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
(funExt λ x → cong (fst f x +ₖ_) (cong -ₖ_ (snd f) ∙ -0ₖ (suc n))
∙ rUnitₖ (suc n) (fst f x)))
snd main =
- makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
+ makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
λ _ _ → refl)
coHom⁰≅coHomRed⁰ : (G : AbGroup ℓ) (A : Pointed ℓ)
@@ -282,19 +282,19 @@
fst (coHom⁰≅coHomRed⁰ G A) = isoToEquiv is
where
is : Iso _ _
- Iso.fun is = uncurry (ST.rec (isSetΠ (λ _ → squash₂))
+ Iso.fun is = uncurry (ST.rec (isSetΠ (λ _ → squash₂))
λ f g → ∣ (λ x → AbGroupStr._+_ (snd G) (fst f x) g) ∣₂)
- Iso.inv is = ST.rec (isSet× squash₂ (is-set (snd G)))
+ Iso.inv is = ST.rec (isSet× squash₂ (is-set (snd G)))
λ f → ∣ (λ x → AbGroupStr._-_ (snd G) (f x) (f (pt A)))
, +InvR (snd G) (f (pt A)) ∣₂ , f (pt A)
- Iso.rightInv is = ST.elim (λ _ → isSetPathImplicit)
+ Iso.rightInv is = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x
→ sym (+Assoc (snd G) _ _ _)
∙∙ cong (AbGroupStr._+_ (snd G) (f x))
(+InvL (snd G) (f (pt A)))
∙∙ +IdR (snd G) (f x))
Iso.leftInv is =
- uncurry (ST.elim
+ uncurry (ST.elim
(λ _ → isSetΠ (λ _ → isOfHLevelPath 2
(isSet× squash₂ (is-set (snd G))) _ _))
λ f → λ g
@@ -311,35 +311,35 @@
, (cong (λ x → AbGroupStr._+_ (snd G) x g) (snd f)
∙ +IdL (snd G) g)))
snd (coHom⁰≅coHomRed⁰ G A) =
- makeIsGroupHom (uncurry (ST.elim (λ _ → isSetΠ2 λ _ _ → isSetPathImplicit)
- λ f1 g1 → uncurry (ST.elim (λ _ → isSetΠ λ _ → isSetPathImplicit)
+ makeIsGroupHom (uncurry (ST.elim (λ _ → isSetΠ2 λ _ _ → isSetPathImplicit)
+ λ f1 g1 → uncurry (ST.elim (λ _ → isSetΠ λ _ → isSetPathImplicit)
λ f2 g2 → cong ∣_∣₂ (funExt λ a → AbGroupTheory.comm-4 G _ _ _ _))))
+ₕ≡id-ℤ/2 : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (x : coHom n ℤ/2 A) → x +ₕ x ≡ 0ₕ n
+ₕ≡id-ℤ/2 n =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → +ₖ≡id-ℤ/2 n (f x))
-ₕConst-ℤ/2 : (n : ℕ) {A : Type ℓ} (x : coHom n ℤ/2 A) → -ₕ x ≡ x
-ₕConst-ℤ/2 zero =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → -Const-ℤ/2 (f x))
-ₕConst-ℤ/2 (suc n) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → -ₖConst-ℤ/2 n (f x))
coHomFun : ∀ {ℓ''} {A : Type ℓ} {B : Type ℓ'} {G : AbGroup ℓ''}
(n : ℕ) (f : A → B)
→ coHom n G B → coHom n G A
-coHomFun n f = ST.map λ g x → g (f x)
+coHomFun n f = ST.map λ g x → g (f x)
coHomHom : ∀ {ℓ''} {A : Type ℓ} {B : Type ℓ'} {G : AbGroup ℓ''}
(n : ℕ) (f : A → B)
→ AbGroupHom (coHomGr n G B) (coHomGr n G A)
fst (coHomHom n f) = coHomFun n f
snd (coHomHom n f) =
- makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
+ makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
λ f g → refl)
coHomEquiv : ∀ {ℓ''} {A : Type ℓ} {B : Type ℓ'} {G : AbGroup ℓ''}
@@ -352,24 +352,24 @@
Iso.fun is = coHomFun n (Iso.fun f)
Iso.inv is = coHomFun n (Iso.inv f)
Iso.rightInv is =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.leftInv f x))
Iso.leftInv is =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.rightInv f x))
snd (coHomEquiv n f) = snd (coHomHom n (Iso.fun f))
coHomFun∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''}
(n : ℕ) (f : A →∙ B)
→ coHomRed n G B → coHomRed n G A
-coHomFun∙ n f = ST.map λ g → g ∘∙ f
+coHomFun∙ n f = ST.map λ g → g ∘∙ f
coHomHom∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''}
(n : ℕ) (f : A →∙ B)
→ AbGroupHom (coHomRedGr n G B) (coHomRedGr n G A)
fst (coHomHom∙ n f) = coHomFun∙ n f
snd (coHomHom∙ n f) =
- makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
+ makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
λ g h → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))
substℕ-coHom : {A : Type ℓ} {G : AbGroup ℓ'} {n m : ℕ}
@@ -416,7 +416,7 @@
→ ((f : A → EM G (suc n)) → f a ≡ 0ₖ (suc n) → B ∣ f ∣₂)
→ (x : coHom (suc n) G A) → B x
coHomPointedElim {ℓ'' = ℓ''} {G = G} {A = A} n a isprop indp =
- ST.elim (λ _ → isOfHLevelSuc 1 (isprop _))
+ ST.elim (λ _ → isOfHLevelSuc 1 (isprop _))
λ f → helper n isprop indp f
where
helper : (n : ℕ) {B : coHom (suc n) G A → Type ℓ''}
@@ -432,9 +432,9 @@
coHomTruncEquiv : {A : Type ℓ} (G : AbGroup ℓ) (n : ℕ)
→ AbGroupEquiv (coHomGr n G (∥ A ∥ (suc (suc n)))) (coHomGr n G A)
fst (coHomTruncEquiv G n) =
- isoToEquiv (setTruncIso (univTrunc (suc (suc n)) {B = _ , hLevelEM G n}))
+ isoToEquiv (setTruncIso (univTrunc (suc (suc n)) {B = _ , hLevelEM G n}))
snd (coHomTruncEquiv G n) =
- makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
+ makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
λ _ _ → refl)
EM→-charac : ∀ {ℓ ℓ'} {A : Pointed ℓ} {G : AbGroup ℓ'} (n : ℕ)
diff --git a/Cubical.Cohomology.EilenbergMacLane.CupProduct.html b/Cubical.Cohomology.EilenbergMacLane.CupProduct.html
index 23f951cc85..e1b2384d72 100644
--- a/Cubical.Cohomology.EilenbergMacLane.CupProduct.html
+++ b/Cubical.Cohomology.EilenbergMacLane.CupProduct.html
@@ -57,51 +57,51 @@
_⌣_ : {n m : ℕ}
→ coHom n G' A → coHom m G' A → coHom (n +' m) G' A
- _⌣_ = ST.rec2 squash₂ λ f g → ∣ (λ x → f x ⌣ₖ g x) ∣₂
+ _⌣_ = ST.rec2 squash₂ λ f g → ∣ (λ x → f x ⌣ₖ g x) ∣₂
⌣-0ₕ : (n m : ℕ) (x : coHom n G' A) → (x ⌣ 0ₕ m) ≡ 0ₕ (n +' m)
⌣-0ₕ n m =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → ⌣ₖ-0ₖ n m (f x))
0ₕ-⌣ : (n m : ℕ) (x : coHom m G' A) → (0ₕ n ⌣ x) ≡ 0ₕ (n +' m)
0ₕ-⌣ n m =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → 0ₖ-⌣ₖ n m (f x))
⌣-1ₕ : (n : ℕ) (x : coHom n G' A)
→ (x ⌣ 1ₕ) ≡ subst (λ n → coHom n G' A) (+'-comm zero n) x
⌣-1ₕ n =
- ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂
+ ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂
(funExt λ x → ⌣ₖ-1ₖ n (f x)
∙ cong (transport (λ i → EM G' (+'-comm zero n i)))
(cong f (sym (transportRefl x))))
1ₕ-⌣ : (n : ℕ) (x : coHom n G' A) → (1ₕ ⌣ x) ≡ x
- 1ₕ-⌣ n = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂
+ 1ₕ-⌣ n = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂
(funExt λ x → 1ₖ-⌣ₖ n (f x))
distrR⌣ : (n m : ℕ) (x y : coHom n G' A) (z : coHom m G' A)
→ ((x +ₕ y) ⌣ z) ≡ (x ⌣ z) +ₕ (y ⌣ z)
distrR⌣ n m =
- ST.elim2 (λ _ _ → isSetΠ (λ _ → isSetPathImplicit))
- λ f g → ST.elim (λ _ → isSetPathImplicit)
+ ST.elim2 (λ _ _ → isSetΠ (λ _ → isSetPathImplicit))
+ λ f g → ST.elim (λ _ → isSetPathImplicit)
λ h → cong ∣_∣₂ (funExt (λ x → distrR⌣ₖ n m (f x) (g x) (h x)))
distrL⌣ : (n m : ℕ) (x : coHom n G' A) (y z : coHom m G' A)
→ (x ⌣ (y +ₕ z)) ≡ (x ⌣ y) +ₕ (x ⌣ z)
distrL⌣ n m =
- ST.elim (λ _ → isSetΠ2 (λ _ _ → isSetPathImplicit))
- λ f → ST.elim2 (λ _ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetΠ2 (λ _ _ → isSetPathImplicit))
+ λ f → ST.elim2 (λ _ _ → isSetPathImplicit)
λ g h → cong ∣_∣₂ (funExt (λ x → distrL⌣ₖ n m (f x) (g x) (h x)))
assoc⌣ : (n m l : ℕ)
(x : coHom n G' A) (y : coHom m G' A) (z : coHom l G' A)
→ ((x ⌣ y) ⌣ z) ≡ subst (λ n → coHom n G' A) (+'-assoc n m l) (x ⌣ (y ⌣ z))
assoc⌣ n m l =
- ST.elim (λ _ → isSetΠ2 (λ _ _ → isSetPathImplicit))
- λ f → ST.elim (λ _ → isSetΠ (λ _ → isSetPathImplicit))
- λ g → ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetΠ2 (λ _ _ → isSetPathImplicit))
+ λ f → ST.elim (λ _ → isSetΠ (λ _ → isSetPathImplicit))
+ λ g → ST.elim (λ _ → isSetPathImplicit)
λ h → cong ∣_∣₂ (funExt λ x → assoc⌣ₖ n m l (f x) (g x) (h x)
∙ cong (transport (λ i → EM G' (+'-assoc n m l i)))
(cong (λ x → (f x ⌣ₖ (g x ⌣ₖ h x))) (sym (transportRefl x))))
@@ -109,20 +109,20 @@
-ₕ^[_·_] : {G' : AbGroup ℓ} {A : Type ℓ'} (n m : ℕ) {k : ℕ}
→ coHom k G' A → coHom k G' A
--ₕ^[ n · m ] = ST.map λ f x → -ₖ^[ n · m ] (f x)
+-ₕ^[ n · m ] = ST.map λ f x → -ₖ^[ n · m ] (f x)
-ₕ^[_·_]-even : {G' : AbGroup ℓ} {A : Type ℓ'} (n m : ℕ) {k : ℕ}
→ isEvenT n ⊎ isEvenT m
→ (x : coHom k G' A) → -ₕ^[ n · m ] x ≡ x
-ₕ^[ n · m ]-even {k = k} p =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → -ₖ^[ n · m ]-even p (f x))
-ₕ^[_·_]-odd : {G' : AbGroup ℓ} {A : Type ℓ'} (n m : ℕ) {k : ℕ}
→ isOddT n × isOddT m
→ (x : coHom k G' A) → -ₕ^[ n · m ] x ≡ -ₕ x
-ₕ^[ n · m ]-odd {k = k} p =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt λ x → -ₖ^[ n · m ]-odd p (f x))
comm⌣ : {G'' : CommRing ℓ} {A : Type ℓ'} (n m : ℕ)
@@ -132,7 +132,7 @@
(+'-comm m n)
(-ₕ^[ n · m ] (y ⌣ x))
comm⌣ {G'' = R} {A = A} n m =
- ST.elim2 (λ _ _ → isSetPathImplicit)
+ ST.elim2 (λ _ _ → isSetPathImplicit)
λ f g →
cong ∣_∣₂ (funExt λ x → ⌣ₖ-comm n m (f x) (g x)
∙ cong (subst (λ n → EM (CommRing→AbGroup R) n) (+'-comm m n))
@@ -184,7 +184,7 @@
where
lem : (x : coHom n ℤ/2 A) (y : coHom m ℤ/2 A)
→ -ₕ^[ n · m ] (y ⌣[ ℤ/2Ring ] x) ≡ (y ⌣ x)
- lem = ST.elim2 (λ _ _ → isSetPathImplicit)
+ lem = ST.elim2 (λ _ _ → isSetPathImplicit)
λ _ _ → cong ∣_∣₂ (funExt λ _ → -ₖ^[ n · m ]-const _)
module _ {G'' : Ring ℓ} {A : Type ℓ'} where
diff --git a/Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod.html b/Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod.html
index 71b7352cc1..3469f4e47b 100644
--- a/Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod.html
+++ b/Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod.html
@@ -67,14 +67,14 @@
compGroupHom (Hmap∙ n g) (Hmap∙ n f)
≡ Hmap∙ n (g ∘∙ f)
compAx (pos n) g f = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
- (funExt (ST.elim (λ _ → isSetPathImplicit)
+ (funExt (ST.elim (λ _ → isSetPathImplicit)
λ a → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)))
compAx (negsuc n) g f = Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl
idAx : (n : ℤ) {A : Pointed ℓ'} →
Hmap∙ n (idfun∙ A) ≡ idGroupHom
idAx (pos n) = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
- (funExt (ST.elim (λ _ → isSetPathImplicit)
+ (funExt (ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (ΣPathP (refl , sym (lUnit (snd f))))))
idAx (negsuc n) = refl
@@ -82,7 +82,7 @@
AbGroupHom (coHomRedℤ G (sucℤ n) (Susp (typ A) , north))
(coHomRedℤ G n A)
fst (suspMap (pos n) {A = A}) =
- ST.map λ f → (λ x → ΩEM+1→EM n
+ ST.map λ f → (λ x → ΩEM+1→EM n
(sym (snd f)
∙∙ cong (fst f) (merid x ∙ sym (merid (pt A)))
∙∙ snd f))
@@ -94,7 +94,7 @@
∙ ΩEM+1→EM-refl n
snd (suspMap (pos n) {A = A}) =
makeIsGroupHom
- (ST.elim2 (λ _ _ → isSetPathImplicit)
+ (ST.elim2 (λ _ _ → isSetPathImplicit)
(λ f g → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
(funExt λ x → main n _ (sym (snd f)) _ (sym (snd g))
(cong (fst f) (merid x ∙ sym (merid (pt A))))
@@ -143,11 +143,11 @@
AbGroupIso (coHomRedℤ G (sucℤ n) (Susp (typ A) , north))
(coHomRedℤ G n A)
fun (fst (suspMapIso n)) = suspMap n .fst
- inv (fst (suspMapIso (pos n))) = ST.map (toSusp-coHomRed n)
+ inv (fst (suspMapIso (pos n))) = ST.map (toSusp-coHomRed n)
inv (fst (suspMapIso (negsuc zero))) _ = 0ₕ∙ zero
inv (fst (suspMapIso (negsuc (suc n)))) _ = tt*
rightInv (fst (suspMapIso (pos n) {A = A})) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
(funExt λ x → cong (ΩEM+1→EM n)
(sym (rUnit _)
@@ -161,7 +161,7 @@
rightInv (fst (suspMapIso (negsuc zero))) tt* = refl
rightInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl
leftInv (fst (suspMapIso (pos n) {A = A})) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
(funExt λ { north → sym (snd f)
; south → sym (snd f) ∙ cong (fst f) (merid (pt A))
@@ -182,7 +182,7 @@
(fst f (compPath-filler (merid a)
(sym (merid (pt A))) (~ i) j))
leftInv (fst (suspMapIso (negsuc zero) {A = A})) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _)
(funExt (suspToPropElim (pt A)
(λ _ → hLevelEM G 0 _ _)
@@ -196,7 +196,7 @@
HMapId (satisfies-ES G) = coHomRedℤ.idAx
fst (Suspension (satisfies-ES G)) n = GroupIso→GroupEquiv (coHomRedℤ.suspMapIso n)
snd (Suspension (satisfies-ES G)) f (pos n) =
- funExt (ST.elim (λ _ → isSetPathImplicit) λ f
+ funExt (ST.elim (λ _ → isSetPathImplicit) λ f
→ cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
(funExt λ { north → refl
; south → refl
@@ -209,22 +209,22 @@
To : (x : coHomRed n G B)
→ isInKer (coHomHom∙ n f) x
→ isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x
- To = ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInIm _ _))
+ To = ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInIm _ _))
λ g p → PT.map (λ id → ∣ (λ { (inl x) → 0ₖ n
; (inr x) → fst g x
; (push a i) → id (~ i) .fst a})
, snd g ∣₂
, cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
refl))
- (Iso.fun ST.PathIdTrunc₀Iso p)
+ (Iso.fun ST.PathIdTrunc₀Iso p)
From : (x : coHomRed n G B)
→ isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x
→ isInKer (coHomHom∙ n f) x
From =
- ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _))
+ ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _))
λ g → PT.rec (isPropIsInKer _ _)
- (uncurry (ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _))
+ (uncurry (ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _))
λ h p → PT.rec (squash₂ _ _)
(λ id → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
(funExt λ x → sym (funExt⁻ (cong fst id) (fst f x))
@@ -232,7 +232,7 @@
∙ push (pt A)
∙ λ i → inr (snd f i))
∙ snd h)))
- (Iso.fun ST.PathIdTrunc₀Iso p)))
+ (Iso.fun ST.PathIdTrunc₀Iso p)))
help : Iso (Ker (coHomHom∙ n f))
(Im (coHomHom∙ n (cfcod (fst f) , refl)))
@@ -253,7 +253,7 @@
Dimension (satisfies-ES G) (pos zero) p = ⊥.rec (p refl)
fst (Dimension (satisfies-ES G) (pos (suc n)) _) = 0ₕ∙ (suc n)
snd (Dimension (satisfies-ES G) (pos (suc n)) _) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → T.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
(λ p → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
(funExt λ { (lift false) → sym p
@@ -267,22 +267,22 @@
where
main : GroupIso _ _
fun (fst main) =
- ST.rec (isSet× squash₂ squash₂)
+ ST.rec (isSet× squash₂ squash₂)
λ f → ∣ f ∘∙ (inl , refl) ∣₂ , ∣ f ∘∙ (inr , sym (push tt)) ∣₂
inv (fst main) =
- uncurry (ST.rec2 squash₂
+ uncurry (ST.rec2 squash₂
λ f g → ∣ (λ { (inl x) → fst f x
; (inr x) → fst g x
; (push a i) → (snd f ∙ sym (snd g)) i})
, snd f ∣₂)
rightInv (fst main) =
uncurry
- (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+ (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
λ f g → ΣPathP
((cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))
, cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)))
leftInv (fst main) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
(funExt λ { (inl x) → refl
; (inr x) → refl
@@ -297,7 +297,7 @@
∙ sym (lUnit q)
snd main =
makeIsGroupHom
- (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+ (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
λ f g → ΣPathP
(cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)
, (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))))
@@ -320,15 +320,15 @@
snd eq = satAC _
mainIso : Iso _ _
- fun mainIso = ST.map λ f i
+ fun mainIso = ST.map λ f i
→ (λ x → f .fst (inr (i , x))) , cong (fst f) (sym (push i)) ∙ snd f
- inv mainIso = ST.map λ f → (λ { (inl x) → 0ₖ n
+ inv mainIso = ST.map λ f → (λ { (inl x) → 0ₖ n
; (inr x) → f (fst x) .fst (snd x)
; (push a i) → f a .snd (~ i)})
, refl
- rightInv mainIso = ST.elim (λ _ → isSetPathImplicit)
+ rightInv mainIso = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt (λ i → ΣPathP (refl , (sym (rUnit (snd (f i)))))))
- leftInv mainIso = ST.elim (λ _ → isSetPathImplicit)
+ leftInv mainIso = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (ΣPathP ((funExt
(λ { (inl x) → sym (snd f)
; (inr x) → refl
@@ -345,7 +345,7 @@
(codomainIsoDep λ i → invIso setTruncTrunc2Iso))
altEquiv≡ : fst altEquiv ≡ _
- altEquiv≡ = funExt (ST.elim (λ _ → isOfHLevelPath 2 (isSetΠ (λ _ → squash₂)) _ _)
+ altEquiv≡ = funExt (ST.elim (λ _ → isOfHLevelPath 2 (isSetΠ (λ _ → squash₂)) _ _)
λ _ → refl)
Wedge (satisfies-ES-gen G) (negsuc n) {I = I} satAC {A = A} =
isoToIsEquiv (iso _ (λ _ → tt*) (λ _ → refl) λ _ → refl)
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html b/Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html
index 65806f6ee7..771ff7a08a 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html
@@ -34,7 +34,7 @@
H⁰→G' : hLevelTrunc 2 A → H⁰A → fst G
H⁰→G' = Trunc.rec (isSetΠ (λ _ → is-set))
- (λ a → ST.rec is-set λ f → f a)
+ (λ a → ST.rec is-set λ f → f a)
H⁰→G'-id : (a : hLevelTrunc 2 A) → H⁰→G' a* ≡ H⁰→G' a
H⁰→G'-id a = cong H⁰→G' (conA .snd a)
@@ -50,8 +50,8 @@
(λ a g i → H⁰→G'-id ∣ a ∣ i (G→H⁰ g)) a*
H⁰→G→H⁰ : (x : H⁰A) → G→H⁰ (H⁰→G x) ≡ x
- H⁰→G→H⁰ = ST.elim (λ _ → isSetPathImplicit) λ f →
- Trunc.rec isSetPathImplicit
+ H⁰→G→H⁰ = ST.elim (λ _ → isSetPathImplicit) λ f →
+ Trunc.rec isSetPathImplicit
(λ a → (λ i → G→H⁰ (H⁰→G'-id ∣ a ∣ₕ i ∣ f ∣₂))
∙ cong ∣_∣₂ (funExt λ x
→ Trunc.rec (is-set _ _)
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle.html b/Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle.html
index a91685949e..7ab0c90251 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle.html
@@ -139,7 +139,7 @@
H¹K²→ℤ/2×ℤ/2 : coHom 1 ℤ/2 KleinBottle → fst (dirProdAb ℤ/2 ℤ/2)
-H¹K²→ℤ/2×ℤ/2 = ST.rec (is-set (snd (dirProdAb ℤ/2 ℤ/2)))
+H¹K²→ℤ/2×ℤ/2 = ST.rec (is-set (snd (dirProdAb ℤ/2 ℤ/2)))
λ f → ΩEM+1→EM-gen _ _ (cong f line1)
, ΩEM+1→EM-gen _ _ (cong f line2)
@@ -181,7 +181,7 @@
H¹K²→ℤ/2×ℤ/2→H¹K² : (x : _)
→ ℤ/2×ℤ/2→H¹K² (H¹K²→ℤ/2×ℤ/2 x) ≡ x
H¹K²→ℤ/2×ℤ/2→H¹K² =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
(ConnK².elim₁ (isConnectedEM 1) (λ _ → squash₂ _ _) embase
λ l1 l2 sq → cong ∣_∣₂ (funExt (elimSet (λ _ → hLevelEM _ 1 _ _) refl
(flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 0) l1))
@@ -268,7 +268,7 @@
H²K²→ℤ/2 : coHom 2 ℤ/2 KleinBottle → fst ℤ/2
H²K²→ℤ/2 =
- ST.rec isSetFin
+ ST.rec isSetFin
λ f → H²K²→ℤ/2₂ (H²K²→ℤ/2₁ f)
@@ -278,7 +278,7 @@
H²K²→ℤ/2→H²K² : (f : coHom 2 ℤ/2 KleinBottle) → ℤ/2→H²K² (H²K²→ℤ/2 f) ≡ f
H²K²→ℤ/2→H²K² =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
(ConnK².elim₂ (isConnectedEM 2) (λ _ → squash₂ _ _) ∣ north ∣
λ sq → cong ℤ/2→H²K² (H²K²→ℤ/2-rewrite sq)
∙ cong ∣_∣₂ (funExt
@@ -316,14 +316,14 @@
Iso.leftInv is = H²K²→ℤ/2→H²K²
snd H²[K²,ℤ/2]≅ℤ/2 =
Isoℤ/2-morph (fst H²[K²,ℤ/2]≅ℤ/2) (0ₕ 2) (sym H²K²→ℤ/2-pres0) _+ₕ_ (-ₕ_)
- (funExt (ST.elim (λ _ → isSetPathImplicit)
+ (funExt (ST.elim (λ _ → isSetPathImplicit)
(λ f → cong ∣_∣₂ (funExt λ x → sym (-ₖConst-ℤ/2 1 (f x))))))
(AbGroupStr.isAbGroup (coHomGr 2 ℤ/2 KleinBottle .snd))
isContr-HⁿKleinBottle : (n : ℕ) (G : AbGroup ℓ)
→ isContr (coHom (suc (suc (suc n))) G KleinBottle)
fst (isContr-HⁿKleinBottle n G) = ∣ (KleinFun ∣ north ∣ refl refl refl) ∣₂
-snd (isContr-HⁿKleinBottle n G) = ST.elim (λ _ → isSetPathImplicit)
+snd (isContr-HⁿKleinBottle n G) = ST.elim (λ _ → isSetPathImplicit)
(ConnK².elim₂ (isConnectedSubtr 3 (suc n)
(subst (λ m → isConnected m (EM G (3 +ℕ n)))
(cong suc (+-comm 3 n))
@@ -387,21 +387,21 @@
mainIso : Iso (coHom 1 G KleinBottle) (fst G × coHom 1 G RP²)
Iso.fun mainIso =
- ST.rec (isSet× (is-set (snd G)) squash₂)
+ ST.rec (isSet× (is-set (snd G)) squash₂)
λ f → (ΩEM+1→EM-gen 0 _ (cong f line2)) , ∣ F→ f ∣₂
- Iso.inv mainIso = uncurry λ g → ST.map (F← g)
+ Iso.inv mainIso = uncurry λ g → ST.map (F← g)
Iso.rightInv mainIso = uncurry λ g
- → ST.elim (λ _ → isOfHLevelPath 2 (isSet× (is-set (snd G)) squash₂) _ _)
+ → ST.elim (λ _ → isOfHLevelPath 2 (isSet× (is-set (snd G)) squash₂) _ _)
λ f → ΣPathP ((Iso.leftInv (Iso-EM-ΩEM+1-gen 0 (f point)) g)
, cong ∣_∣₂ (funExt (elimSetRP² (λ _ → hLevelEM G 1 _ _)
refl λ i j → f (line i))))
- Iso.leftInv mainIso = ST.elim (λ _ → isSetPathImplicit)
+ Iso.leftInv mainIso = ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt (elimSet (λ _ → hLevelEM G 1 _ _)
refl
(λ i j → f (line1 i))
(flipSquare (Iso.rightInv (Iso-EM-ΩEM+1-gen 0 (f point)) (cong f line2)))))
snd (H¹[K²,G]≅G×H¹[RP²,G] G) =
- makeIsGroupHom (ST.elim2
+ makeIsGroupHom (ST.elim2
(λ _ _ → isOfHLevelPath 2 lem _ _)
(ConnK².elim₁ (isConnectedEM 1) (λ _ → isPropΠ λ _ → lem _ _) embase
λ p1 q1 r1
@@ -439,30 +439,30 @@
Σ[ q ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] Square (sym p) p q q) ∥₂
∥ (Σ[ x ∈ EM G (2 +ℕ n) ] (Σ[ p ∈ Ω (EM G (2 +ℕ n) , x) .fst ]
Σ[ q ∈ Ω (EM G (2 +ℕ n) , x) .fst ] Square (sym p) p q q)) ∥₂
- Iso.fun (H²K²-helperIso₁ G n) = ST.map (0ₖ _ ,_)
- Iso.inv (H²K²-helperIso₁ G n) = ST.rec squash₂
+ Iso.fun (H²K²-helperIso₁ G n) = ST.map (0ₖ _ ,_)
+ Iso.inv (H²K²-helperIso₁ G n) = ST.rec squash₂
(uncurry (EM-raw'-elim G (2 +ℕ n)
(λ _ → isOfHLevelΠ (3 +ℕ n) λ _ → isOfHLevelPlus' {n = suc n} 2 squash₂)
(EM-raw'-trivElim G (suc n) (λ _
→ isOfHLevelΠ (2 +ℕ n) λ _ → isOfHLevelPlus' {n = n} 2 squash₂)
∣_∣₂)))
- Iso.rightInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit)
+ Iso.rightInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit)
(uncurry (EM-raw'-elim G (2 +ℕ n)
(λ _ → isOfHLevelΠ (3 +ℕ n)
λ _ → isOfHLevelPlus' {n = suc (suc n)} 1 (squash₂ _ _))
(EM-raw'-trivElim G (suc n) (λ _ → isOfHLevelΠ (2 +ℕ n)
λ _ → isOfHLevelPlus' {n = suc n} 1 (squash₂ _ _))
λ _ → refl)))
- Iso.leftInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl
+ Iso.leftInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl
H²K²-helperIso₂ : (G : AbGroup ℓ) (n : ℕ) →
Iso ∥ (Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ]
Σ[ q ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] Square (sym p) p q q) ∥₂
∥ ((Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ]
p ≡ sym p)) ∥₂
- Iso.fun (H²K²-helperIso₂ G n) = ST.map (H²K²-helperFun₁ G n)
- Iso.inv (H²K²-helperIso₂ G n) = ST.map (λ p → fst p , refl , sym (snd p))
- Iso.rightInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) λ {(p , r)
+ Iso.fun (H²K²-helperIso₂ G n) = ST.map (H²K²-helperFun₁ G n)
+ Iso.inv (H²K²-helperIso₂ G n) = ST.map (λ p → fst p , refl , sym (snd p))
+ Iso.rightInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) λ {(p , r)
→ TR.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
(λ { P → cong ∣_∣₂ (main p P r)})
((F p .fst))}
@@ -474,7 +474,7 @@
→ H²K²-helperFun₁ G n (p , refl , sym r) ≡ (p , r)
main = (J> λ r → (ΣPathP (refl , sym (rUnit _)
∙ λ i j k → rUnitₖ (suc (suc n)) (r j k) i)))
- Iso.leftInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit)
+ Iso.leftInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit)
(uncurry λ p → TR.rec (isProp→isOfHLevelSuc n (isPropΠ (λ _ → squash₂ _ _ )))
(λ P → uncurry λ q → TR.rec (isProp→isOfHLevelSuc n (isPropΠ (λ _ → squash₂ _ _ )))
(λ Q x → cong ∣_∣₂ (main p P q Q x))
@@ -499,24 +499,24 @@
(coHom (2 +ℕ n) G RP²)
Iso-H²⁺ⁿ[K²,G]-H²⁺ⁿ[RP²,G] G n =
compIso
- (setTruncIso
+ (setTruncIso
(compIso K²FunCharacIso
(Σ-cong-iso-snd λ p → Σ-cong-iso-snd λ q
→ Σ-cong-iso-snd λ r → equivToIso flipSquareEquiv)))
(compIso (invIso (H²K²-helperIso₁ G n))
(compIso (H²K²-helperIso₂ G n)
(compIso (invIso (killFirstCompIsoGen G n))
- (setTruncIso (invIso RP²FunCharacIso)))))
+ (setTruncIso (invIso RP²FunCharacIso)))))
H²[RP²,G]≅H²[K²,G] : (G : AbGroup ℓ)
→ AbGroupEquiv (coHomGr 2 G RP²) (coHomGr 2 G KleinBottle)
fst (H²[RP²,G]≅H²[K²,G] G) = isoToEquiv (invIso (Iso-H²⁺ⁿ[K²,G]-H²⁺ⁿ[RP²,G] G 0))
snd (H²[RP²,G]≅H²[K²,G] G) =
- makeIsGroupHom (ST.elim (λ _ → isSetΠ λ _ → isSetPathImplicit)
+ makeIsGroupHom (ST.elim (λ _ → isSetΠ λ _ → isSetPathImplicit)
(RP²Conn.elim₂ (isConnectedEM 2)
(λ _ → isPropΠ λ _ → squash₂ _ _)
(0ₖ 2)
- λ p → ST.elim (λ _ → isSetPathImplicit)
+ λ p → ST.elim (λ _ → isSetPathImplicit)
(RP²Conn.elim₂ (isConnectedEM 2)
(λ _ → squash₂ _ _)
(0ₖ 2) λ q
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.RP2.html b/Cubical.Cohomology.EilenbergMacLane.Groups.RP2.html
index 937437fd84..dadb8489f4 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.RP2.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.RP2.html
@@ -130,7 +130,7 @@
H¹[RP²,ℤ/2]→ℤ/2 : coHom 1 ℤ/2 RP² → fst ℤ/2
H¹[RP²,ℤ/2]→ℤ/2 =
- ST.rec isSetFin
+ ST.rec isSetFin
λ f → ΩEM+1→EM-gen 0 _ (cong f line)
ℤ/2→H¹[RP²,ℤ/2] : fst ℤ/2 → coHom 1 ℤ/2 RP²
@@ -146,8 +146,8 @@
H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2] : (f : coHom 1 ℤ/2 RP²)
→ ℤ/2→H¹[RP²,ℤ/2] (H¹[RP²,ℤ/2]→ℤ/2 f) ≡ f
H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2] =
- ST.elim
- (λ _ → isSetPathImplicit)
+ ST.elim
+ (λ _ → isSetPathImplicit)
(RP²Conn.elim₁ (isConnectedEM 1)
(λ _ → squash₂ _ _)
embase
@@ -177,7 +177,7 @@
H²[RP²,ℤ/2]→ℤ/2 : coHom 2 ℤ/2 RP² → fst ℤ/2
H²[RP²,ℤ/2]→ℤ/2 =
- ST.rec isSetFin
+ ST.rec isSetFin
λ f → ΩEM+1→EM-gen 0 _
(cong (ΩEM+1→EM-gen 1 _)
((cong (cong f) square ∙ symConst-ℤ/2 2 _ (sym (cong f line)))))
@@ -203,7 +203,7 @@
H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] : (x : coHom 2 ℤ/2 RP²)
→ ℤ/2→H²[RP²,ℤ/2] (H²[RP²,ℤ/2]→ℤ/2 x) ≡ x
H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
(RP²Conn.elim₂
(isConnectedEM 2)
(λ _ → squash₂ _ _)
@@ -226,7 +226,7 @@
_ (sym (H²[RP²,ℤ/2]→ℤ/2-Id refl)
∙ cong (H²[RP²,ℤ/2]→ℤ/2 ∘ ∣_∣₂)
(characRP²Fun (λ _ → 0ₖ 2)))
- _ _ (funExt (ST.elim (λ _ → isSetPathImplicit)
+ _ _ (funExt (ST.elim (λ _ → isSetPathImplicit)
λ f → cong ∣_∣₂ (funExt
λ x → sym (-ₖConst-ℤ/2 1 (f x))))) _
@@ -237,7 +237,7 @@
fst (H³⁺ⁿ[RP²,G]≅G n G) =
isoToEquiv (isContr→Iso
(∣ RP²Fun (0ₖ (3 +ℕ n)) refl refl ∣₂
- , (ST.elim (λ _ → isSetPathImplicit)
+ , (ST.elim (λ _ → isSetPathImplicit)
(RP²Conn.elim₃
(isConnectedSubtr 4 n
(subst (λ x → isConnected x (EM G (3 +ℕ n)))
@@ -272,7 +272,7 @@
H¹[RP²,G]→G[2] : coHom 1 G RP² → (G [ 2 ]ₜ) .fst
H¹[RP²,G]→G[2] =
- ST.rec (is-set (snd (G [ 2 ]ₜ)))
+ ST.rec (is-set (snd (G [ 2 ]ₜ)))
λ f → ΩEM+1→EM-gen {G = G} 0 (f point) (cong f line)
, cong (_+_ (snd G) (ΩEM+1→EM-gen 0 (f point) (cong f line)))
(+IdR (snd G) _)
@@ -300,7 +300,7 @@
Iso.rightInv is (g , p) =
Σ≡Prop (λ _ → is-set (snd G) _ _)
(Iso.leftInv (Iso-EM-ΩEM+1 0) g)
- Iso.leftInv is = ST.elim (λ _ → isSetPathImplicit)
+ Iso.leftInv is = ST.elim (λ _ → isSetPathImplicit)
(RP²Conn.elim₁ (isConnectedEM 1) (λ _ → squash₂ _ _)
embase
λ p q → cong ∣_∣₂
@@ -344,15 +344,15 @@
→ Iso ∥ (Σ[ x ∈ EM G (2 +ℕ n) ] (Σ[ p ∈ x ≡ x ] p ≡ sym p)) ∥₂
∥ (Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] p ≡ sym p) ∥₂
Iso.fun (killFirstCompIsoGen n) =
- ST.rec squash₂
+ ST.rec squash₂
(uncurry (TR.elim (λ _ → isOfHLevelPlus {n = 2 +ℕ n} 2
(isOfHLevelPlus' {n = n} 2 (isSetΠ λ _ → squash₂)))
(EM-raw'-trivElim G (suc n)
(λ _ → isOfHLevelΠ (suc (suc n))
λ _ → isOfHLevelPlus' {n = n} 2 squash₂) ∣_∣₂)))
- Iso.inv (killFirstCompIsoGen n) = ST.map (0ₖ (2 +ℕ n) ,_)
- Iso.rightInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl
- Iso.leftInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit)
+ Iso.inv (killFirstCompIsoGen n) = ST.map (0ₖ (2 +ℕ n) ,_)
+ Iso.rightInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl
+ Iso.leftInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit)
(uncurry (TR.elim (λ _ → isProp→isOfHLevelSuc (3 +ℕ n)
(isPropΠ (λ _ → squash₂ _ _)))
(EM-raw'-trivElim G (suc n) (λ _ → isProp→isOfHLevelSuc (suc n)
@@ -360,7 +360,7 @@
λ _ → refl)))
H²RP²-Iso₁ : Iso (coHom 2 G RP²) ∥ (Σ[ p ∈ Ω (EM∙ G 2) .fst ] p ≡ sym p) ∥₂
- H²RP²-Iso₁ = compIso (setTruncIso RP²FunCharacIso) (killFirstCompIsoGen 0)
+ H²RP²-Iso₁ = compIso (setTruncIso RP²FunCharacIso) (killFirstCompIsoGen 0)
H²RP²-Iso₂ : Iso ((Σ[ p ∈ Ω (EM∙ G 2) .fst ] p ≡ sym p)) (Σ[ p ∈ EM G 1 ] p ≡ -ₖ p)
H²RP²-Iso₂ = (Σ-cong-iso (invIso (Iso-EM-ΩEM+1 1))
@@ -406,16 +406,16 @@
(((sym≡flipSquare p) ∙ flipSquare≡cong-sym p) j k r))
H²RP²-Iso₁,₂-charac : (p : (Ω^ 2) (EM∙ G 2) .fst)
- → ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁ ∣ RP²Fun _ _ p ∣₂)
+ → ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁ ∣ RP²Fun _ _ p ∣₂)
≡ ∣ embase , (cong (ΩEM+1→EM 1) p) ∣₂
H²RP²-Iso₁,₂-charac p = cong ∣_∣₂ (ΣPathP (refl
, (λ i → cong (ΩEM+1→EM {G = G} 1) p ∙ ΩEM+1→EM-sym'-refl i)
∙ sym (rUnit (cong (ΩEM+1→EM 1) p))))
H²RP²-Iso₁,₂+ : (p q : (Ω^ 2) (EM∙ G 2) .fst)
- → ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁ (∣ RP²Fun _ _ p ∣₂ +ₕ ∣ RP²Fun _ _ q ∣₂))
+ → ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁ (∣ RP²Fun _ _ p ∣₂ +ₕ ∣ RP²Fun _ _ q ∣₂))
≡ ∣ embase , cong (ΩEM+1→EM 1) p ∙ cong (ΩEM+1→EM 1) q ∣₂
- H²RP²-Iso₁,₂+ p q = cong (ST.map (Iso.fun H²RP²-Iso₂) ∘ Iso.fun H²RP²-Iso₁)
+ H²RP²-Iso₁,₂+ p q = cong (ST.map (Iso.fun H²RP²-Iso₂) ∘ Iso.fun H²RP²-Iso₁)
(cong ∣_∣₂ (funExt (RP²Fun-pres+ p q)))
∙ H²RP²-Iso₁,₂-charac (p ∙ q)
∙ cong ∣_∣₂ (ΣPathP (refl , cong-∙ (ΩEM+1→EM 1) p q))
@@ -442,7 +442,7 @@
∙ +Assoc (snd G) _ _ _ ∣₁)
H²RP²-Iso₃ : Iso ∥ (Σ[ p ∈ EM G 1 ] p ≡ -ₖ p) ∥₂ (fst (G /^ 2))
- Iso.fun H²RP²-Iso₃ = ST.rec squash/ (uncurry H²RP²-Iso₃→)
+ Iso.fun H²RP²-Iso₃ = ST.rec squash/ (uncurry H²RP²-Iso₃→)
Iso.inv H²RP²-Iso₃ =
SQ.elim (λ _ → squash₂) (λ a → ∣ embase , emloop a ∣₂)
λ a b → PT.rec (squash₂ _ _)
@@ -467,7 +467,7 @@
∙ +IdR (snd G) b)))))
Iso.rightInv H²RP²-Iso₃ = SQ.elimProp (λ _ → squash/ _ _)
λ a → cong [_] (Iso.leftInv (Iso-EM-ΩEM+1 0) a)
- Iso.leftInv H²RP²-Iso₃ = ST.elim (λ _ → isSetPathImplicit)
+ Iso.leftInv H²RP²-Iso₃ = ST.elim (λ _ → isSetPathImplicit)
(uncurry (EM1.elimProp (AbGroup→Group G) (λ _ → isPropΠ λ _ → squash₂ _ _)
λ p → cong ∣_∣₂ (ΣPathP (refl , (Iso.rightInv (Iso-EM-ΩEM+1 0) p)))))
@@ -475,9 +475,9 @@
fst H²[RP²,G]≅G/2 = isoToEquiv is
where
is : Iso _ _
- is = compIso (compIso H²RP²-Iso₁ (setTruncIso H²RP²-Iso₂)) H²RP²-Iso₃
+ is = compIso (compIso H²RP²-Iso₁ (setTruncIso H²RP²-Iso₂)) H²RP²-Iso₃
snd H²[RP²,G]≅G/2 =
- makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash/ _ _)
+ makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash/ _ _)
(RP²Conn.elim₂ (isConnectedEM 2) (λ _ → isPropΠ λ _ → squash/ _ _)
(0ₖ 2) λ p → RP²Conn.elim₂ (isConnectedEM 2) (λ _ → squash/ _ _)
(0ₖ 2) λ q → cong (Iso.fun H²RP²-Iso₃) (H²RP²-Iso₁,₂+ p q)
@@ -489,7 +489,7 @@
H³⁺ⁿ[RP²,G]≅0 : (n : ℕ) → AbGroupEquiv (coHomGr (3 +ℕ n) G RP²) (trivialAbGroup {ℓ})
fst (H³⁺ⁿ[RP²,G]≅0 n) = isContr→≃Unit* (0ₕ _
- , ST.elim (λ _ → isSetPathImplicit)
+ , ST.elim (λ _ → isSetPathImplicit)
(RP²Conn.elim₃ (isConnectedSubtr 4 n
(subst (λ k → isConnected k (EM G (3 +ℕ n)))
(+-comm 4 n) (isConnectedEM (3 +ℕ n))))
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.RPinf.html b/Cubical.Cohomology.EilenbergMacLane.Groups.RPinf.html
index 460fbca8b1..f96b0a945b 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.RPinf.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.RPinf.html
@@ -234,15 +234,15 @@
help = equivToIso (invEquiv (⌣RP∞''Equiv n))
∥EM-ℤ/2ˣ∥₀-Iso : (n : ℕ) → Iso ∥ EM ℤ/2 ˣ n ∥₂ (fst ℤ/2)
-∥EM-ℤ/2ˣ∥₀-Iso zero = setTruncIdempotentIso (is-set (snd ℤ/2Ring))
+∥EM-ℤ/2ˣ∥₀-Iso zero = setTruncIdempotentIso (is-set (snd ℤ/2Ring))
∥EM-ℤ/2ˣ∥₀-Iso (suc n) =
compIso
(compIso
- setTruncOfProdIso
+ setTruncOfProdIso
(compIso (Σ-cong-iso-snd λ _
→ equivToIso
(isContr→≃Unit (∣ 0ₖ (suc n) ∣₂
- , ST.elim (λ _ → isSetPathImplicit)
+ , ST.elim (λ _ → isSetPathImplicit)
(EM→Prop _ _ (λ _ → squash₂ _ _) refl))))
rUnit×Iso))
(∥EM-ℤ/2ˣ∥₀-Iso n)
@@ -254,7 +254,7 @@
∙ subst-EM∙ (+'-suc₁ n) .snd)
cohomRP∞Iso : (n : ℕ) → Iso (coHom n ℤ/2 (EM ℤ/2 1)) (ℤ/2 .fst)
-cohomRP∞Iso n = compIso (setTruncIso (RP→EM-ℤ/2-CharacIso n)) (∥EM-ℤ/2ˣ∥₀-Iso n)
+cohomRP∞Iso n = compIso (setTruncIso (RP→EM-ℤ/2-CharacIso n)) (∥EM-ℤ/2ˣ∥₀-Iso n)
RP→EM-ℤ/2-CharacIso∙ : (n : ℕ)
→ Iso.fun (RP→EM-ℤ/2-CharacIso n) (λ _ → 0ₖ n) ≡ EM-ℤ/2ˣ∙ n
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html b/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html
index c4deecf5e3..ecb1f9a671 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html
@@ -99,7 +99,7 @@
module _ (G : AbGroup ℓ) where
open AbGroupStr (snd G) renaming (is-set to is-setG)
H¹S¹→G : coHom 1 G S¹ → fst G
- H¹S¹→G = ST.rec is-setG λ f → ΩEM+1→EM-gen 0 (f base) (cong f loop)
+ H¹S¹→G = ST.rec is-setG λ f → ΩEM+1→EM-gen 0 (f base) (cong f loop)
G→H¹S¹ : fst G → coHom 1 G S¹
G→H¹S¹ g = ∣ S¹fun (0ₖ 1) (emloop g) ∣₂
@@ -112,7 +112,7 @@
Iso.inv is = G→H¹S¹
Iso.rightInv is = Iso.leftInv (Iso-EM-ΩEM+1 0)
Iso.leftInv is =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
(S¹-connElim (isConnectedEM 1) (λ _ → squash₂ _ _)
embase
λ p → cong ∣_∣₂ (cong (S¹fun embase) (Iso.rightInv (Iso-EM-ΩEM+1 0) p)))
@@ -125,7 +125,7 @@
HⁿSⁿ↓ : (n : ℕ) → coHom (suc (suc n)) G (S₊ (suc (suc n)))
→ coHom (suc n) G (S₊ (suc n))
- HⁿSⁿ↓ n = ST.map λ f x → ΩEM+1→EM-gen (suc n) _ (cong f (toSusp (S₊∙ (suc n)) x))
+ HⁿSⁿ↓ n = ST.map λ f x → ΩEM+1→EM-gen (suc n) _ (cong f (toSusp (S₊∙ (suc n)) x))
private
liftMap : (n : ℕ) (f : S₊ (suc n) → EM G (suc n))
@@ -134,7 +134,7 @@
HⁿSⁿ↑ : (n : ℕ) → coHom (suc n) G (S₊ (suc n))
→ coHom (suc (suc n)) G (S₊ (suc (suc n)))
- HⁿSⁿ↑ n = ST.map (liftMap n)
+ HⁿSⁿ↑ n = ST.map (liftMap n)
Hⁿ[Sⁿ,G]≅Hⁿ⁺¹[Sⁿ⁺¹,G] : (n : ℕ)
→ AbGroupEquiv (coHomGr (suc n) G (S₊ (suc n)))
@@ -145,7 +145,7 @@
Iso.fun is = HⁿSⁿ↑ n
Iso.inv is = HⁿSⁿ↓ n
Iso.rightInv is =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
(Sⁿ-connElim n (isConnectedSubtr 2 (suc n)
(subst (λ x → isConnected x (EM G (suc (suc n))))
(cong suc (+-comm 2 n)) (isConnectedEM (suc (suc n)))))
@@ -165,7 +165,7 @@
(isConnectedPath (suc (suc n))
(isConnectedEM (suc (suc n))) _ _)
(p (ptSn _)) refl .fst))
- Iso.leftInv is = ST.elim (λ _ → isSetPathImplicit)
+ Iso.leftInv is = ST.elim (λ _ → isSetPathImplicit)
λ f → TR.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
(λ q → cong ∣_∣₂ (funExt λ x
→ cong (ΩEM+1→EM (suc n))
@@ -180,7 +180,7 @@
(f (ptSn (suc n))) (0ₖ (suc n)) .fst)
snd (Hⁿ[Sⁿ,G]≅Hⁿ⁺¹[Sⁿ⁺¹,G] n) =
makeIsGroupHom
- (ST.elim2 (λ _ _ → isSetPathImplicit)
+ (ST.elim2 (λ _ _ → isSetPathImplicit)
λ f g → cong ∣_∣₂
(funExt λ { north → refl
; south → refl
@@ -199,7 +199,7 @@
→ isContr (coHom ((suc m) +ℕ suc n) G (S₊ (suc n)))
fst (isContr-Hᵐ⁺ⁿ[Sⁿ,G] zero m) = 0ₕ _
snd (isContr-Hᵐ⁺ⁿ[Sⁿ,G] zero m) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
(S¹-connElim
(isConnectedSubtr 2 (suc m)
(subst (λ x → isConnected x (EM G (suc (m +ℕ 1))))
@@ -215,7 +215,7 @@
(isConnectedEM (suc (m +ℕ 1))) _ _) refl p .fst))
fst (isContr-Hᵐ⁺ⁿ[Sⁿ,G] (suc n) m) = 0ₕ _
snd (isContr-Hᵐ⁺ⁿ[Sⁿ,G] (suc n) m) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
(Sⁿ-connElim n
(isConnectedSubtr 2 (suc (suc m) +ℕ n)
(subst (λ x → isConnected x (EM G (suc (m +ℕ suc (suc n)))))
@@ -227,7 +227,7 @@
λ p → PT.rec (squash₂ _ _)
(λ q → cong ∣_∣₂ (sym (characSⁿFun n (λ _ → 0ₖ _))
∙ cong (SⁿFun n (0ₖ (suc (m +ℕ suc (suc n))))) q))
- (Iso.fun PathIdTrunc₀Iso
+ (Iso.fun PathIdTrunc₀Iso
(isContr→isProp
(subst (λ A → isContr ∥ (S₊ (suc n) → A) ∥₂)
(cong (EM G) (sym (+-suc m (suc n)))
@@ -254,7 +254,7 @@
isoToEquiv
(isContr→Iso
((0ₕ _)
- , (ST.elim (λ _ → isSetPathImplicit)
+ , (ST.elim (λ _ → isSetPathImplicit)
(subst (λ x → (a : S₊ x → EM G 1) → 0ₕ 1 ≡ ∣ a ∣₂)
(cong suc (+-comm 1 m))
λ f → TR.rec (squash₂ _ _)
@@ -269,7 +269,7 @@
isoToEquiv
(isContr→Iso
((0ₕ _)
- , ST.elim (λ _ → isSetPathImplicit)
+ , ST.elim (λ _ → isSetPathImplicit)
(subst (λ x → (a : S₊ x → EM G (suc (suc n)))
→ 0ₕ (suc (suc n)) ≡ ∣ a ∣₂)
(cong suc (cong suc (sym (+-suc m n))
@@ -357,7 +357,7 @@
compEquiv
(invEquiv
(compEquiv (fst (coHom≅coHomRed n G (S₊∙ (suc n))))
- (isoToEquiv (setTruncIdempotentIso (isSet-Sn→∙EM G (suc n))))))
+ (isoToEquiv (setTruncIdempotentIso (isSet-Sn→∙EM G (suc n))))))
(fst (Hⁿ[Sⁿ,G]≅G G n))
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.Torus.html b/Cubical.Cohomology.EilenbergMacLane.Groups.Torus.html
index 13a33ca05c..4751e3d090 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.Torus.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.Torus.html
@@ -153,12 +153,12 @@
_+1_ = _+ₖ_ {G = G} {n = 1}
typIso : Iso _ _
- Iso.fun typIso = ST.rec (isSet× squash₂ squash₂)
+ Iso.fun typIso = ST.rec (isSet× squash₂ squash₂)
λ f → ∣ (λ x → f (x , base)) ∣₂ , ∣ (λ x → f (base , x)) ∣₂
- Iso.inv typIso = uncurry (ST.rec2 squash₂
+ Iso.inv typIso = uncurry (ST.rec2 squash₂
λ f g → ∣ (λ x → f (fst x) +1 g (snd x)) ∣₂)
Iso.rightInv typIso =
- uncurry (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+ uncurry (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
(S¹-connElim (isConnectedEM {G' = G} 1)
(λ _ → isPropΠ λ _ → isSet× squash₂ squash₂ _ _)
(0ₖ {G = G} 1)
@@ -176,8 +176,8 @@
theIso : AbGroupIso (AbDirProd (coHomGr 1 G S¹) (coHomGr 1 G S¹)) (coHomGr 1 G (S¹ × S¹))
fst theIso = invIso typIso
snd theIso = makeIsGroupHom
- (uncurry (ST.elim2 (λ _ _ → isSetΠ λ _ → isSetPathImplicit)
- λ f1 g1 → uncurry (ST.elim2 (λ _ _ → isSetPathImplicit)
+ (uncurry (ST.elim2 (λ _ _ → isSetΠ λ _ → isSetPathImplicit)
+ λ f1 g1 → uncurry (ST.elim2 (λ _ _ → isSetPathImplicit)
λ f2 g2 → cong ∣_∣₂ (funExt λ {(x , y)
→ move4 (f1 x) (f2 x) (g1 y) (g2 y) _+1_ (assocₖ {G = G} 1) (commₖ {G = G} 1)}))))
@@ -198,9 +198,9 @@
(Σ-cong-iso-snd λ t → invIso (Iso-EM-ΩEM+1-gen {G = G} 1 t))
is : Iso _ _
- is = compIso (setTruncIso (compIso curryIso
+ is = compIso (setTruncIso (compIso curryIso
(compIso (codomainIso is1) toProdIso)))
- (compIso setTruncOfProdIso
+ (compIso setTruncOfProdIso
(compIso (prodIso
(equivToIso (fst (Hᵐ⁺ⁿ[Sⁿ,G]≅0 G 0 0))) idIso)
lUnit*×Iso))
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.Unit.html b/Cubical.Cohomology.EilenbergMacLane.Groups.Unit.html
index 868456a8f0..5ddb9e46e5 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.Unit.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.Unit.html
@@ -37,7 +37,7 @@
→ isContr (coHom (suc n) G Unit)
fst (isContr-Hⁿ⁺¹[Unit,G] {G = G} n) = 0ₕ (suc n)
snd (isContr-Hⁿ⁺¹[Unit,G] {G = G} n) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → Trunc.rec
(isProp→isOfHLevelSuc n (squash₂ _ _))
(λ p → cong ∣_∣₂ (funExt λ _ → p))
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html b/Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html
index 91f8f308c7..a4c243f3f8 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html
@@ -62,12 +62,12 @@
(coHom (suc n) G (fst A)
× coHom (suc n) G (fst B))
Iso.fun (Hⁿ⋁-Iso n) =
- ST.rec (isSet× squash₂ squash₂)
+ ST.rec (isSet× squash₂ squash₂)
λ f → ∣ f ∘ inl ∣₂ , ∣ f ∘ inr ∣₂
Iso.inv (Hⁿ⋁-Iso n) =
- uncurry (ST.rec2 squash₂ λ f g → ∣ Hⁿ-⋁→Hⁿ× n f g ∣₂)
+ uncurry (ST.rec2 squash₂ λ f g → ∣ Hⁿ-⋁→Hⁿ× n f g ∣₂)
Iso.rightInv (Hⁿ⋁-Iso n) =
- uncurry (ST.elim2
+ uncurry (ST.elim2
(λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
λ f g
→ ΣPathP (Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
@@ -83,7 +83,7 @@
(isConnectedPath (suc n)
(isConnectedEM (suc n)) (g (pt B)) (0ₖ (suc n)) .fst)))
Iso.leftInv (Hⁿ⋁-Iso n) =
- ST.elim (λ _ → isSetPathImplicit)
+ ST.elim (λ _ → isSetPathImplicit)
λ f → Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
(λ p → cong ∣_∣₂
(funExt λ { (inl x) → pgen f p (inl x)
@@ -133,6 +133,6 @@
fst (Hⁿ-⋁≅Hⁿ×Hⁿ n) = isoToEquiv (Hⁿ⋁-Iso n)
snd (Hⁿ-⋁≅Hⁿ×Hⁿ n) =
makeIsGroupHom
- (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+ (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
λ f g → refl)