Whitehead's Lemma #1067
Whitehead's Lemma #1067
Conversation
| SetTrunc→PropTrunc : {A : Type ℓ} → ∥ A ∥₂ → ∥ A ∥₁ | ||
| SetTrunc→PropTrunc = sRec (isProp→isSet isPropPropTrunc) ∣_∣₁ | ||
|
|
||
| isoPostComp : {A : Type ℓ} {a b c : A} (p : b ≡ c) |
There was a problem hiding this comment.
Duplication: compPathrEquiv in Foundations.Path
| Iso.leftInv (isoPostComp p) = | ||
| λ r → (sym (assoc r p (sym p))) ∙ cong (r ∙_) (rCancel p) ∙ sym (rUnit r) | ||
|
|
||
| isoPostComp≃∙ : {A : Type ℓ} {a b c : A} {q : a ≡ b} (p : b ≡ c) |
There was a problem hiding this comment.
This should be in the lib already (but isn't). I suggest adding it to the end of Foundations.Pointed.Properties and calling it compPathrEquiv∙ just for the sake of consistency w other things in the lib.
| fst (isoPostComp≃∙ p) = isoToEquiv (isoPostComp p) | ||
| snd (isoPostComp≃∙ p) = refl | ||
|
|
||
| isoPreComp : {A : Type ℓ} {a b c : A} (p : a ≡ b) |
There was a problem hiding this comment.
Duplication: compPathlEquiv in Foundations.Path
| Iso.leftInv (isoPreComp p) = | ||
| λ r → assoc (sym p) p r ∙ cong (_∙ r) (lCancel p) ∙ sym (lUnit r) | ||
|
|
||
| isoPreComp≃∙ : {A : Type ℓ} {a b c : A} {q : b ≡ c} (p : a ≡ b) |
There was a problem hiding this comment.
Same as isoPostComp≃∙: should probably be moved to Foundations.Pointed.Properties and get a name change
|
|
||
| doubleCompPath-filler-refl : {A : Type ℓ} {a b : A} (p : a ≡ b) | ||
| → p ≡ refl ∙∙ p ∙∙ refl | ||
| doubleCompPath-filler-refl p = doubleCompPath-filler refl p refl |
There was a problem hiding this comment.
This is actually just rUnit
| ( f _) b' | ||
| ( transport (λ i → f _ ≡ b') _) (snd a'))))) | ||
|
|
||
| isPointedTarget→isEquiv→isEquiv : {A B : Type ℓ} (f : A → B) |
There was a problem hiding this comment.
Think we're missing this one. I think it should be put in Foundations.Properties.Equiv.
| ∙ cong (cong f) (sym (rUnit _)))) | ||
|
|
||
| private | ||
| setMapFunctorial : {A B C : Type ℓ} (f : A → B) (g : B → C) |
There was a problem hiding this comment.
Oh wow, we really should have this one lol... Could you put it in HITs.SetTruncation.Properties? And maybe just call it mapFunctorial to match the naming there better.
| ( PathPΩ^→Ω (1 + n) (f , refl))) | ||
|
|
||
| private | ||
| ∙∙Lemma : {A B : Type ℓ} {f : A → B} {a b : A} (p : a ≡ b) |
There was a problem hiding this comment.
This one can be removed. If you just use sym (rUnit (cong f p)) for this one, it is definitionally equal to ∙∙lCancel refl when p is refl
| ∙ cong map (cong (fst ∘ (Ω^→ (1 + n))) | ||
| ( funExt∙ | ||
| ( ∙∙Lemma {f = f} | ||
| , JRefl ( λ b p → (refl ∙∙ cong f p ∙∙ refl) ≡ cong f p) |
There was a problem hiding this comment.
funExt∙ ((λ a → sym (rUnit (cong f a))) , rUnit (∙∙lCancel refl))
| ( Iso.fun (flipΩIso (1 + n)) ∘ fst ((Ω^→ (2 + n)) (f , refl))) | ||
|
|
||
| -- Ω (Ω→ f) ≡ Ω→ (Ω f) | ||
| PathPΩ^→Ω : {A B : Pointed ℓ} (n : ℕ) (f : A →∙ B) |
There was a problem hiding this comment.
In the future we may consider moving some of these properties to Homotopy.Group.Base or something (or maybe a new Properties file?) but let's keep it here for now.
Thanks! |
|
Have all comments been resolved? If so I can merge as soon as the CI is finished |
|
@aljungstrom confirmed that all comments are resolved, so I'll merge now |
* Whiteheads Lemma * comments in Whiteheads lemma file * delete-trailing-whitespace * moved lemmas, removed duplicates
Proof of Whitehead's lemma for truncated spaces (theorem 8.8.3 in the HoTT book).