This commit is contained in:
Michael Zhang 2024-07-26 23:24:51 -05:00
parent a0906b6bff
commit 5d3ebb119b
3 changed files with 74 additions and 27 deletions

View file

@ -11,6 +11,7 @@ open import HottBook.Chapter1
open import HottBook.Chapter1Util
open import HottBook.Chapter2Lemma221 public
open import HottBook.Chapter2Lemma231 public
open import HottBook.Chapter2Definition217 public
private
variable
@ -84,36 +85,34 @@ module lemma2∙1∙4 {l : Level} {A : Set l} where
iv {x} {y} {z} {w} refl refl refl = refl
```
### Definition 2.1.7 (pointed type)
This comes first, since it is needed to define Theorem 2.1.6.
```
pointed : (l : Level) → Set (lsuc l)
pointed l = Σ (Set l) (λ A → A)
```
### Definition 2.1.8 (loop space)
```
Ω : {l : Level} → pointed l → Set l
Ω (A , a) = a ≡ a
```
### Theorem 2.1.6 (Eckmann-Hilton)
```
module theorem2∙1∙6 where
Ω² : {l : Level} → pointed l → Set l
Ω² p = Ω (Ω p , refl)
Ω-type : (A : Set) → (a : A) → Set
Ω-type A a = refl {x = a} ≡ refl
compose : {l : Level} {p : pointed l} → (Ω² p) × (Ω² p) → Ω² p
compose (a , b) = a ∙ b
compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a))
compose1 x y = x ∙ y
-- commute : {l : Level} {p : pointed l} → (α β : Ω² p) → α ∙ β ≡ β ∙ α
-- commute {l} {p @ (A , a₀)} α β = {! !}
Ω² : {l : Level} → Set* l → Set* l
Ω² {l} = Ω[_] {l = l} 2
compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a))
compose2 x y = x ∙ y
compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x
compose2-commutative {l} {A} {a} x y = {! !}
```
### Definition 2.1.7 (pointed type)
{{#include HottBook.Chapter2Definition217.md:pointedtype}}
### Definition 2.1.8 (loop space)
{{#include HottBook.Chapter2Definition217.md:loopspace}}
## 2.2 Functions are functors
### Lemma 2.2.1

View file

@ -0,0 +1,30 @@
```
{-# OPTIONS --rewriting #-}
module HottBook.Chapter2Definition217 where
open import Agda.Primitive
open import HottBook.Chapter1
```
[//]: <> (ANCHOR: pointedtype)
```
Set* : (l : Level) → Set (lsuc l)
Set* l = Σ (Set l) (λ A → A)
```
[//]: <> (ANCHOR_END: pointedtype)
[//]: <> (ANCHOR: loopspace)
```
Ω : {l : Level} → Set* l → Set* l
Ω (A , a) = (a ≡ a) , refl
Ω[_] : {l : Level} → → Set* l → Set* l
Ω[ zero ] (A , a) = (A , a)
Ω[ suc n ] (A , a) = Ω[ n ] (Ω (A , a))
```
[//]: <> (ANCHOR_END: loopspace)

View file

@ -300,10 +300,10 @@ module Suspension where
A : Set l
postulate
Susp : Set → Set
Susp : Set l → Set l
N : Susp A
S : Susp A
merid : A → (N {A} ≡ S {A})
merid : A → (N {A = A} ≡ S {A = A})
rec-Susp : {B : Set l} → (n s : B) → (m : A → n ≡ s) → Susp A → B
rec-Susp-N : {B : Set l} → (n s : B) → (m : A → n ≡ s) → rec-Susp n s m N ≡ n
@ -371,7 +371,7 @@ module definition6∙5∙2 where
### Lemma 6.5.3
```
Map* : {l : Level} → (A B : pointed l) → Set l
Map* : {l : Level} → (A B : Set* l) → Set l
Map* (A , a₀) (B , b₀) = Σ (A → B) (λ f → f a₀ ≡ b₀)
```
@ -379,13 +379,13 @@ Adjoining a disjoint basepoint
```
module lol where
_₊ : {l : Level} → Set l → pointed l
_₊ : {l : Level} → Set l → Set* l
A ₊ = A + Lift 𝟙 , inr (lift tt)
```
```
open lol
lemma6∙5∙3 : {l : Level} (A : Set l) → (B* @ (B , b₀) : pointed l)
lemma6∙5∙3 : {l : Level} (A : Set l) → (B* @ (B , b₀) : Set* l)
→ (Map* (A ₊) B*) ≃ (A → B)
lemma6∙5∙3 A B* @ (B , b₀) = f , qinv-to-isequiv (mkQinv g forward {! !})
where
@ -409,6 +409,24 @@ lemma6∙5∙3 A B* @ (B , b₀) = f , qinv-to-isequiv (mkQinv g forward {! !}
-- g (f' x) gives us b₀
```
### Lemma 6.5.4
```
Susp* : {l : Level} → Set* l → Set* l
Susp* (A , a₀) = Susp A , N
lemma6∙5∙4 : {l : Level}
→ (A* @ (A , a₀) : Set* l)
→ (B* @ (B , b₀) : Set* l)
→ Map* {l = l} (Susp* A*) B* ≃ Map* A* (Ω B*)
lemma6∙5∙4 A* B* = f , {! !}
where
f : Map* (Susp* A*) B* → Map* A* (Ω B*)
f (f' , p) = {! f'' , ? !}
where
f'' : A* → Ω B*
```
## 6.6 Cell complexes
```