Experience shows that, at least for homotopy groups, ⊙Ω^ (S

Compare, for example, <div class="Box-head

<a class="user-mention notranslate" data-hovercard-type="user" data-hovercard-url="/us

Change the inductive definition of iterative loop spaces? about hott-agda HOT 6 CLOSED

hott commented on June 27, 2024

Change the inductive definition of iterative loop spaces?

from hott-agda.

Comments (6)

guillaumebrunerie commented on June 27, 2024

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?

from hott-agda.

favonia commented on June 27, 2024

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)

from hott-agda.

fpvandoorn commented on June 27, 2024

@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.

from hott-agda.

favonia commented on June 27, 2024

@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)

from hott-agda.

favonia commented on June 27, 2024

@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.

from hott-agda.

favonia commented on June 27, 2024

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

from hott-agda.

Change the inductive definition of iterative loop spaces? about hott-agda HOT 6 CLOSED

Comments (6)

Related Issues (20)

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent

	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

	Ω^'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)

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

	Ω^'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)