wip

src/HottBook/Chapter2.lagda.md

@@ -89,14 +89,14 @@ module lemma2∙1∙4 {l : Level} {A : Set l} where
 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)
+pointed : (l : Level) → Set (lsuc l)
+pointed l = Σ (Set l) (λ A → A)
 ```
 
 ### Definition 2.1.8 (loop space)
 
 ```
-Ω : {l : Level} → pointed {l} → pointed {l}
+Ω : {l : Level} → pointed l → pointed l
 Ω (A , a) = (a ≡ a) , refl
 ```
 
@@ -104,7 +104,7 @@ pointed {l} = Σ (Set l) (λ A → A)
 
 ```
 module theorem2∙1∙6 where
-  Ω² : {l : Level} → pointed {l} → pointed {l}
+  Ω² : {l : Level} → pointed l → pointed l
   Ω² p = Ω (Ω p)
 
   -- compose : {l : Level} {p : pointed {l}} → (Ω² p) × (Ω² p) → Ω² p

src/HottBook/Chapter6.lagda.md

@@ -193,33 +193,38 @@ lemma6∙4∙2 = f , g
 ### Corollary 6.4.3
 
 ```
--- corollary6∙4∙3 : (l : Level) → ¬ (is-1-type (Set l))
--- corollary6∙4∙3 l p = {!   !}
---   where
---     open lemma2∙4∙12
+corollary6∙4∙3 : (l : Level) → ¬ (is-1-type (Set l))
+corollary6∙4∙3 l p = {!   !}
+  where
+    open lemma2∙4∙12
 
---     Circle : Set l
---     Circle = Lift S¹
+    Circle : Set l
+    Circle = Lift S¹
 
---     self : Set (lsuc l)
---     self = Circle ≡ Circle
+    self : Set (lsuc l)
+    self = Circle ≡ Circle
 
---     self-equiv : Set l
---     self-equiv = Circle ≃ Circle
+    self-equiv : Set l
+    self-equiv = Circle ≃ Circle
 
---     goal1 : ¬ isSet self-equiv
+    goal1 : ¬ isSet self-equiv
 
---     goal2 : ¬ isProp (id-equiv Circle ≡ id-equiv Circle)
---     goal1 p = goal2 λ p' q' → p (id-equiv Circle) (id-equiv Circle) p' q'
+    goal2 : ¬ isProp (id-equiv Circle ≡ id-equiv Circle)
+    goal1 p = goal2 λ p' q' → p (id-equiv Circle) (id-equiv Circle) p' q'
 
---     postulate
---       equivalence-isProp : isProp self-equiv
+    goal2 = {!   !}
 
---     goal3 : ¬ isProp (id {A = Circle} ≡ id)
---     goal4 : (id {A = Circle} ≡ id) ≡ (id-equiv Circle ≡ id-equiv Circle)
+    -- postulate
+    --   equivalence-isProp : isProp self-equiv
 
---     A : Set l
---     goal : ⊥
+    -- goal3 : ¬ isProp (id {A = Circle} ≡ id)
+    -- goal2 prop = goal3 λ x y → {!   !}
+
+    -- goal4 : (id {A = Circle} ≡ id) ≃ (id-equiv Circle ≡ id-equiv Circle)
+    -- goal4 = f , {!   !}
+    --   where
+    --     f : (id {A = Circle} ≡ id) → (id-equiv Circle ≡ id-equiv Circle)
+    --     f p = ap (λ z → z , {! mkIsEquiv id (λ _ → refl) id (λ _ → refl)  !}) p
 ```
 
 ### Lemma 6.4.4
