From d9b9f37ee2cda05a635a38b2af6feedda5ea08ea Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 2 Jun 2024 18:13:09 -0400 Subject: [PATCH] converting primarily to cubical --- .vscode/settings.json | 3 +- Makefile | 5 +- html/Agda.css | 10 +- html/src/SUMMARY.md | 28 ++- src/CubicalHott/Chapter1.lagda.md | 85 ++++++- src/CubicalHott/Chapter2.lagda.md | 225 +++++++++++++++++++ src/CubicalHott/Chapter2Lemma221.lagda.md | 20 ++ src/CubicalHott/Chapter3.lagda.md | 10 +- src/CubicalHott/Chapter6.lagda.md | 16 +- src/CubicalHott/Primitives.agda | 6 + src/CubicalHott/Primitives/Interval.lagda.md | 83 +++++++ src/CubicalHott/Primitives/Kan.lagda.md | 48 ++++ src/CubicalHott/Primitives/Type.lagda.md | 36 +++ src/HottBook/Chapter1.lagda.md | 5 +- src/HottBook/Chapter2.lagda.md | 5 +- src/HottBook/Chapter6.lagda.md | 81 ------- src/HottBook/Chapter8.lagda.md | 33 --- src/VanDoornDissertation/HIT.lagda.md | 1 - 18 files changed, 546 insertions(+), 154 deletions(-) create mode 100644 src/CubicalHott/Chapter2Lemma221.lagda.md create mode 100644 src/CubicalHott/Primitives.agda create mode 100644 src/CubicalHott/Primitives/Interval.lagda.md create mode 100644 src/CubicalHott/Primitives/Kan.lagda.md create mode 100644 src/CubicalHott/Primitives/Type.lagda.md delete mode 100644 src/HottBook/Chapter6.lagda.md delete mode 100644 src/HottBook/Chapter8.lagda.md diff --git a/.vscode/settings.json b/.vscode/settings.json index 41a3d0e..9fb1700 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -2,5 +2,6 @@ "editor.unicodeHighlight.ambiguousCharacters": false, "gitdoc.enabled": false, "gitdoc.autoCommitDelay": 300000, - "gitdoc.commitMessageFormat": "'auto gitdoc commit'" + "gitdoc.commitMessageFormat": "'auto gitdoc commit'", + "agdaMode.connection.commandLineOptions": "--no-load-primitives" } diff --git a/Makefile b/Makefile index 8ffac85..044d83a 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,6 @@ GENDIR := html/src/generated build-to-html: find src \ -not \( -path src/Misc -prune \) \ - -not \( -path src/CubicalHott -prune \) \ \( -name "*.agda" -o -name "*.lagda.md" \) \ -print0 \ | rust-parallel -0 agda \ @@ -11,6 +10,7 @@ build-to-html: --html-dir=$(GENDIR) \ --allow-unsolved-metas \ --html-highlight=auto \ + --no-load-primitives \ || true fd --no-ignore "html$$" $(GENDIR) -x rm @@ -23,4 +23,5 @@ refresh-book: build-to-html deploy: build-book rsync -azr html/book/ root@veil:/home/blogDeploy/public/research -.PHONY: build-book build-to-html deploy \ No newline at end of file +.PHONY: build-book build-to-html deploy + # -not \( -path src/CubicalHott -prune \) \ \ No newline at end of file diff --git a/html/Agda.css b/html/Agda.css index 877db88..f87123e 100644 --- a/html/Agda.css +++ b/html/Agda.css @@ -1,9 +1,7 @@ -@media (prefers-color-scheme: light) { - :root { - --default-text: black; - --symbol: #404040; - --primitive: #0000CD; - } +:root { + --default-text: black; + --symbol: #404040; + --blue: #5175be; } @media (prefers-color-scheme: dark) { diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md index 03605c5..3b6c1ca 100644 --- a/html/src/SUMMARY.md +++ b/html/src/SUMMARY.md @@ -2,25 +2,23 @@ - [Front](./front.md) -# HoTT Book +# HoTT Book (Cubical formulation) -- [Chapter 1](./generated/HottBook.Chapter1.md) - - [Exercises](./generated/HottBook.Chapter1Exercises.md) -- [Chapter 2](./generated/HottBook.Chapter2.md) - - [Exercises](./generated/HottBook.Chapter2Exercises.md) -- [Chapter 3](./generated/HottBook.Chapter3.md) -- [Chapter 4](./generated/HottBook.Chapter4.md) -- [Chapter 5](./generated/HottBook.Chapter5.md) -- [Chapter 6](./generated/HottBook.Chapter6.md) -- [Chapter 7](./generated/HottBook.Chapter7.md) -- [Chapter 8](./generated/HottBook.Chapter8.md) -- [Chapter 9](./generated/HottBook.Chapter9.md) +- [Chapter 1](./generated/CubicalHott.Chapter1.md) +- [Chapter 2](./generated/CubicalHott.Chapter2.md) +- [Chapter 3](./generated/CubicalHott.Chapter3.md) +- [Chapter 4](./generated/CubicalHott.Chapter4.md) +- [Chapter 5](./generated/CubicalHott.Chapter5.md) +- [Chapter 6](./generated/CubicalHott.Chapter6.md) +- [Chapter 7](./generated/CubicalHott.Chapter7.md) +- [Chapter 8](./generated/CubicalHott.Chapter8.md) +- [Chapter 9](./generated/CubicalHott.Chapter9.md) # Individual lemmas -- [Lemma 2.2.1](./generated/HottBook.Chapter2Lemma221.md) -- [Definition 3.3.1](./generated/HottBook.Chapter3Definition331.md) -- [Lemma 3.3.3](./generated/HottBook.Chapter3Lemma333.md) +- [Lemma 2.2.1](./generated/CubicalHott.Chapter2Lemma221.md) +- [Definition 3.3.1](./generated/CubicalHott.Chapter3Definition331.md) +- [Lemma 3.3.3](./generated/CubicalHott.Chapter3Lemma333.md) # Van Doorn Dissertation diff --git a/src/CubicalHott/Chapter1.lagda.md b/src/CubicalHott/Chapter1.lagda.md index 717e257..7d5ba0b 100644 --- a/src/CubicalHott/Chapter1.lagda.md +++ b/src/CubicalHott/Chapter1.lagda.md @@ -2,21 +2,68 @@ {-# OPTIONS --cubical #-} module CubicalHott.Chapter1 where --- TODO: -open import Cubical.Core.Everything public +open import CubicalHott.Primitives public +``` + +## 1.4 Dependent function types (Ξ -types) + +``` +id : βˆ€ {l} {A : Type l} β†’ A β†’ A +id x = x +``` + +## 1.5 Product types + +``` +data πŸ™ : Type where + tt : πŸ™ ``` ## 1.7 Coproduct types ``` -data βŠ₯ {l : Level} : Type l where +record Ξ£ {β„“ β„“'} (A : Type β„“) (B : A β†’ Type β„“') : Type (β„“ βŠ” β„“') where + constructor _,_ + field + fst : A + snd : B fst + +open Ξ£ public + +{-# BUILTIN SIGMA Ξ£ #-} +``` + +Unit type: + +``` +record ⊀ : Type where + instance constructor tt +{-# BUILTIN UNIT ⊀ #-} +``` + +``` +data βŠ₯ {l} : Type l where +``` + +## 1.8 The type of booleans + +``` +data 𝟚 : Type where + true : 𝟚 + false : 𝟚 +``` + +``` +neg : 𝟚 β†’ 𝟚 +neg true = false +neg false = true ``` ## 1.11 Propositions as types ``` infix 3 Β¬_ -Β¬_ : βˆ€ {l : Level} (A : Set l) β†’ Set l +Β¬_ : βˆ€ {l} (A : Type l) β†’ Type l Β¬_ {l} A = A β†’ βŠ₯ {l} ``` @@ -36,4 +83,34 @@ refl {x = x} = to-path (Ξ» i β†’ x) ``` _β‰’_ : {A : Type} (x y : A) β†’ Type _β‰’_ x y = (p : x ≑ y) β†’ βŠ₯ +``` + +# Exercises + +## Exercise 1.1 + +Given functions f : A β†’ B and g : B β†’ C, define their composite g β—¦ f : A β†’ C. +Show that we have h β—¦ (g β—¦ f) ≑ (h β—¦ g) β—¦ f. + +``` +composite : {A B C : Type} + β†’ (f : A β†’ B) + β†’ (g : B β†’ C) + β†’ A β†’ C +composite f g x = g (f x) + +-- https://agda.github.io/agda-stdlib/master/Function.Base.html +infixr 9 _∘_ +_∘_ : {l1 l2 l3 : Level} {A : Type l1} {B : Type l2} {C : Type l3} + β†’ (g : B β†’ C) + β†’ (f : A β†’ B) + β†’ A β†’ C +_∘_ g f x = g (f x) + +composite-assoc : {A B C D : Type} + β†’ (f : A β†’ B) + β†’ (g : B β†’ C) + β†’ (h : C β†’ D) + β†’ h ∘ (g ∘ f) ≑ (h ∘ g) ∘ f +composite-assoc f g h = refl ``` \ No newline at end of file diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md index 49f9fdf..ac995cc 100644 --- a/src/CubicalHott/Chapter2.lagda.md +++ b/src/CubicalHott/Chapter2.lagda.md @@ -3,7 +3,232 @@ module CubicalHott.Chapter2 where open import CubicalHott.Chapter1 +open import CubicalHott.Chapter2Lemma221 public ``` ``` +``` + + +### Lemma 2.1.1 + +``` +sym : {l : Level} {A : Type l} {x y : A} β†’ (x ≑ y) β†’ y ≑ x +sym {l} {A} {x} {y} p i = p (~ i) +``` + +### Lemma 2.1.2 + +TODO: Read more about composition [here](https://1lab.dev/1Lab.Path.html#composition) + +``` +private + -- https://1lab.dev/1Lab.Reflection.Regularity.html#1191 + double-comp + : βˆ€ {β„“} {A : Type β„“} {w z : A} (x y : A) + β†’ w ≑ x β†’ x ≑ y β†’ y ≑ z + β†’ w ≑ z + double-comp x y p q r i = primHComp + (Ξ» { j (i = i0) β†’ p (~ j) ; j (i = i1) β†’ r j }) (q i) + +trans : βˆ€ {l} {A : Type l} {x y z : A} β†’ (x ≑ y) β†’ (y ≑ z) β†’ (x ≑ z) +trans {l} {A} {x} {y} {z} p q = double-comp x y refl p q + +infixr 30 _βˆ™_ +_βˆ™_ = trans +``` + +### Equational Reasoning + +``` +module ≑-Reasoning where + infix 1 begin_ + begin_ : {l : Level} {A : Type l} {x y : A} β†’ (x ≑ y) β†’ (x ≑ y) + begin x = x + + _β‰‘βŸ¨βŸ©_ : {l : Level} {A : Type l} (x {y} : A) β†’ x ≑ y β†’ x ≑ y + _ β‰‘βŸ¨βŸ© x≑y = x≑y + + infixr 2 _β‰‘βŸ¨βŸ©_ step-≑ + step-≑ : {l : Level} {A : Type l} (x {y z} : A) β†’ y ≑ z β†’ x ≑ y β†’ x ≑ z + step-≑ _ y≑z x≑y = trans x≑y y≑z + syntax step-≑ x y≑z x≑y = x β‰‘βŸ¨ x≑y ⟩ y≑z + + infix 3 _∎ + _∎ : {l : Level} {A : Type l} (x : A) β†’ (x ≑ x) + _ ∎ = refl +``` + +### Lemma 2.2.1 + +{{#include CubicalHott.Chapter2Lemma221.md:ap}} + +### Lemma 2.3.1 (Transport) + +``` +-- transport : {l₁ lβ‚‚ : Level} {A : Set l₁} {x y : A} +-- β†’ (P : A β†’ Set lβ‚‚) +-- β†’ (p : x ≑ y) +-- β†’ P x β†’ P y +-- transport {l₁} {lβ‚‚} {A} {x} {y} P refl = id + +transport : βˆ€ {l1 l2} {A : Type l1} {x y : A} + β†’ (P : A β†’ Type l2) β†’ (p : x ≑ y) β†’ P x β†’ P y +transport P p = transp (Ξ» i β†’ P (p i)) i0 +``` + +### Definition 2.4.1 (Homotopy) + +``` +infixl 18 _∼_ +_∼_ : {l₁ lβ‚‚ : Level} {A : Type l₁} {P : A β†’ Type lβ‚‚} + β†’ (f g : (x : A) β†’ P x) + β†’ Type (l₁ βŠ” lβ‚‚) +_∼_ {l₁} {lβ‚‚} {A} {P} f g = (x : A) β†’ f x ≑ g x +``` + +### Definition 2.4.6 + +``` +record qinv {l1 l2 : Level} {A : Type l1} {B : Type l2} (f : A β†’ B) : Type (l1 βŠ” l2) where + constructor mkQinv + field + g : B β†’ A + Ξ± : (f ∘ g) ∼ id + Ξ² : (g ∘ f) ∼ id +``` + +### Definition 2.4.10 + +``` +record isequiv {l1 l2 : Level} {A : Type l1} {B : Type l2} (f : A β†’ B) : Type (l1 βŠ” l2) where + eta-equality + constructor mkIsEquiv + field + g : B β†’ A + g-id : (f ∘ g) ∼ id + h : B β†’ A + h-id : (h ∘ f) ∼ id +``` + +``` +qinv-to-isequiv : {l1 l2 : Level} {A : Type l1} {B : Type l2} + β†’ {f : A β†’ B} + β†’ qinv f + β†’ isequiv f +qinv-to-isequiv (mkQinv g Ξ± Ξ²) = mkIsEquiv g Ξ± g Ξ² +``` + +Still kinda shaky on this one, TODO study it later: + +``` +isequiv-to-qinv : {l : Level} {A B : Type l} + β†’ {f : A β†’ B} + β†’ isequiv f + β†’ qinv f +isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) = + let + Ξ³ : g ∼ h + Ξ³ x = (sym (h-id (g x))) βˆ™ ap h (g-id x) + + Ξ² : (g ∘ f) ∼ id + Ξ² x = Ξ³ (f x) βˆ™ h-id x + in + mkQinv g g-id Ξ² +``` + +### Definition 2.4.11 + +``` +_≃_ : {l1 l2 : Level} β†’ (A : Type l1) (B : Type l2) β†’ Type (l1 βŠ” l2) +A ≃ B = Ξ£ (A β†’ B) isequiv +``` + +### Lemma 2.4.12 + +``` +module lemma2βˆ™4βˆ™12 where + id-equiv : {l : Level} β†’ (A : Type l) β†’ A ≃ A + id-equiv A = id , e + where + e : isequiv id + e = mkIsEquiv id (Ξ» _ β†’ refl) id (Ξ» _ β†’ refl) + + sym-equiv : {A B : Type} β†’ (f : A ≃ B) β†’ B ≃ A + sym-equiv {A} {B} (f , eqv) = + let (mkQinv g Ξ± Ξ²) = isequiv-to-qinv eqv + in g , qinv-to-isequiv (mkQinv f Ξ² Ξ±) + + trans-equiv : {A B C : Type} β†’ (f : A ≃ B) β†’ (g : B ≃ C) β†’ A ≃ C + trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) = + let + (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv + (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv + + open ≑-Reasoning + + forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id + forward c = + begin + ((g ∘ f) ∘ (f-inv ∘ g-inv)) c β‰‘βŸ¨ ap (Ξ» f β†’ f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩ + (g ∘ (f ∘ f-inv) ∘ g-inv) c β‰‘βŸ¨ ap g (f-inv-left (g-inv c)) ⟩ + (g ∘ id ∘ g-inv) c β‰‘βŸ¨βŸ© + (g ∘ g-inv) c β‰‘βŸ¨ g-inv-left c ⟩ + id c ∎ + + backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id + backward a = + begin + ((f-inv ∘ g-inv) ∘ (g ∘ f)) a β‰‘βŸ¨ ap (Ξ» f β†’ f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩ + (f-inv ∘ (g-inv ∘ (g ∘ f))) a β‰‘βŸ¨ ap f-inv (g-inv-right (f a)) ⟩ + (f-inv ∘ (id ∘ f)) a β‰‘βŸ¨βŸ© + (f-inv ∘ f) a β‰‘βŸ¨ f-inv-right a ⟩ + id a ∎ + + in ? + -- in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward) +``` + +## 2.10 Universes and the univalence axiom + +### Lemma 2.10.1 + +``` +idtoeqv : {l : Level} {A B : Type l} + β†’ (A ≑ B) + β†’ (A ≃ B) +idtoeqv {l} {A} {B} refl = lemma2βˆ™4βˆ™12.id-equiv A +``` + +### Axiom 2.10.3 (Univalence) + +``` +module axiom2βˆ™10βˆ™3 where + postulate + ua : {l : Level} {A B : Type l} β†’ (A ≃ B) β†’ (A ≑ B) + + forward : {l : Level} {A B : Type l} β†’ (eqv : A ≃ B) β†’ (idtoeqv ∘ ua) eqv ≑ eqv + -- forward eqv = {! !} + + backward : {l : Level} {A B : Type l} β†’ (p : A ≑ B) β†’ (ua ∘ idtoeqv) p ≑ p + -- backward p = {! !} + + ua-eqv : {l : Level} {A : Type l} {B : Type l} β†’ (A ≃ B) ≃ (A ≑ B) + ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward) + +open axiom2βˆ™10βˆ™3 hiding (forward; backward) +``` + +### Remark 2.12.6 + +``` +remark2βˆ™12βˆ™6 : true β‰’ false +remark2βˆ™12βˆ™6 p = genBot tt + where + Bmap : 𝟚 β†’ Type + Bmap true = πŸ™ + Bmap false = βŠ₯ + + genBot : πŸ™ β†’ βŠ₯ + genBot = transport Bmap p ``` \ No newline at end of file diff --git a/src/CubicalHott/Chapter2Lemma221.lagda.md b/src/CubicalHott/Chapter2Lemma221.lagda.md new file mode 100644 index 0000000..097be26 --- /dev/null +++ b/src/CubicalHott/Chapter2Lemma221.lagda.md @@ -0,0 +1,20 @@ +``` +{-# OPTIONS --cubical #-} +module CubicalHott.Chapter2Lemma221 where + +open import CubicalHott.Chapter1 +``` + +## Lemma 2.2.1 + +[//]: <> (ANCHOR: ap) + +``` +ap : {l1 l2 : Level} {A : Type l1} {B : Type l2} {x y : A} + β†’ (f : A β†’ B) + β†’ (p : x ≑ y) + β†’ f x ≑ f y +ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i) +``` + +[//]: <> (ANCHOR_END: ap) \ No newline at end of file diff --git a/src/CubicalHott/Chapter3.lagda.md b/src/CubicalHott/Chapter3.lagda.md index 9392dba..b0073ef 100644 --- a/src/CubicalHott/Chapter3.lagda.md +++ b/src/CubicalHott/Chapter3.lagda.md @@ -3,6 +3,7 @@ module CubicalHott.Chapter3 where open import CubicalHott.Chapter1 +open import CubicalHott.Chapter2 ``` ### Definition 3.1.1 @@ -19,10 +20,9 @@ example3βˆ™1βˆ™9 : {l : Level} β†’ Β¬ (isSet (Type l)) example3βˆ™1βˆ™9 p = {! !} where - open import Data.Bool - f : Bool β†’ Bool - f false = true - f true = false + lol : (x : 𝟚) β†’ neg (neg x) ≑ x + lol true = refl + lol false = refl ``` ### Definition 3.3.1 @@ -36,7 +36,7 @@ isProp P = (x y : P) β†’ x ≑ y ``` module section3βˆ™7 where - data βˆ₯_βˆ₯ (A : Set) : Set where + data βˆ₯_βˆ₯ (A : Type) : Type where ∣_∣ : (a : A) β†’ βˆ₯ A βˆ₯ witness : (x y : βˆ₯ A βˆ₯) β†’ x ≑ y open section3βˆ™7 diff --git a/src/CubicalHott/Chapter6.lagda.md b/src/CubicalHott/Chapter6.lagda.md index 0d06155..c62650a 100644 --- a/src/CubicalHott/Chapter6.lagda.md +++ b/src/CubicalHott/Chapter6.lagda.md @@ -3,6 +3,7 @@ module CubicalHott.Chapter6 where open import CubicalHott.Chapter1 +open import CubicalHott.Chapter2 ``` ## 6.4 Circles and spheres @@ -17,5 +18,18 @@ data SΒΉ : Type where ``` lemma6βˆ™4βˆ™1 : loop β‰’ refl -lemma6βˆ™4βˆ™1 p = {! !} +lemma6βˆ™4βˆ™1 p = + {! !} + where + open ≑-Reasoning + + f : {A : Type} (x : A) β†’ (p : x ≑ x) β†’ SΒΉ β†’ A + f x p base = x + f x p (loop i) = p i + + bad : {A : Type} (x : A) β†’ (p : x ≑ x) β†’ p ≑ refl + bad x p = begin + p β‰‘βŸ¨ {! !} ⟩ + p β‰‘βŸ¨ {! !} ⟩ + refl ∎ ``` \ No newline at end of file diff --git a/src/CubicalHott/Primitives.agda b/src/CubicalHott/Primitives.agda new file mode 100644 index 0000000..7de7b90 --- /dev/null +++ b/src/CubicalHott/Primitives.agda @@ -0,0 +1,6 @@ +{-# OPTIONS --cubical #-} +module CubicalHott.Primitives where + +open import CubicalHott.Primitives.Interval public +open import CubicalHott.Primitives.Kan public +open import CubicalHott.Primitives.Type public \ No newline at end of file diff --git a/src/CubicalHott/Primitives/Interval.lagda.md b/src/CubicalHott/Primitives/Interval.lagda.md new file mode 100644 index 0000000..a71543f --- /dev/null +++ b/src/CubicalHott/Primitives/Interval.lagda.md @@ -0,0 +1,83 @@ +``` +{-# OPTIONS --cubical #-} +module CubicalHott.Primitives.Interval where + +open import CubicalHott.Primitives.Type +``` + +The interval type, and its associated operations, are also very magical. + +``` +{-# BUILTIN CUBEINTERVALUNIV IUniv #-} -- IUniv : SSet₁ +{-# BUILTIN INTERVAL I #-} -- I : IUniv +``` + +Note that the interval (as of Agda 2.6.3) is in its own sort, IUniv. The reason for this is that the interval can serve as the domain of fibrant types: + +``` +_ : Type β†’ Type +_ = Ξ» A β†’ (I β†’ A) +``` + +The interval has two endpoints, the builtins IZERO and IONE: + +``` +{-# BUILTIN IZERO i0 #-} +{-# BUILTIN IONE i1 #-} +``` + +It also supports a De Morgan algebra structure. Unlike the other built-in symbols, the operations on the interval are defined as primitive, so we must use renaming to give them usable names. + +``` +private module X where + infix 30 primINeg + infixr 20 primIMin primIMax + primitive + primIMin : I β†’ I β†’ I + primIMax : I β†’ I β†’ I + primINeg : I β†’ I +open X public + renaming ( primIMin to _∧_ + ; primIMax to _∨_ + ; primINeg to ~_ + ) +``` + +The IsOne predicate + +To specify the shape of composition problems, Cubical Agda gives us the predicate IsOne, which can be thought of as an embedding Iβ†ͺΞ© of the interval object into the subobject classifier. Of course, we have that IsOne i0 is uninhabited (since 0 is not 1), but note that assuming a term in IsOne i0 collapses the judgemental equality. + +``` +{-# BUILTIN ISONE IsOne #-} -- IsOne : I β†’ SetΟ‰ + +postulate + 1=1 : IsOne i1 + leftIs1 : βˆ€ i j β†’ IsOne i β†’ IsOne (i ∨ j) + rightIs1 : βˆ€ i j β†’ IsOne j β†’ IsOne (i ∨ j) + +{-# BUILTIN ITISONE 1=1 #-} +{-# BUILTIN ISONE1 leftIs1 #-} +{-# BUILTIN ISONE2 rightIs1 #-} +``` + +The IsOne proposition is used as the domain of the type Partial, where Partial Ο† A is a refinement of the type .(IsOne Ο†) β†’ A1, where inhabitants p, q : Partial Ο† A are equal iff they agree on a decomposition of Ο† into DNF. + +``` +{-# BUILTIN PARTIAL Partial #-} +{-# BUILTIN PARTIALP PartialP #-} + +postulate + isOneEmpty : βˆ€ {β„“} {A : Partial i0 (Type β„“)} β†’ PartialP i0 A + +primitive + primPOr : βˆ€ {β„“} (i j : I) {A : Partial (i ∨ j) (Type β„“)} + β†’ (u : PartialP i (Ξ» z β†’ A (leftIs1 i j z))) + β†’ (v : PartialP j (Ξ» z β†’ A (rightIs1 i j z))) + β†’ PartialP (i ∨ j) A + +{-# BUILTIN ISONEEMPTY isOneEmpty #-} + +syntax primPOr Ο† ψ u v = [ Ο† ↦ u , ψ ↦ v ] +``` + +Note that the type of primPOr is incomplete: it looks like the eliminator for a coproduct, but i ∨ j behaves more like a pushout. We can represent the accurate type with extension types. \ No newline at end of file diff --git a/src/CubicalHott/Primitives/Kan.lagda.md b/src/CubicalHott/Primitives/Kan.lagda.md new file mode 100644 index 0000000..7e4419c --- /dev/null +++ b/src/CubicalHott/Primitives/Kan.lagda.md @@ -0,0 +1,48 @@ +``` +{-# OPTIONS --cubical #-} +module CubicalHott.Primitives.Kan where + +open import CubicalHott.Primitives.Type +open import CubicalHott.Primitives.Interval + +private module X where primitive + primTransp : βˆ€ {β„“} (A : (i : I) β†’ Type (β„“ i)) (Ο† : I) (a : A i0) β†’ A i1 + primHComp : βˆ€ {β„“} {A : Type β„“} {Ο† : I} (u : βˆ€ i β†’ Partial Ο† A) (a : A) β†’ A + primComp : βˆ€ {β„“} (A : (i : I) β†’ Type (β„“ i)) {Ο† : I} (u : βˆ€ i β†’ Partial Ο† (A i)) (a : A i0) β†’ A i1 + +open X public renaming (primTransp to transp) + +hcomp + : βˆ€ {β„“} {A : Type β„“} (Ο† : I) + β†’ (u : (i : I) β†’ Partial (Ο† ∨ ~ i) A) + β†’ A +hcomp Ο† u = X.primHComp (Ξ» j .o β†’ u j (leftIs1 Ο† (~ j) o)) (u i0 1=1) + +βˆ‚ : I β†’ I +βˆ‚ i = i ∨ ~ i + +comp + : βˆ€ {β„“ : I β†’ Level} (A : (i : I) β†’ Type (β„“ i)) (Ο† : I) + β†’ (u : (i : I) β†’ Partial (Ο† ∨ ~ i) (A i)) + β†’ A i1 +comp A Ο† u = X.primComp A (Ξ» j .o β†’ u j (leftIs1 Ο† (~ j) o)) (u i0 1=1) +``` + +We also define the type of dependent paths, and of non-dependent paths. + +``` +postulate + PathP : βˆ€ {β„“} (A : I β†’ Type β„“) β†’ A i0 β†’ A i1 β†’ Type β„“ + +{-# BUILTIN PATHP PathP #-} + +infix 4 _≑_ + +Path : βˆ€ {β„“} (A : Type β„“) β†’ A β†’ A β†’ Type β„“ +Path A = PathP (Ξ» i β†’ A) + +_≑_ : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ A β†’ Type β„“ +_≑_ {A = A} = Path A + +{-# BUILTIN PATH _≑_ #-} +``` diff --git a/src/CubicalHott/Primitives/Type.lagda.md b/src/CubicalHott/Primitives/Type.lagda.md new file mode 100644 index 0000000..a1a87dd --- /dev/null +++ b/src/CubicalHott/Primitives/Type.lagda.md @@ -0,0 +1,36 @@ +``` +{-# OPTIONS --cubical #-} +module CubicalHott.Primitives.Type where +``` + +Primitives: Sorts + +This module defines bindings for the primitive sorts in Agda. These are very magic symbols since they bootstrap everything about the type system. For more details about the use of universes, see 1Lab.Type. + +``` +{-# BUILTIN TYPE Type #-} +{-# BUILTIN SETOMEGA TypeΟ‰ #-} + +{-# BUILTIN PROP Prop #-} +{-# BUILTIN PROPOMEGA PropΟ‰ #-} + +{-# BUILTIN STRICTSET SSet #-} +{-# BUILTIN STRICTSETOMEGA SSetΟ‰ #-} +``` + +Additionally, we have the Level type, of universe levels. The universe levels are an algebra containing 0, closed under successor and maximum. The difference between this and e.g. the natural numbers is that Level isn’t initial, i.e. you can’t pattern-match on it. + +``` +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 _βŠ”_ #-} +``` diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 507c31e..768f557 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -4,7 +4,8 @@ ``` module HottBook.Chapter1 where -open import Agda.Primitive +open import Agda.Primitive public +open import Agda.Primitive.Cubical public ``` @@ -204,7 +205,7 @@ composite-assoc f g h = refl ## Exercise 1.14 Why do the induction principles for identity types not allow us to construct a -function $f : \prod_{x:A} \prod_{p:x \equiv x}(p \equiv \refl_x)$ with the defining equation $f (x, \refl_x) :≑ \refl_{\refl_x}$ ? +function $f : \prod_{x:A} \prod_{p:x \equiv x}(p \equiv \refl_x)$ with the defining equation $f (x, \refl_x) :\equiv \refl_{\refl_x}$ ? Under non-UIP systems, there are identity types that are different from refl, and this ability gives us higher dimensional paths. Otherwise, we would be diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 9a24e62..35e6bbc 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -4,8 +4,8 @@ ``` module HottBook.Chapter2 where -open import Agda.Primitive -open import HottBook.Chapter1 +open import Agda.Primitive.Cubical hiding (i1) +open import HottBook.Chapter1 hiding (i1) open import HottBook.Chapter2Lemma221 public open import HottBook.Util ``` @@ -513,7 +513,6 @@ module theorem2βˆ™6βˆ™2 where forward : (pair-≑ ∘ definition2βˆ™6βˆ™1) ∼ id forward refl = refl - open theorem2βˆ™6βˆ™2 using (pair-≑) ``` diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md deleted file mode 100644 index 74731f1..0000000 --- a/src/HottBook/Chapter6.lagda.md +++ /dev/null @@ -1,81 +0,0 @@ -``` -module HottBook.Chapter6 where - -open import HottBook.Chapter1 -open import HottBook.Chapter2 -``` - -# 6 Higher inductive types - -### Definition 6.2.2 (Dependent paths) - -``` -definition6βˆ™2βˆ™2 : {A : Set} - β†’ (P : A β†’ Set) - β†’ {x y : A} - β†’ (p : x ≑ y) - β†’ (u : P x) β†’ (v : P y) β†’ Set -definition6βˆ™2βˆ™2 P p u v = transport P p u ≑ v - -syntax definition6βˆ™2βˆ™2 P p u v = u ≑[ P , p ] v -``` - -Circle definition - -``` -postulate - SΒΉ : Set - base : SΒΉ - loop : base ≑ base - SΒΉ-elim : (P : SΒΉ β†’ Set) - β†’ (p-base : P base) - β†’ (p-loop : p-base ≑[ P , loop ] p-base) - β†’ (x : SΒΉ) β†’ P x -``` - -### Lemma 6.2.5 - -``` -lemma6βˆ™2βˆ™5 : {A : Set} β†’ (a : A) β†’ (p : a ≑ a) β†’ SΒΉ β†’ A -lemma6βˆ™2βˆ™5 {A} a p circ = SΒΉ-elim P p-base p-loop circ - where - P : SΒΉ β†’ Set - P _ = A - - p-base : P base - p-base = a - - p-loop : a ≑[ P , loop ] a - p-loop = transportconst A loop a βˆ™ p -``` - -### Lemma 6.2.8 - -``` --- TODO: Finish this -postulate - lemma6βˆ™2βˆ™8 : {A : Set} {f g : SΒΉ β†’ A} - β†’ (p : f base ≑ g base) - β†’ (q : (ap f loop) ≑[ (Ξ» x β†’ x ≑ x) , p ] (ap g loop)) - β†’ (x : SΒΉ) β†’ f x ≑ g x --- lemma6βˆ™2βˆ™8 {A} {f} {g} p q = SΒΉ-elim (Ξ» x β†’ f x ≑ g x) p {! !} -``` - -## 6.3 The interval - -``` -postulate - I : Set - 0I : I - 1I : I - seg : 0I ≑ 1I -``` - -## 6.10 Quotients - -``` --- module Quotient (A : Set) (R : A Γ— A β†’ Prop) where --- postulate --- _/_ : Set β†’ Set β†’ Set --- q : (A : Set) β†’ A / A -``` \ No newline at end of file diff --git a/src/HottBook/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md deleted file mode 100644 index 177bb1d..0000000 --- a/src/HottBook/Chapter8.lagda.md +++ /dev/null @@ -1,33 +0,0 @@ -``` -module HottBook.Chapter8 where - -open import Agda.Primitive -open import HottBook.Chapter1 -open import HottBook.Chapter2 -open import HottBook.Chapter6 -``` - -### Definition 8.0.1 - -``` --- TODO: Finish -postulate - Ο€ : (n : β„•) β†’ (A : Set) β†’ (a : A) β†’ Set -``` - -## 8.1 π₁(SΒΉ) - -### Definition 8.1.1 - -``` -data β„€ : Set where -``` - -``` --- code : {l : Level} β†’ SΒΉ β†’ Set (lsuc l) --- code {l} = SΒΉ-elim (Ξ» _ β†’ Set l) β„€ (ua suc) -``` - -## 8.7 The van Kampen theorem - -### 8.7.1 Naive van Kampen diff --git a/src/VanDoornDissertation/HIT.lagda.md b/src/VanDoornDissertation/HIT.lagda.md index c65b905..b6289b6 100644 --- a/src/VanDoornDissertation/HIT.lagda.md +++ b/src/VanDoornDissertation/HIT.lagda.md @@ -2,7 +2,6 @@ module VanDoornDissertation.HIT where open import HottBook.Chapter1 --- open import VanDoornDissertation.Preliminaries ``` # 3 Higher Inductive Types