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

make it error-less

Browse source
This commit is contained in:
Michael Zhang 2024-05-30 16:54:04 -05:00
parent df0887af8c
commit 282be4abed
10 changed files with 90 additions and 102 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
Makefile
View file

@ -1,7 +1,11 @@
GENDIR := html/src/generated
build-to-html:
find src \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
find src \
-not \( -path src/Misc -prune \) \
-not \( -path src/CubicalHott -prune \) \
\( -name "*.agda" -o -name "*.lagda.md" \) \
-print0 \
| rust-parallel -0 agda \
--html \
--html-dir=$(GENDIR) \
@ -17,6 +21,6 @@ refresh-book: build-to-html
mdbook serve html
deploy: build-book
rsync -azrP html/book/ root@veil:/home/blogDeploy/public/research
rsync -azr html/book/ root@veil:/home/blogDeploy/public/research
.PHONY: build-book build-to-html deploy

6
src/HottBook/Chapter2Exercises.lagda.md
View file

@ -133,10 +133,6 @@ exercise2∙13 = f , equiv
where
open WithAbstractionUtil
neg : 𝟚 → 𝟚
neg true = false
neg false = true
f : 𝟚 ≃ 𝟚 → 𝟚
f (fst , snd) = fst true
@ -168,7 +164,7 @@ exercise2∙13 = f , equiv
let p3 = trans (sym (h-id true)) p2 in
remark2∙12∙6 p3
⊥-elim : {A : Set} → ⊥ → A
⊥-elim : {l : Level} {A : Set l} → ⊥ {l} → A
⊥-elim ()
opposite-prop : {a b : 𝟚} → (p : f' a ≡ b) → f' (neg a) ≡ neg b

109
src/HottBook/Chapter3.lagda.md
View file

@ -48,28 +48,28 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
### Example 3.1.9
```
example3∙1∙9 : ∀ {l : Level} → ¬_ {lsuc l} (isSet (Set l))
example3∙1∙9 p = remark2∙12∙6 lol
where
open axiom2∙10∙3
-- example3∙1∙9 : ∀ {l : Level} → ¬_ {lsuc l} (isSet (Set l))
-- example3∙1∙9 p = remark2∙12∙6 lol
-- where
-- open axiom2∙10∙3
f-path : 𝟚 ≡ 𝟚
f-path = ua neg-equiv
-- f-path : 𝟚 ≡ 𝟚
-- f-path = ua neg-equiv
bogus : id ≡ neg
bogus =
let
-- helper : f-path ≡ refl
-- helper = p 𝟚 𝟚 f-path refl
-- bogus : id ≡ neg
-- bogus =
-- let
-- -- helper : f-path ≡ refl
-- -- helper = p 𝟚 𝟚 f-path refl
a = ap
-- a = ap
-- wtf : idtoeqv f-path ≡ idtoeqv refl
-- wtf = ap idtoeqv helper
in {! !}
-- -- wtf : idtoeqv f-path ≡ idtoeqv refl
-- -- wtf = ap idtoeqv helper
-- in {! !}
lol : true ≡ false
lol = ap (λ f → f true) bogus
-- lol : true ≡ false
-- lol = ap (λ f → f true) bogus
```
## 3.2 Propositions as types?
@ -79,55 +79,56 @@ example3∙1∙9 p = remark2∙12∙6 lol
TODO: Study this more
```
theorem3∙2∙2 : ((A : Set) → ¬ ¬ A → A) → ⊥
theorem3∙2∙2 f = let wtf = f 𝟚 in {! !}
where
open axiom2∙10∙3
postulate
theorem3∙2∙2 : {l : Level} → ((A : Set l) → ¬ ¬ A → A) → ⊥ {l}
-- theorem3∙2∙2 f = let wtf = f 𝟚 in {! !}
-- where
-- open axiom2∙10∙3
p : 𝟚 ≡ 𝟚
p = ua neg-equiv
-- p : 𝟚 ≡ 𝟚
-- p = ua neg-equiv
wtf : ¬ ¬ 𝟚 → 𝟚
wtf = f 𝟚
-- wtf : ¬ ¬ 𝟚 → 𝟚
-- wtf = f 𝟚
wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
wtf2 = apd f p
-- wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
-- wtf2 = apd f p
wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
wtf3 u = happly wtf2 u
-- wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
-- wtf3 u = happly wtf2 u
wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u))
wtf4 u =
let
wtf5 :
let A = λ A → ¬ ¬ A in
let B = id in
transport (λ x → A x → B x) p (f 𝟚) ≡ λ x → transport B p (f 𝟚 (transport A (sym p) x))
wtf5 = equation2∙9∙4 (f 𝟚) p
in
happly wtf5 u
-- wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u))
-- wtf4 u =
-- let
-- wtf5 :
-- let A = λ A → ¬ ¬ A in
-- let B = id in
-- transport (λ x → A x → B x) p (f 𝟚) ≡ λ x → transport B p (f 𝟚 (transport A (sym p) x))
-- wtf5 = equation2∙9∙4 (f 𝟚) p
-- in
-- happly wtf5 u
wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v
wtf6 u v = funext (λ x → rec-⊥ (u x))
-- wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v
-- wtf6 u v = funext (λ x → rec-⊥ (u x))
wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
wtf7 u = {! !}
-- wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
-- wtf7 u = {! !}
wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
wtf8 u = {! sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
-- wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
-- wtf8 u = {! sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
wtf9 = {! !}
-- wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
-- wtf9 = {! !}
wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
wtf10 true p = remark2∙12∙6 (sym p)
wtf10 false p = remark2∙12∙6 p
-- wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
-- wtf10 true p = remark2∙12∙6 (sym p)
-- wtf10 false p = remark2∙12∙6 p
wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u))
wtf11 u = wtf10 (f 𝟚 u)
-- wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u))
-- wtf11 u = wtf10 (f 𝟚 u)
wtf12 : (u : ¬ ¬ 𝟚) → ⊥
wtf12 u = wtf11 u (wtf9 u)
-- wtf12 : (u : ¬ ¬ 𝟚) → ⊥
-- wtf12 u = wtf11 u (wtf9 u)
```
### Corollary 3.2.7

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

@ -52,11 +52,13 @@ lemma6∙2∙5 {A} a p circ = S¹-elim P p-base p-loop circ
### Lemma 6.2.8
```
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 {! !}
-- 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

2
src/HottBook/Chapter7.lagda.md
View file

@ -13,4 +13,6 @@ open import HottBook.Chapter6
```
is-_-type : ℕ → Set → Set
is- zero -type X = 𝟙
is- suc n -type X = (x y : X) → is- n -type (x ≡ y)
```

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

@ -10,8 +10,9 @@ open import HottBook.Chapter6
### Definition 8.0.1
```
π : (n : ℕ) → (A : Set) → (a : A) → Set
-- TODO: Finish
postulate
π : (n : ℕ) → (A : Set) → (a : A) → Set
```
## 8.1 π₁(S¹)

13
src/HottBook/Chapter9.lagda.md
View file

@ -11,19 +11,19 @@ open import HottBook.Chapter1
record precat {l : Level} (A : Set l) : Set (lsuc l) where
field
hom : (a b : A) → Set
id : (a : A) → hom a a
id' : (a : A) → hom a a
comp : {a b c : A} → hom a b → hom b c → hom a c
lol : (a b : A) → (f : hom a b) → (f ≡ comp f (id b)) × (f ≡ comp (id a) f)
lol : (a b : A) → (f : hom a b) → (f ≡ comp f (id' b)) × (f ≡ comp (id' a) f)
```
### Definition 9.1.2
```
record isIso {l : Level} {A : Set l} {PC : precat A} {a b : A} (f : precat.hom PC a b) : Set (lsuc l) where
field
g : precat.hom PC b a
g-f : precat.comp f g ≡ precat.id a
-- record isIso {l : Level} {A : Set l} {PC : precat A} {a b : A} (f : precat.hom PC a b) : Set (lsuc l) where
-- field
-- g : precat.hom PC b a
-- g-f : precat.comp f g ≡ precat.id' a
```
### Lemma 9.1.4
@ -34,4 +34,5 @@ idtoiso : {A : Set}
→ (a b : A)
→ a ≡ b
→ precat.hom PC a b
idtoiso {A} PC a b refl = precat.id' PC a
```

21
src/HottBook/Primitives.agda
View file

@ -1,21 +0,0 @@
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 _⊔_ #-}

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

@ -1,9 +1,8 @@
```
{-# OPTIONS --cubical #-}
module VanDoornDissertation.HIT where
open import Data.Nat
open import VanDoornDissertation.Preliminaries
open import HottBook.Chapter1
-- open import VanDoornDissertation.Preliminaries
```
# 3 Higher Inductive Types
@ -11,9 +10,13 @@ open import VanDoornDissertation.Preliminaries
## 3.1 Propositional Truncation
```
data one-step-truncation (A : Set) : Set where
f : A → one-step-truncation A
e : (x y : A) → f x ≡ f y
postulate
one-step-truncation : Set → Set
f : {A : Set} → A → one-step-truncation A
e : {A : Set} → (x y : A) → f x ≡ f y
-- data one-step-truncation (A : Set) : Set where
-- f : A → one-step-truncation A
-- e : (x y : A) → f x ≡ f y
weakly-constant : {A B : Set} → (g : A → B) → Set
weakly-constant {A} g = {x y : A} → g x ≡ g y

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

@ -1,5 +1,4 @@
```
{-# OPTIONS --cubical #-}
module VanDoornDissertation.Preliminaries where
open import Agda.Primitive