@@ -307,30 +312,115 @@ module Suspension where
     {-# REWRITE rec-Susp-S #-}
 
     rec-Susp-merid : {B : Set l} (n s : B) → (m : A → n ≡ s) → (a : A) → ap (rec-Susp n s m) (merid a) ≡ m a
+
+    ind-Susp : {P : Susp A → Set l} → (n : P N) → (s : P S) → (m : (a : A) → n ≡[ P , merid a ] s) → (x : Susp A) → P x
+    ind-Susp-N : {P : Susp A → Set l} → (n : P N) → (s : P S) → (m : (a : A) → n ≡[ P , merid a ] s) → ind-Susp {P = P} n s m N ≡ n
+    ind-Susp-S : {P : Susp A → Set l} → (n : P N) → (s : P S) → (m : (a : A) → n ≡[ P , merid a ] s) → ind-Susp {P = P} n s m S ≡ s
+    {-# REWRITE ind-Susp-N #-}
+    {-# REWRITE ind-Susp-S #-}
+
+    ind-Susp-merid : {P : Susp A → Set l} → (n : P N) → (s : P S) → (m : (a : A) → n ≡[ P , merid a ] s) → (a : A) → apd (ind-Susp {P = P} n s m) (merid a) ≡ m a
 open Suspension public
 ```
 
 ### Lemma 6.5.1
 
 ```
--- lemma6∙5∙1 : Susp 𝟚 ≃ S¹
--- lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
---   where
---     open S¹
+lemma6∙5∙1 : Susp 𝟚 ≃ S¹
+lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
+  where
+    open S¹
 
---     m : 𝟚 → base ≡ base
---     m true = refl
---     m false = loop
+    m : 𝟚 → base ≡ base
+    m true = refl
+    m false = loop
 
---     f : Susp 𝟚 → S¹
---     f s = rec-Susp base base m s
+    f : Susp 𝟚 → S¹
+    f s = rec-Susp base base m s
 
---     g : S¹ → Susp 𝟚
---     g s = rec-S¹ N (merid false ∙ sym (merid true)) s
+    g : S¹ → Susp 𝟚
+    g s = rec-S¹ N (merid false ∙ sym (merid true)) s
+      -- g : S¹ → Susp 𝟚
+      -- g base = N
+      -- g loop = (merid false ∙ sym (merid true))
     
---     forward : (f ∘ g) ∼ id
---     forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl {!  refl !} x
+    forward : (f ∘ g) ∼ id
+    forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl p x
+      where
+        p : refl ≡[ (λ x → f (g x) ≡ x) , loop ] refl
+        p = {!  merid true !}
     
---     backward : (g ∘ f) ∼ id
---     backward x = {!   !}
+    backward : (g ∘ f) ∼ id
+    backward x = ind-Susp {P = λ y → g (f y) ≡ y} refl (merid true) goal x
+      where
+        goal : (y : 𝟚) → transport (λ z → g (f z) ≡ z) (merid y) refl ≡ merid true
+
+        goal2 : (y : 𝟚) → {!   !} ∙ refl ∙ {!   !} ≡ merid true
+        goal y = {!   !}
+
 ```
+
+### Definition 6.5.2
+
+```
+module definition6∙5∙2 where
+  S[_] : ℕ → Set
+  S[ zero ] = 𝟚
+  S[ suc n ] = Susp (S[ n ])
+```
+
+### Lemma 6.5.3
+
+```
+Map* : {l : Level} → (A B : pointed l) → Set l
+Map* (A , a₀) (B , b₀) = Σ (A → B) (λ f → f a₀ ≡ b₀)
+```
+
+Adjoining a disjoint basepoint
+
+```
+module lol where
+  _₊ : {l : Level} → Set l → pointed l
+  A ₊ = A + Lift 𝟙 , inr (lift tt)
+```
+
+```
+open lol
+lemma6∙5∙3 : {l : Level} (A : Set l) → (B* @ (B , b₀) : pointed l)
+  → (Map* (A ₊) B*) ≃ (A → B)
+lemma6∙5∙3 A B* @ (B , b₀) = f , qinv-to-isequiv (mkQinv g forward {!   !})
+  where
+    f : Map* (A ₊) (B , b₀) → A → B
+    f (h , p) a = h (inl a)
+
+    g : (A → B) → Map* (A ₊) (B , b₀)
+    g h = p1 , refl
+      where
+        p1 : fst (A ₊) → B
+        p1 (inl x) = h x
+        p1 (inr x) = b₀
+
+    open axiom2∙9∙3
+
+    forward : (f ∘ g) ∼ id
+    forward f' = funext λ x → {!   !}
+      -- (x : A) (f' : A → B)
+      -- f (g (f' x)) ≡ f' x
+      -- f forgets the proof :(
+      -- g (f' x) gives us b₀
+```
+
+## 6.6 Cell complexes
+
+```
+```
+
+## 6.8 Pushouts
+
+```
+module Pushout where
+  postulate
+    Pushout : {A B C : Set} → (f : C → A) → (g : C → B) → Set
+
+  syntax Pushout A B C = A ⊔[ C ] B
+```

src/HottBook/Chapter7.lagda.md

@@ -2,6 +2,8 @@
   <summary>Imports</summary>
 
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter7 where
 
 open import HottBook.Chapter1
@@ -16,3 +18,25 @@ private
 
 </details>
 
+## 7.1 Definition of $n$-types
+
+### Definition 7.1.1
+
+```
+data ℕ' : Set where
+  negtwo : ℕ'
+  suc : ℕ' → ℕ'
+
+is_type : (n : ℕ') → Set → Set
+is negtwo type X = isContr X
+is suc n type X = (x y : X) → is n type (x ≡ y)
+```
+
+### Theorem 7.1.4
+
+```
+theorem7∙1∙4 : {X Y : Set} 
+  → (f : X → Y) → (n : ℕ') → is n type X → is n type Y
+theorem7∙1∙4 {X} {Y} f negtwo q = f (fst q) , λ y → {!   !}
+theorem7∙1∙4 {X} {Y} f (suc n) q = {!   !}
+```