From 27524b92506b5401a550dc0e01a45feeccfa8cd1 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 10 Jul 2024 23:03:58 -0500 Subject: [PATCH] update --- src/CubicalHott/Chapter1.lagda.md | 5 +++ src/HottBook/Chapter2Exercises.lagda.md | 22 +++++++++--- src/HottBook/Chapter4.lagda.md | 19 +++++++--- .../Preliminaries.lagda.md | 35 ++++++++++++++++++- 4 files changed, 70 insertions(+), 11 deletions(-) diff --git a/src/CubicalHott/Chapter1.lagda.md b/src/CubicalHott/Chapter1.lagda.md index afec5ac..b8d802d 100644 --- a/src/CubicalHott/Chapter1.lagda.md +++ b/src/CubicalHott/Chapter1.lagda.md @@ -32,6 +32,11 @@ open Σ public {-# BUILTIN SIGMA Σ #-} infixr 4 _,_ + +syntax Σ A (λ x → B) = Σ[ x ∈ A ] B + +_×_ : {l : Level} (A B : Type l) → Type l +_×_ A B = Σ A (λ _ → B) ``` Unit type: diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index 2166a7a..5b6bae5 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -167,9 +167,21 @@ TODO: Generalizing to dependent functions. ## Exercise 2.10 ``` -postulate - exercise2∙10 : {A : Set} {B : A → Set} {C : Σ A B → Set} - → Σ A (λ x → Σ (B x) (λ y → C (x , y))) ≃ Σ (Σ A B) (λ p → C p) +exercise2∙10 : {A : Set} {B : A → Set} {C : Σ A B → Set} + → (Σ A (λ x → Σ (B x) (λ y → C (x , y)))) ≃ Σ (Σ A B) C +exercise2∙10 {A} {B} {C} = f , qinv-to-isequiv (mkQinv g f-g g-f) + where + f : (Σ A (λ x → Σ (B x) (λ y → C (x , y)))) → Σ (Σ A B) C + f (x , (y , cxy)) = (x , y) , cxy + + g : Σ (Σ A B) C → (Σ A (λ x → Σ (B x) (λ y → C (x , y)))) + g ((x , y) , cxy) = x , (y , cxy) + + f-g : (f ∘ g) ∼ id + f-g ((x , y) , cxy) = refl + + g-f : (g ∘ f) ∼ id + g-f (x , (y , cxy)) = refl ``` ## Exercise 2.13 @@ -311,5 +323,5 @@ module exercise2∙17 where B-id = ua B-eqv combined-id = pair-≡ A-id B-id - in idtoeqv combined-id -``` \ No newline at end of file + in idtoeqv combined-id +``` \ No newline at end of file diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md index 1bcb079..4ffd44f 100644 --- a/src/HottBook/Chapter4.lagda.md +++ b/src/HottBook/Chapter4.lagda.md @@ -82,12 +82,18 @@ lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {! !}) , {! !} There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition. ``` -theorem4∙1∙3 : ∀ {l} {A B : Set l} - → Σ (A → B) (λ f → isProp (qinv f) → ⊥) -theorem4∙1∙3 = {! !} , {! !} - where - goal : Σ (Set (lsuc l)) (λ X → isProp ((x : X) → x ≡ x) → ⊥) +theorem4∙1∙3 : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥))) +-- theorem4∙1∙3 {l} = goal +-- where +-- goal : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥))) +-- goal2 : ∀ {l} → Σ (Set l) (λ X → isProp ((x : X) → x ≡ x) → ⊥) +-- goal {l} = Σ.fst (goal2 {l}) , {! !} , {! !} , {! !} + +-- X : ∀ {l} → Set (lsuc l) +-- X {l} = Σ (Set l) (λ A → ∥ Lift 𝟚 ≡ A ∥) + +-- goal2 {l} = X {l} , ? ``` ## 4.2 Half adjoint equivalences @@ -106,6 +112,9 @@ record ishae {A B : Set} (f : A → B) : Set where ### Lemma 4.2.2 +``` +``` + ### Theorem 4.2.3 ``` diff --git a/src/VanDoornDissertation/Preliminaries.lagda.md b/src/VanDoornDissertation/Preliminaries.lagda.md index 51014f8..f3be99e 100644 --- a/src/VanDoornDissertation/Preliminaries.lagda.md +++ b/src/VanDoornDissertation/Preliminaries.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --cubical --no-load-primitives #-} module VanDoornDissertation.Preliminaries where open import CubicalHott.Chapter1 @@ -57,4 +57,37 @@ Square p q s r = PathP (λ i → p i ≡ r i) q s ``` +``` + +### 2.2.5 Pointed Types + +#### Definition 2.2.6 + +``` +data pointed (A : Type) : Type where + mkPointed : (a₀ : A) → pointed A + +1-is-pointed : pointed 𝟙 +1-is-pointed = mkPointed tt + +2-is-pointed : pointed 𝟚 +2-is-pointed = mkPointed false + +S⁰ = 2-is-pointed + +_×_-is-pointed : {A B : Type} → pointed A → pointed B → pointed (A × B) +_×_-is-pointed {A} {B} (mkPointed a₀) (mkPointed b₀) = mkPointed (a₀ , b₀) +``` + +### 2.2.6 Higher inductive types + +``` +data Interval : Type where + 0I : Interval + 1I : Interval + seg : 0I ≡ 1I + +data Quotient (A : Type) (R : A → A → Type) : Type where + x : A → Quotient A R + glue : (a a' : A) → R a a' → x a ≡ x a' ``` \ No newline at end of file