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

Jump to bottom

New rec for EM-spaces #968

Merged
merged 4 commits into from
Dec 7, 2022
Merged

New rec for EM-spaces #968

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
cbb01e5
refactor: clean up imports, add comment
felixwellen Dec 3, 2022
cd9f9e8
alternative recursor for first eilenberg maclane space
felixwellen Dec 3, 2022
632f451
typo
felixwellen Dec 6, 2022
d2feb7f
one sym for matthias
felixwellen Dec 6, 2022
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
5 changes: 5 additions & 0 deletions Cubical/HITs/EilenbergMacLane1/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,11 @@ This file contains:

- The first Eilenberg–Mac Lane type as a HIT

Remark: The proof that there is an isomorphism of types
between Ω EM₁ and G is in

Cubical.Homotopy.EilenbergMacLane.Properties

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.EilenbergMacLane1.Base where
Expand Down
31 changes: 22 additions & 9 deletions Cubical/HITs/EilenbergMacLane1/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,27 +7,23 @@ Eilenberg–Mac Lane type K(G, 1)
{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-}
module Cubical.HITs.EilenbergMacLane1.Properties where

open import Cubical.HITs.EilenbergMacLane1.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Functions.Morphism

open import Cubical.Data.Sigma
open import Cubical.Data.Empty renaming (rec to ⊥-rec) hiding (elim)


open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup.Base

open import Cubical.Functions.Morphism
open import Cubical.HITs.EilenbergMacLane1.Base


private
variable
Expand Down Expand Up @@ -127,3 +123,20 @@ module _ ((G , str) : Group ℓG) where
→ (x : EM₁ (G , str))
→ B
rec Bgpd = elim (λ _ → Bgpd)

rec' : {B : Type ℓ}
→ isGroupoid B
→ (b : B)
→ (bloop : G → b ≡ b)
→ ((g h : G) → bloop (g · h) ≡ bloop g ∙ bloop h)
→ (x : EM₁ (G , str))
→ B
rec' Bgpd b bloop square =
rec Bgpd b bloop
(λ g h → compPath→Square (withRefl g h))
where withRefl : (g h : G)
→ refl ∙ bloop (g · h) ≡ bloop g ∙ bloop h
withRefl g h =
refl ∙ bloop (g · h) ≡⟨ sym (lUnit (bloop (g · h))) ⟩
bloop (g · h) ≡⟨ square g h ⟩
bloop g ∙ bloop h ∎
21 changes: 9 additions & 12 deletions Cubical/Homotopy/EilenbergMacLane/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,8 @@ open import Cubical.Data.Sigma
open import Cubical.Data.Nat hiding (_·_)

open import Cubical.HITs.Truncation as Trunc
renaming (rec to trRec; elim to trElim)
open import Cubical.HITs.EilenbergMacLane1
renaming (rec to EMrec ; elim to EM₁elim)
open import Cubical.HITs.Truncation
renaming (elim to trElim ; rec to trRec ; rec2 to trRec2)
open import Cubical.HITs.Susp

private
Expand All @@ -48,7 +45,7 @@ isConnectedEM₁ : (G : Group ℓ) → isConnected 2 (EM₁ G)
isConnectedEM₁ G = ∣ embase ∣ , h
where
h : (y : hLevelTrunc 2 (EM₁ G)) → ∣ embase ∣ ≡ y
h = trElim (λ y → isOfHLevelSuc 1 (isOfHLevelTrunc 2 ∣ embase ∣ y))
h = Trunc.elim (λ y → isOfHLevelSuc 1 (isOfHLevelTrunc 2 ∣ embase ∣ y))
(elimProp G (λ x → isOfHLevelTrunc 2 ∣ embase ∣ ∣ x ∣) refl)

