michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

converting primarily to cubical

Browse source
This commit is contained in:
Michael Zhang 2024-06-02 18:13:09 -04:00
parent e48922ebc5
commit d9b9f37ee2
18 changed files with 546 additions and 154 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.vscode/settings.json vendored
View file

@ -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"
}

5
Makefile
View file

@ -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
.PHONY: build-book build-to-html deploy
# -not \( -path src/CubicalHott -prune \) \

10
html/Agda.css
View file

@ -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) {

28
html/src/SUMMARY.md
View file

@ -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

85
src/CubicalHott/Chapter1.lagda.md
View file

@ -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
```

225
src/CubicalHott/Chapter2.lagda.md
View file

@ -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
```

20
src/CubicalHott/Chapter2Lemma221.lagda.md Normal file
View file

@ -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)

10
src/CubicalHott/Chapter3.lagda.md
View file

@ -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

16
src/CubicalHott/Chapter6.lagda.md
View file

@ -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 ∎
```

6
src/CubicalHott/Primitives.agda Normal file
View file

@ -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

83
src/CubicalHott/Primitives/Interval.lagda.md Normal file
View file

@ -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.

48
src/CubicalHott/Primitives/Kan.lagda.md Normal file
View file

@ -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 _≡_ #-}
```

36
src/CubicalHott/Primitives/Type.lagda.md Normal file
View file

@ -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 _⊔_ #-}
```

5
src/HottBook/Chapter1.lagda.md
View file

@ -4,7 +4,8 @@
```
module HottBook.Chapter1 where
open import Agda.Primitive
open import Agda.Primitive public
open import Agda.Primitive.Cubical public
```
</details>
@ -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

5
src/HottBook/Chapter2.lagda.md
View file

@ -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-≡)
```

81
src/HottBook/Chapter6.lagda.md
View file

@ -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
```

33
src/HottBook/Chapter8.lagda.md
View file

@ -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

1
src/VanDoornDissertation/HIT.lagda.md
View file

@ -2,7 +2,6 @@
module VanDoornDissertation.HIT where
open import HottBook.Chapter1
-- open import VanDoornDissertation.Preliminaries
```
# 3 Higher Inductive Types