From 21b96f236c9f8e2a8454fddcd744181a133fc024 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 14 Jul 2024 12:54:06 -0400 Subject: [PATCH] 6.3.2 --- src/CubicalHott/Chapter2.lagda.md | 8 +++ src/CubicalHott/Chapter6.lagda.md | 18 ++++++ src/HottBook/Chapter2.lagda.md | 2 + src/HottBook/Chapter3.lagda.md | 4 +- src/HottBook/Chapter6.lagda.md | 97 +++++++++++++++++++++---------- 5 files changed, 98 insertions(+), 31 deletions(-) diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md index 72dc340..7d42e18 100644 --- a/src/CubicalHott/Chapter2.lagda.md +++ b/src/CubicalHott/Chapter2.lagda.md @@ -59,6 +59,14 @@ module ≡-Reasoning where _ ∎ = refl ``` +### Lemma 2.1.4 + +``` +module lemma2∙1∙4 {l : Level} {A : Type l} where + iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p + iii {x} {y} p i j = p j +``` + ### Lemma 2.2.1 {{#include CubicalHott.Chapter2Lemma221.md:ap}} diff --git a/src/CubicalHott/Chapter6.lagda.md b/src/CubicalHott/Chapter6.lagda.md index 7903742..38ef916 100644 --- a/src/CubicalHott/Chapter6.lagda.md +++ b/src/CubicalHott/Chapter6.lagda.md @@ -4,6 +4,10 @@ module CubicalHott.Chapter6 where open import CubicalHott.Chapter1 open import CubicalHott.Chapter2 + +private + variable + l : Level ``` ## 6.3 The interval @@ -18,7 +22,21 @@ data Iv : Type where ### Lemma 6.3.1 ``` +isContr : (A : Type l) → Type l +isContr A = Σ A (λ a → (x : A) → a ≡ x) + lemma6∙3∙1 : isContr Iv +lemma6∙3∙1 = 1I , f + where + f : (x : Iv) → 1I ≡ x + f 0I = sym seg + f 1I = refl + f (seg i) j = {! !} +``` + +### Lemma 6.3.2 + +``` ``` ## 6.4 Circles and spheres diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index acde53e..821c90a 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -185,6 +185,8 @@ transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A} → (b : B) → transport (λ _ → B) p b ≡ b transportconst {l₁} {l₂} {A} {x} {y} B refl b = refl + +{-# REWRITE transportconst #-} ``` ### Equation 2.3.6 diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 1116007..96a8725 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -481,7 +481,9 @@ Principle of unique choice -- → ((x : A) → isProp (P x)) -- → ((x : A) → ∥ P x ∥) -- → (x : A) → P x --- corollary3∙9∙2 assump1 assump2 x = {! !} +-- corollary3∙9∙2 {A = A} {P = P} assump1 assump2 x = +-- let rec = trunc-rec A (assump1 x) (λ y → {!assump2 x !}) (∣ x ∣) +-- in rec ``` ## 3.11 Contractibility diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md index b3b2631..dbdf1b0 100644 --- a/src/HottBook/Chapter6.lagda.md +++ b/src/HottBook/Chapter6.lagda.md @@ -31,25 +31,60 @@ syntax dep-path P p u v = u ≡[ P , p ] v ## 6.3 The interval ``` -postulate +module Interval where + data #I : Set where + #0 : #I + #1 : #I + I : Set + I = #I + 0I : I + 0I = #0 + 1I : I - seg : 0I ≡ 1I + 1I = #1 -record I-rec (B : Set) (b0 b1 : B) (s : b0 ≡ b1) : Set where - field - f : I → B - prop1 : f 0I ≡ b0 - prop2 : f 1I ≡ b1 - prop3 : apd f seg ≡ {! s !} + postulate + seg : 0I ≡ 1I -record I-ind (P : I → Set) (b0 : P 0I) (b1 : P 1I) (s : b0 ≡[ P , seg ] b1) : Set where - field - f : (x : I) → P x - prop1 : f 0I ≡ b0 - prop2 : f 1I ≡ b1 - prop3 : apd f seg ≡ {! s !} + postulate + rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B + + rec-Interval-1 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 0I ≡ b₀ + rec-Interval-2 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 1I ≡ b₁ + + {-# REWRITE rec-Interval-1 #-} + {-# REWRITE rec-Interval-2 #-} + + postulate + rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s + {-# REWRITE rec-Interval-3 #-} +open Interval public +``` + +### Lemma 6.3.1 + +``` +lemma6∙3∙1 : isContr I +lemma6∙3∙1 = 1I , f + where + f : (x : I) → 1I ≡ x + f #0 = sym seg + f #1 = refl +``` + +### Lemma 6.3.2 + +``` +lemma6∙3∙2 : {A B : Set} {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g +lemma6∙3∙2 {A = A} {B = B} {f = f} {g = g} p = apd q seg + where + p' : (x : A) → I → B + p' x = rec-Interval (f x) (g x) (p x) + + q : I → (A → B) + q i x = p' x i ``` ## 6.4 Circles and sphere @@ -72,28 +107,30 @@ S¹-rec : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → ( S¹-rec b l #base = b postulate - S¹-rec-loop : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → apd (S¹-rec b l) loop ≡ l + S¹-rec-loop : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (S¹-rec b l) loop ≡ l + +{-# REWRITE S¹-rec-loop #-} ``` ### Lemma 6.4.1 ``` -lemma6∙4∙1 : loop ≢ refl -lemma6∙4∙1 loop≡refl = - {! !} - where - f : {A : Set} {x : A} {p : x ≡ x} → (S¹ → A) - f {A = A} {x = x} {p = p} s = - let p' = transportconst A loop x - in (S¹-rec x (p' ∙ p)) s - f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p - f-loop {x = x} = S¹-rec-loop x ? +-- lemma6∙4∙1 : loop ≢ refl +-- lemma6∙4∙1 loop≡refl = +-- {! !} +-- where +-- f : {A : Set} {x : A} {p : x ≡ x} → (S¹ → A) +-- f {A = A} {x = x} {p = p} s = +-- let p' = transportconst A loop x +-- in (S¹-rec x (p' ∙ p)) s +-- -- f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p +-- -- f-loop {x = x} = S¹-rec-loop x ? - goal : ⊥ +-- goal : ⊥ - goal2 : (A : Set l) (a : A) (p : a ≡ a) → isSet A - goal = example3∙1∙9 (goal2 {! !} {! !} {! !}) +-- goal2 : (A : Set l) (a : A) (p : a ≡ a) → isSet A +-- goal = example3∙1∙9 (goal2 {! !} {! !} {! !}) - -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl - goal2 A a p x y r s = {! !} +-- -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl +-- goal2 A a p x y r s = {! !} ``` \ No newline at end of file