module _ {G' : AbGroup ℓ} where
Expand All @@ -63,8 +60,8 @@ module _ {G' : AbGroup ℓ} where
isConnectedEM (suc zero) = isConnectedEM₁ (AbGroup→Group G')
fst (isConnectedEM (suc (suc n))) = ∣ 0ₖ _ ∣
snd (isConnectedEM (suc (suc n))) =
trElim (λ _ → isOfHLevelTruncPath)
(trElim (λ _ → isOfHLevelSuc (3 + n) (isOfHLevelTruncPath {n = (3 + n)}))
Trunc.elim (λ _ → isOfHLevelTruncPath)
(Trunc.elim (λ _ → isOfHLevelSuc (3 + n) (isOfHLevelTruncPath {n = (3 + n)}))
(raw-elim G'
(suc n)
(λ _ → isOfHLevelTrunc (3 + n) _ _)
Expand Down Expand Up @@ -190,7 +187,7 @@ module _ {G : AbGroup ℓ} where

CODE : (n : ℕ) → EM G (suc (suc n)) → TypeOfHLevel ℓ (3 + n)
CODE n =
trElim (λ _ → isOfHLevelTypeOfHLevel (3 + n))
Trunc.elim (λ _ → isOfHLevelTypeOfHLevel (3 + n))
λ { north → EM G (suc n) , hLevelEM G (suc n)
; south → EM G (suc n) , hLevelEM G (suc n)
; (merid a i) → fib n a i}
Expand All @@ -206,7 +203,7 @@ module _ {G : AbGroup ℓ} where

decode' : (n : ℕ) (x : EM G (suc (suc n))) → CODE n x .fst → 0ₖ (suc (suc n)) ≡ x
decode' n =
trElim (λ _ → isOfHLevelΠ (4 + n)
Trunc.elim (λ _ → isOfHLevelΠ (4 + n)
λ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
λ { north → f n
; south → g n
Expand Down Expand Up @@ -283,7 +280,7 @@ module _ {G : AbGroup ℓ} where
(λ i → lUnitₖ 1 (transportRefl x i) i)
∙ (λ i → rUnitₖ 1 (transportRefl x i) i))
encode'-decode' (suc n) =
trElim (λ _ → isOfHLevelTruncPath {n = 4 + n})
Trunc.elim (λ _ → isOfHLevelTruncPath {n = 4 + n})
λ x → cong (encode' (suc n) (0ₖ (3 + n))) (cong-∙ ∣_∣ₕ (merid x) (sym (merid north)))
∙∙ substComposite (λ x → CODE (suc n) x .fst)
(cong ∣_∣ₕ (merid x)) (sym (cong ∣_∣ₕ (merid ptEM-raw))) (0ₖ (2 + n))
Expand Down Expand Up @@ -397,7 +394,7 @@ module _ {G : AbGroup ℓ} where
∙∙ cong (_∙ q) (rCancel (emloop g))
∙∙ sym (lUnit q)))))
ΩEM+1→EM-gen (suc n) =
trElim (λ _ → isOfHLevelΠ (4 + n)
Trunc.elim (λ _ → isOfHLevelΠ (4 + n)
λ _ → isOfHLevelSuc (3 + n) (hLevelEM _ (suc n)))
λ { north → ΩEM+1→EM (suc n)
; south p → ΩEM+1→EM (suc n) (cong ∣_∣ₕ (merid ptEM-raw)
Expand Down Expand Up @@ -454,7 +451,7 @@ module _ where
(funExt (raw-elim G 0 (λ _ → is-set (snd H) _ _) (sym p)))
fst (isContr-↓∙ {G = G} {H = H} (suc n)) = (λ _ → 0ₖ (suc n)) , refl
fst (snd (isContr-↓∙ {G = G} {H = H} (suc n)) f i) x =
trElim {B = λ x → 0ₖ (suc n) ≡ fst f x}
Trunc.elim {B = λ x → 0ₖ (suc n) ≡ fst f x}
(λ _ → isOfHLevelPath (4 + n) (isOfHLevelSuc (3 + n) (hLevelEM H (suc n))) _ _)
(raw-elim _ _ (λ _ → hLevelEM H (suc n) _ _) (sym (snd f)))
x i
Expand Down Expand Up @@ -562,7 +559,7 @@ module _ where
raw-elim G zero
(λ _ → isOfHLevel↑∙ zero m _ _) p
help (suc n) f p =
trElim (λ _ → isOfHLevelPath (4 + n)
Trunc.elim (λ _ → isOfHLevelPath (4 + n)
(subst (λ x → isOfHLevel x (EM∙ H (suc m) →∙ EM∙ L (suc ((suc n) + m))))
(λ i → suc (suc (+-comm (suc n) 1 i)))
(isOfHLevelPlus' {n = 1} (3 + n) (isOfHLevel↑∙ (suc n) m))) _ _)
Expand Down