From 3ce217e319d9012c4f1bc4641674c2a24d1d4e00 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 30 May 2024 15:22:43 -0500 Subject: [PATCH] 2.12.5 --- src/HottBook/Chapter1.lagda.md | 27 ++++++++++++--- src/HottBook/Chapter2.lagda.md | 62 ++++++++++++++++++++++++++++------ src/HottBook/Primitives.agda | 21 ++++++++++++ 3 files changed, 94 insertions(+), 16 deletions(-) create mode 100644 src/HottBook/Primitives.agda diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 16b7864..9ee31a6 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -1,9 +1,16 @@ +
+ Imports + ``` module HottBook.Chapter1 where open import Agda.Primitive ``` +
+ +# 1 Type theory + ## 1.1 Type theory versus set theory ## 1.2 Function types @@ -67,7 +74,7 @@ _×_ A B = Σ A (λ _ → B) ``` infixl 6 _+_ -data _+_ (A B : Set) : Set where +data _+_ {l : Level} (A B : Set l) : Set l where inl : A → A + B inr : B → A + B ``` @@ -86,9 +93,9 @@ rec-+ C f g (inr x) = g x ``` ``` -data ⊥ : Set where +data ⊥ {l : Level} : Set l where -rec-⊥ : {C : Set} → (x : ⊥) → C +rec-⊥ : {l : Level} → {C : Set l} → (x : ⊥ {l}) → C rec-⊥ {C} () ``` @@ -123,8 +130,8 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n) ``` infix 3 ¬_ -¬_ : {l : Level} (A : Set l) → Set l -¬ A = A → ⊥ +¬_ : {l : Level} → (A : Set l) → Set l +¬_ {l} A = A → ⊥ {l} ``` ## 1.12 Identity types @@ -152,6 +159,16 @@ J : {l₁ l₂ : Level} {A : Set l₁} J C c x x refl = c x ``` +Based path induction: + +``` +based-path-induction : {l1 l2 : Level} {A : Set l1} (a : A) + → (C : (x : A) → (a ≡ x) → Set l2) + → (c : C a refl) + → (x : A) → (p : a ≡ x) → C x p +based-path-induction a C c x refl = c +``` + # Exercises ## Exercise 1.1 diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 9209779..6248f85 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -65,7 +65,7 @@ module ≡-Reasoning where ### Lemma 2.1.4 ``` -module lemma2∙1∙4 {A : Set} where +module lemma2∙1∙4 {l : Level} {A : Set l} where i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl i1 {x} {y} p = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p @@ -85,7 +85,7 @@ module lemma2∙1∙4 {A : Set} where iv {x} {y} {z} {w} p q r = let open ≡-Reasoning - C : (x y : A) → (p : x ≡ y) → Set + C : (x y : A) → (p : x ≡ y) → Set l C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r c : (x : A) → C x x refl @@ -254,9 +254,9 @@ lemma2∙3∙9 {A} {x} {y} {z} P p q u = ### Lemma 2.3.10 ``` -lemma2∙3∙10 : {l : Level} {A B : Set (lsuc l)} +lemma2∙3∙10 : {l1 l2 : Level} {A B : Set l1} → (f : A → B) - → (P : B → Set l) + → (P : B → Set l2) → {x y : A} → (p : x ≡ y) → (u : P (f x)) @@ -768,32 +768,32 @@ open axiom2∙10∙3 ### Theorem 2.11.2 ``` -module theorem2∙11∙2 where +module lemma2∙11∙2 where open ≡-Reasoning - i : {A : Set} {a x1 x2 : A} + i : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : a ≡ x1) → transport (λ y → a ≡ y) p q ≡ q ∙ p - i {A} {a} {x1} {x2} p q = + i {l} {A} {a} {x1} {x2} p q = J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1) (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → lemma2∙1∙4.i1 q1) a x3 q1) x1 x2 p q - ii : {A : Set} {a x1 x2 : A} + ii : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : x1 ≡ a) → transport (λ y → y ≡ a) p q ≡ sym p ∙ q - ii {A} {a} {x1} {x2} p q = + ii {l} {A} {a} {x1} {x2} p q = J (λ x y p → (q1 : x ≡ a) → transport (λ y → y ≡ a) p q1 ≡ sym p ∙ q1) (λ x q1 → J (λ x y p → transport (λ y → y ≡ a) refl q1 ≡ sym refl ∙ q1) (λ x → lemma2∙1∙4.i2 q1) x a q1) x1 x2 p q - iii : {A : Set} {a x1 x2 : A} + iii : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : x1 ≡ x1) → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p - iii {A} {a} {x1} {x2} p q = + iii {l} {A} {a} {x1} {x2} p q = J (λ x y p → (q1 : x ≡ x) → transport (λ y → y ≡ y) p q1 ≡ sym p ∙ q1 ∙ p) (λ x q1 → J (λ x y p → transport (λ y → y ≡ y) refl q1 ≡ sym refl ∙ q1 ∙ refl) (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper) @@ -845,8 +845,48 @@ theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} p q = a a' p q ``` +### Theorem 2.11.5 + +``` +-- theorem2∙11∙5 : {A : Set} {a a' : A} +-- → (p : a ≡ a') +-- → (q : a ≡ a) +-- → (r : a' ≡ a') +-- → (transport (λ y → y ≡ y) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r) +``` + ## 2.12 Coproducts +### Theorem 2.12.5 + +``` +module 2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where + code : A + B → Set l + code (inl a) = a₀ ≡ a + code (inr b) = ⊥ + + encode : (x : A + B) → (p : inl a₀ ≡ x) → code x + encode x p = transport code p refl + + decode : (x : A + B) → code x → inl a₀ ≡ x + decode (inl x) c = ap inl c + + backward : (x : A + B) → (c : code x) → encode x (decode x c) ≡ c + backward (inl x) c = + let open ≡-Reasoning in begin + encode (inl x) (decode (inl x) c) ≡⟨⟩ + transport code (ap inl c) refl ≡⟨ sym (lemma2∙3∙10 inl code c refl) ⟩ + transport (λ a → a₀ ≡ a) c refl ≡⟨ lemma2∙11∙2.i c refl ⟩ + refl ∙ c ≡⟨ sym (lemma2∙1∙4.i2 c) ⟩ + c ∎ + + forward : (x : A + B) → (p : inl a₀ ≡ x) → decode x (encode x p) ≡ p + forward x p = based-path-induction (inl a₀) (λ x1 p1 → decode x1 (encode x1 p1) ≡ p1) refl x p + + theorem2∙12∙5 : (x : A + B) → (inl a₀ ≡ x) ≃ (code x) + theorem2∙12∙5 x = encode x , qinv-to-isequiv (mkQinv (decode x) (backward x) (forward x)) +``` + ### Remark 2.12.6 ``` diff --git a/src/HottBook/Primitives.agda b/src/HottBook/Primitives.agda new file mode 100644 index 0000000..ea545c7 --- /dev/null +++ b/src/HottBook/Primitives.agda @@ -0,0 +1,21 @@ +module HottBook.Primitives where + +{-# BUILTIN TYPE Type #-} +{-# BUILTIN SETOMEGA Typeω #-} +{-# BUILTIN PROP Prop #-} +{-# BUILTIN PROPOMEGA Propω #-} +{-# BUILTIN STRICTSET SType #-} +{-# BUILTIN STRICTSETOMEGA STypeω #-} + +postulate + Level : Type + lzero : Level + lsuc : Level → Level + _⊔_ : Level → Level → Level +infixl 6 _⊔_ + +{-# BUILTIN LEVELUNIV LevelUniv #-} +{-# BUILTIN LEVEL Level #-} +{-# BUILTIN LEVELZERO lzero #-} +{-# BUILTIN LEVELSUC lsuc #-} +{-# BUILTIN LEVELMAX _⊔_ #-} \ No newline at end of file