Change the inductive definition of iterative loop spaces?

[favonia]

Experience shows that, at least for homotopy groups, ⊙Ω^ (S n) X should be ⊙Ω^ n (⊙Ω X), not ⊙Ω (⊙Ω^ n X).

[guillaumebrunerie]

I have no objection to that change. I believe I chose the other one just because I had no idea which one was better and I had to choose one.
Do you have any explicit example showing that it’s a better option?

[favonia]

Compare, for example,

HoTT-Agda/core/lib/groups/HomotopyGroup.agda

Lines 64 to 103 in 159df93

	private
	record Ω^STruncPreIso (n : ℕ) (m : ℕ₋₂) (k : ℕ₋₂) (X : Ptd i)
	: Type i where
	field
	F : ⊙Ω^ (S n) (⊙Trunc k X) ⊙→ ⊙Trunc m (⊙Ω^ (S n) X)
	pres-comp : ∀ (p q : Ω^ (S n) (⊙Trunc k X))
	→ fst F (Ω^S-∙ n p q) == Trunc-fmap2 (Ω^S-∙ n) (fst F p) (fst F q)
	e : is-equiv (fst F)
	Ω^S-Trunc-preiso : (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
	→ Ω^STruncPreIso n m (⟨ S n ⟩₋₂ +2+ m) X
	Ω^S-Trunc-preiso O m X =
	record { F = (–> (Trunc=-equiv [ pt X ] [ pt X ]) , idp);
	pres-comp = Trunc=-∙-comm;
	e = snd (Trunc=-equiv [ pt X ] [ pt X ]) }
	Ω^S-Trunc-preiso (S n) m X =
	let
	r : Ω^STruncPreIso n (S m) (⟨ S n ⟩₋₂ +2+ S m) X
	r = Ω^S-Trunc-preiso n (S m) X
	H = (–> (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]) , idp)
	G = ⊙Ω-fmap (Ω^STruncPreIso.F r)
	in
	transport (λ k → Ω^STruncPreIso (S n) m k X)
	(+2+-βr ⟨ S n ⟩₋₂ m)
	(record {
	F = H ⊙∘ G;
	pres-comp = λ p q →
	ap (fst H) (Ω^S-fmap-∙ 0 (Ω^STruncPreIso.F r) p q)
	∙ (Trunc=-∙-comm (fst G p) (fst G q));
	e = snd (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]
	∘e Ω^-emap 1 (Ω^STruncPreIso.F r , Ω^STruncPreIso.e r))})
	Ω^S-group-Trunc-fuse-diag-iso : (n : ℕ) (X : Ptd i)
	→ Ω^S-group n (⊙Trunc ⟨ S n ⟩ X) ≃ᴳ πS n X
	Ω^S-group-Trunc-fuse-diag-iso n X = group-hom (fst F) pres-comp , e
	where
	r = transport (λ k → Ω^STruncPreIso n 0 k X)
	(+2+0 ⟨ S n ⟩₋₂) (Ω^S-Trunc-preiso n 0 X)
	open Ω^STruncPreIso r

and

HoTT-Agda/core/lib/groups/HomotopyGroup.agda

Lines 107 to 113 in 159df93

	Ω^'S-group-Trunc-fuse-diag-iso : (n : ℕ) (X : Ptd i)
	→ Ω^'S-group n (⊙Trunc ⟨ S n ⟩ X) ≃ᴳ π'S n X
	Ω^'S-group-Trunc-fuse-diag-iso O X =
	≃-to-≃ᴳ (Trunc=-equiv [ pt X ] [ pt X ]) Trunc=-∙-comm
	Ω^'S-group-Trunc-fuse-diag-iso (S n) X =
	Ω^'S-group-Trunc-fuse-diag-iso n (⊙Ω X)
	∘eᴳ Ω^'S-group-emap n {X = ⊙Ω (⊙Trunc ⟨ S (S n) ⟩ X)} (≃-to-⊙≃ (Trunc=-equiv [ pt X ] [ pt X ]) idp)

.

[fpvandoorn]

@favonia asked me to comment.

In Lean we use the definition of Ωⁿ(X) where Ωⁿ⁺¹(X) :≡ Ω(Ωⁿ(X)). I think that definition is more convenient, even though you wish you sometimes had the other definition. One major convenience is that the binary operation on Ωⁿ⁺¹(X) is just path concatenation in this case, and that for pointed maps f we have Ωⁿ⁺¹(f) :≡ Ω(Ωⁿ(f)). Of course, in many results in homotopy we do need to apply the equivalence Ωⁿ⁺¹(X) ≃ Ωⁿ(Ω(X)).

Actually, long ago we did use the other definition where Ωⁿ⁺¹(X) ≡ Ωⁿ(Ω(X)) (I think Coq-HoTT uses that). When we changed it I thought it was a simplification overall.

[favonia]

@fpvandoorn Thanks for the comment. I have done the concatenation and lemmas about it, and felt they are fine once you get used to the induction from X to Ω(X). I will check the change in more details later.

Right now the alternative concatenation is defined as

HoTT-Agda/core/lib/types/LoopSpace.agda

Lines 278 to 280 in 159df93

	Ω^'S-∙ : (n : ℕ) {X : Ptd i} → Ω^' (S n) X → Ω^' (S n) X → Ω^' (S n) X
	Ω^'S-∙ O = Ω-∙
	Ω^'S-∙ (S n) {X} = Ω^'S-∙ n {⊙Ω X}

and one lemma is

HoTT-Agda/core/lib/types/LoopSpace.agda

Lines 351 to 356 in 159df93

	Ω^'S-fmap-∙ : ∀ {i j} (n : ℕ)
	{X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p q : Ω^' (S n) X)
	→ Ω^'-fmap (S n) F (Ω^'S-∙ n p q)
	== Ω^'S-∙ n (Ω^'-fmap (S n) F p) (Ω^'-fmap (S n) F q)
	Ω^'S-fmap-∙ O = Ω-fmap-∙
	Ω^'S-fmap-∙ (S n) F = Ω^'S-fmap-∙ n (⊙Ω-fmap F)

.

[favonia]

@fpvandoorn I think my main point is that we do not seem to need any add.comm or loop_space_add if I stick with the alternative definition. I will ask Coq-HoTT people.

[favonia]

Closing this as there's nothing to do. We have two versions now.