Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proof of Blakers-Massey Theorem #613

Merged
merged 20 commits into from
Nov 11, 2021
Merged

Proof of Blakers-Massey Theorem #613

Show file tree
Hide file tree
Changes from 19 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
a21d4d4
add parts of proof
kangxyz Oct 30, 2021
9bb4207
add a property
kangxyz Oct 30, 2021
901af5e
add composition of squares
kangxyz Oct 30, 2021
46661d8
add some properties of recursor
kangxyz Oct 30, 2021
a87c55d
add a square version of hom
kangxyz Oct 30, 2021
e862bca
add more prrof parts and move preliminary functions to other modules
kangxyz Oct 30, 2021
bc0933b
add infixr for square composition
kangxyz Oct 30, 2021
65d607a
finish all coherence cubes
kangxyz Oct 30, 2021
5dc09db
finite the coherence part
kangxyz Oct 30, 2021
d67d26f
finish the definition of Code
kangxyz Oct 30, 2021
a78a7f1
add some definitions
kangxyz Oct 30, 2021
20592e2
add transp rule of truncations
kangxyz Oct 31, 2021
5585a07
add a transportation rule for Code
kangxyz Oct 31, 2021
4a37aee
finish the contractibility of Code
kangxyz Oct 31, 2021
fbfed61
finish the proof
kangxyz Oct 31, 2021
ee42a4a
make indent correct
kangxyz Oct 31, 2021
bf18d2c
fix whitespaces
kangxyz Oct 31, 2021
0116e01
fix whitespace again
kangxyz Oct 31, 2021
d8e6c1b
fix by request
kangxyz Nov 11, 2021
49ff905
fix names
kangxyz Nov 11, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions Cubical/Foundations/HLevels.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -409,6 +409,10 @@ isOfHLevelΠ (suc (suc (suc (suc (suc n))))) h f g p q P Q R S =
(cong funExt⁻ P) (cong funExt⁻ Q)
(cong (cong funExt⁻) R) (cong (cong funExt⁻) S))

isOfHLevelΠ2 : (n : HLevel) → ((x : A) → (y : B x) → isOfHLevel n (C x y))
→ isOfHLevel n ((x : A) → (y : B x) → C x y)
isOfHLevelΠ2 n f = isOfHLevelΠ n (λ x → isOfHLevelΠ n (f x))

isContrΠ : (h : (x : A) → isContr (B x)) → isContr ((x : A) → B x)
isContrΠ = isOfHLevelΠ 0

Expand Down
13 changes: 13 additions & 0 deletions Cubical/Foundations/Prelude.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ module Cubical.Foundations.Prelude where
open import Cubical.Core.Primitives public

infixr 30 _∙_
infixr 30 _∙₂_
infix 3 _∎
infixr 2 _≡⟨_⟩_
infixr 2.5 _≡⟨_⟩≡⟨_⟩_
Expand Down Expand Up @@ -353,6 +354,18 @@ Square :
→ Type _
Square a₀₋ a₁₋ a₋₀ a₋₁ = PathP (λ i → a₋₀ i ≡ a₋₁ i) a₀₋ a₁₋

-- vertical composition of squares
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@aljungstrom Didn't you need something like this in your very big PR?

_∙₂_ :
{a₀₀ a₀₁ a₀₂ : A} {a₀₋ : a₀₀ ≡ a₀₁} {b₀₋ : a₀₁ ≡ a₀₂}
{a₁₀ a₁₁ a₁₂ : A} {a₁₋ : a₁₀ ≡ a₁₁} {b₁₋ : a₁₁ ≡ a₁₂}
{a₋₀ : a₀₀ ≡ a₁₀} {a₋₁ : a₀₁ ≡ a₁₁} {a₋₂ : a₀₂ ≡ a₁₂}
(p : Square a₀₋ a₁₋ a₋₀ a₋₁) (q : Square b₀₋ b₁₋ a₋₁ a₋₂)
→ Square (a₀₋ ∙ b₀₋) (a₁₋ ∙ b₁₋) a₋₀ a₋₂
_∙₂_ {a₋₀ = a₋₀} p q i j =
hcomp (λ k → λ { (j = i0) → a₋₀ i
; (j = i1) → q i k })
(p i j)

isSet' : Type ℓ → Type ℓ
isSet' A =
{a₀₀ a₀₁ : A} (a₀₋ : a₀₀ ≡ a₀₁)
Expand Down
36 changes: 36 additions & 0 deletions Cubical/HITs/Truncation/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -258,6 +258,34 @@ Iso.rightInv (univTrunc (suc n) {B , lev}) b = refl
Iso.leftInv (univTrunc (suc n) {B , lev}) b = funExt (elim (λ x → isOfHLevelPath _ lev _ _)
λ a → refl)

-- some useful properties of recursor

recUniq : {n : HLevel}
→ (h : isOfHLevel n B)
→ (g : A → B)
→ (x : A)
→ rec h g ∣ x ∣ₕ ≡ g x
recUniq {n = zero} h g x = h .snd (g x)
recUniq {n = suc n} _ _ _ = refl

∘rec : ∀{ℓ''} {n : HLevel}{C : Type ℓ''}
→ (h : isOfHLevel n B)
→ (h' : isOfHLevel n C)
→ (g : A → B)
→ (f : B → C)
→ (x : hLevelTrunc n A)
→ rec h' (f ∘ g) x ≡ f (rec h g x)
∘rec {n = zero} h h' g f x = h' .snd (f (rec h g x))
∘rec {n = suc n} h h' g f = elim (λ _ → isOfHLevelPath _ h' _ _) (λ _ → refl)

recId : {n : HLevel}
→ (f : A → hLevelTrunc n A)
→ ((x : A) → f x ≡ ∣ x ∣ₕ)
→ rec (isOfHLevelTrunc _) f ≡ idfun _
recId {n = n} f h i x =
elim {B = λ a → rec (isOfHLevelTrunc _) f a ≡ a}
(λ _ → isOfHLevelTruncPath) (λ a → recUniq {n = n} (isOfHLevelTrunc _) f a ∙ h a) x i

-- functorial action

map : {n : HLevel} {B : Type ℓ'} (g : A → B)
Expand Down Expand Up @@ -528,3 +556,11 @@ Iso.rightInv (truncOfΣIso (suc n)) =
λ b → refl)
Iso.leftInv (truncOfΣIso (suc n)) =
elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ {(a , b) → refl}

{- transport along family of truncations -}

transportTrunc : {n : HLevel}{p : A ≡ B}
→ (a : A)
→ transport (λ i → hLevelTrunc n (p i)) ∣ a ∣ₕ ≡ ∣ transport (λ i → p i) a ∣ₕ
transportTrunc {n = zero} a = refl
transportTrunc {n = suc n} a = refl
Loading