diff --git a/Cubical.CW.Approximation.html b/Cubical.CW.Approximation.html
index 7bf7b2eb2..8cf8eecdb 100644
--- a/Cubical.CW.Approximation.html
+++ b/Cubical.CW.Approximation.html
@@ -147,7 +147,7 @@
invEq propTrunc≃Trunc1
(invEq (_ , InductiveFinSatAC 1 (CWskel-fields.card C (suc m)) _)
λ a → fst propTrunc≃Trunc1
- (sphereToTrunc m λ y →
+ (sphereToTrunc m λ y →
TR.map fst (isConnectedCong _ _ (isConnected-CW↪∞ (suc (suc m)) D)
(sym (push _)
∙ (fh (CWskel-fields.α C (suc m) (a , y))
@@ -191,8 +191,8 @@
(fib-f-r x)) ∥₁
mere-fib-f-coh = invEq propTrunc≃Trunc1
(invEq (_ , InductiveFinSatAC 1 (card (suc m)) _)
- λ a → fst propTrunc≃Trunc1 (sphereToTrunc m
- (sphereElim' m
+ λ a → fst propTrunc≃Trunc1 (sphereToTrunc m
+ (sphereElim' m
(λ x → isOfHLevelRetractFromIso m
(invIso (PathPIdTruncIso (suc m)))
(isOfHLevelPathP' m (isProp→isOfHLevelSuc m
@@ -521,7 +521,7 @@
Iso.inv propTruncTrunc1Iso
(invEq (_ , InductiveFinSatAC 1 _ _)
λ x → Iso.fun propTruncTrunc1Iso
- (sphereToTrunc n' (fiber-cong²-hₙ₊₁-push∞ x)))
+ (sphereToTrunc n' (fiber-cong²-hₙ₊₁-push∞ x)))
module _ (q : (x : Fin (fst (snd C) (suc n'))) (y : S₊ n')
→ fiber (cong² x y) (hₙ₊₁-push∞ x y)) where
diff --git a/Cubical.CW.Properties.html b/Cubical.CW.Properties.html
index 375c1182d..ca8bd61ff 100644
--- a/Cubical.CW.Properties.html
+++ b/Cubical.CW.Properties.html
@@ -240,7 +240,7 @@
inPushoutConnected : isConnectedFun (suc n) inPushout
inPushoutConnected = inlConnected (suc n) (α (suc n)) fst
- λ b → subst (isConnected (suc n)) (fstProjPath b) (sphereConnected n)
+ λ b → subst (isConnected (suc n)) (fstProjPath b) (sphereConnected n)
isConnected-CW↪∞ : (n : ℕ) (C : CWskel ℓ) → isConnectedFun n (CW↪∞ C n)
diff --git a/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html b/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html
index 3ace6bd5c..c46177d97 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html
@@ -258,7 +258,7 @@
(subst (λ x → (a : S₊ x → EM G 1) → 0ₕ 1 ≡ ∣ a ∣₂)
(cong suc (+-comm 1 m))
λ f → TR.rec (squash₂ _ _)
- (λ q → cong ∣_∣₂ (funExt (sphereElim (suc m)
+ (λ q → cong ∣_∣₂ (funExt (sphereElim (suc m)
(λ _ → isOfHLevelPath' (suc (suc zero +ℕ m))
(isOfHLevelPlus' {n = m} 3 (hLevelEM _ 1)) _ _) q)))
(isConnectedPath 1 (isConnectedEM 1) embase (f north) .fst))))
@@ -277,7 +277,7 @@
λ f →
TR.rec (isProp→isOfHLevelSuc (suc n) (squash₂ _ _))
(λ q → cong ∣_∣₂
- (funExt (sphereElim _
+ (funExt (sphereElim _
(λ s → isOfHLevelPath' (suc (suc (suc (m +ℕ n))))
(subst (λ x → isOfHLevel x (EM G (suc (suc n))))
(+-assoc m 4 n ∙ cong (_+ℕ n) (+-comm m 4))
@@ -297,7 +297,7 @@
H⁰[Sⁿ,G]≅G n = H⁰conn
(∣ ptSn (suc n) ∣ₕ
, (TR.elim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _)
- (sphereElim n (λ _ → isProp→isOfHLevelSuc n (isOfHLevelTrunc 2 _ _))
+ (sphereElim n (λ _ → isProp→isOfHLevelSuc n (isOfHLevelTrunc 2 _ _))
refl))) G
Hⁿ[Sᵐ,G]Full : (n m : ℕ)
diff --git a/Cubical.Cohomology.EilenbergMacLane.Gysin.html b/Cubical.Cohomology.EilenbergMacLane.Gysin.html
index 9fc38198e..738279f4c 100644
--- a/Cubical.Cohomology.EilenbergMacLane.Gysin.html
+++ b/Cubical.Cohomology.EilenbergMacLane.Gysin.html
@@ -667,8 +667,8 @@
(isoToEquiv
(congSuspIso
(equivToIso (fst e))) , refl)
- (isoToEquiv (invIso (IsoSucSphereSusp n))
- , IsoSucSphereSusp∙ n)
+ (isoToEquiv (invIso (IsoSucSphereSusp n))
+ , IsoSucSphereSusp∙ n)
module con (c : (b : fst B) → Q b →∙ EM∙ (CommRing→AbGroup R) (suc n))
(r : c (pt B) ≡ (gen-HⁿSⁿ-raw (CommRing→Ring R) (suc n) ∘∙ ≃∙map Q≃))
diff --git a/Cubical.Experiments.Problem.html b/Cubical.Experiments.Problem.html
index 0dd85fa7c..ce9159762 100644
--- a/Cubical.Experiments.Problem.html
+++ b/Cubical.Experiments.Problem.html
@@ -28,7 +28,7 @@
S³pt : ptType
S³pt = (S³ , base)
joinpt : ptType
-joinpt = (join S¹ S¹ , inl base)
+joinpt = (join S¹ S¹ , inl base)
Ω : (A : ptType) → ptType
Ω A = Path _ (pt A) (pt A) , refl
@@ -38,10 +38,10 @@
Ω³ A = Ω² (Ω A)
-α : join S¹ S¹ → S²
-α (inl _) = base
-α (inr _) = base
-α (push x y i) = (merid y ∙ merid x) i
+α : join S¹ S¹ → S²
+α (inl _) = base
+α (inr _) = base
+α (push x y i) = (merid y ∙ merid x) i
where
merid : S¹ → Path S² base base
merid base = refl
@@ -53,7 +53,7 @@
test0To2 i j k = surf i j k
f3 : Ω³ S³pt .fst → Ω³ joinpt .fst
-f3 p i j k = S³→joinS¹S¹ (p i j k)
+f3 p i j k = S³→joinS¹S¹ (p i j k)
test0To3 : Ω³ joinpt .fst
test0To3 = f3 test0To2
diff --git a/Cubical.Experiments.ZCohomology.Benchmarks.html b/Cubical.Experiments.ZCohomology.Benchmarks.html
index 02e2b3f83..d4e01c5fc 100644
--- a/Cubical.Experiments.ZCohomology.Benchmarks.html
+++ b/Cubical.Experiments.ZCohomology.Benchmarks.html
@@ -361,7 +361,7 @@
transport (λ i → (B : isoToPath IsoS³TotalHopf i → Type)
→ ((x : _) → isOfHLevel 3 (B x))
→ B (transp (λ j → isoToPath IsoS³TotalHopf (i ∨ ~ j)) i (north , base)) → (x : _) → B x)
- λ B hLev ind → sphereElim _ (λ _ → hLev _) ind
+ λ B hLev ind → sphereElim _ (λ _ → hLev _) ind
p : (a : TotalHopf) → ∣ fst a ∣ ≡ 0ₖ 2
p = ind _ (λ _ → isOfHLevelTrunc 4 _ _) refl
diff --git a/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html b/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html
index c2c93b44e..ed3aea6d7 100644
--- a/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html
+++ b/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html
@@ -72,10 +72,10 @@
∙ λ i → ∣ north , lUnit r (~ i) ∣
totalFun : (a b : S2+n) → P a b
- totalFun = wedgeconFun (suc n) (suc n) hLevelP rightFun leftFun funsAgree
+ totalFun = wedgeconFun (suc n) (suc n) hLevelP rightFun leftFun funsAgree
leftId : (λ x → totalFun x north) ≡ leftFun
- leftId x i = wedgeconRight (suc n) (suc n) hLevelP rightFun leftFun funsAgree i x
+ leftId x i = wedgeconRight (suc n) (suc n) hLevelP rightFun leftFun funsAgree i x
fwd : (p : north ≡ north) (a : S2+n)
→ hLevelTrunc 4n+2 (fiber σ p)
@@ -179,7 +179,7 @@
rotLemma (loop i) = refl
sphereConnectedSpecCase : isConnected 4 (Susp (Susp S¹))
-sphereConnectedSpecCase = sphereConnected 3
+sphereConnectedSpecCase = sphereConnected 3
d-mapComp : Iso (fiber d-map base) (Path (S₊ 3) north north)
d-mapComp = compIso (IsoΣPathTransportPathΣ {B = HopfSuspS¹} _ _)
@@ -193,7 +193,7 @@
where
contrHelper : isContr (Path (∥ Susp (Susp S¹) ∥ 4) ∣ north ∣ ∣ north ∣)
fst contrHelper = refl
- snd contrHelper = isOfHLevelPlus {n = 0} 2 (sphereConnected 3) ∣ north ∣ ∣ north ∣ refl
+ snd contrHelper = isOfHLevelPlus {n = 0} 2 (sphereConnected 3) ∣ north ∣ ∣ north ∣ refl
d-Iso : Iso (∥ Path (S₊ 2) north north ∥ 3) (coHomK 1)
d-Iso = connectedTruncIso _ d-map is1Connected-dmap
diff --git a/Cubical.Experiments.ZCohomologyOld.Properties.html b/Cubical.Experiments.ZCohomologyOld.Properties.html
index 74acbdb88..f74694272 100644
--- a/Cubical.Experiments.ZCohomologyOld.Properties.html
+++ b/Cubical.Experiments.ZCohomologyOld.Properties.html
@@ -65,7 +65,7 @@
(suspToPropElim (ptSn (suc n)) (λ _ → isOfHLevelTrunc 2 _ _) refl))
isConnectedKn : (n : ℕ) → isConnected (2 + n) (coHomK (suc n))
-isConnectedKn n = isOfHLevelRetractFromIso 0 (invIso (truncOfTruncIso (2 + n) 1)) (sphereConnected (suc n))
+isConnectedKn n = isOfHLevelRetractFromIso 0 (invIso (truncOfTruncIso (2 + n) 1)) (sphereConnected (suc n))
diff --git a/Cubical.HITs.Everything.html b/Cubical.HITs.Everything.html
index 6fa2db5c2..389947229 100644
--- a/Cubical.HITs.Everything.html
+++ b/Cubical.HITs.Everything.html
@@ -59,13 +59,14 @@
import Cubical.HITs.SmashProduct.SymmetricMonoidalCat
import Cubical.HITs.Sn
import Cubical.HITs.Sn.Degree
-import Cubical.HITs.SphereBouquet
-import Cubical.HITs.SphereBouquet.Degree
-import Cubical.HITs.Susp
-import Cubical.HITs.Susp.LoopAdjunction
-import Cubical.HITs.Torus
-import Cubical.HITs.Truncation
-import Cubical.HITs.TypeQuotients
-import Cubical.HITs.UnorderedPair
-import Cubical.HITs.Wedge
+import Cubical.HITs.Sn.Multiplication
+import Cubical.HITs.SphereBouquet
+import Cubical.HITs.SphereBouquet.Degree
+import Cubical.HITs.Susp
+import Cubical.HITs.Susp.LoopAdjunction
+import Cubical.HITs.Torus
+import Cubical.HITs.Truncation
+import Cubical.HITs.TypeQuotients
+import Cubical.HITs.UnorderedPair
+import Cubical.HITs.Wedge