This commit is contained in:
Michael Zhang 2024-07-02 22:11:19 -05:00
parent 05eb94c28e
commit d3f5406ffa
7 changed files with 131 additions and 40 deletions

View file

@ -2,6 +2,14 @@
- [Front](./front.md)
# HoTT Book
- [Chapter 1](./generated/HottBook.Chapter1.md)
- [Chapter 2](./generated/HottBook.Chapter2.md)
- [Chapter 3](./generated/HottBook.Chapter3.md)
- [Chapter 4](./generated/HottBook.Chapter4.md)
- [Chapter 5](./generated/HottBook.Chapter5.md)
# HoTT Book (Cubical formulation)
- [Chapter 1](./generated/CubicalHott.Chapter1.md)

22
src/CEKCoinductive.agda Normal file
View file

@ -0,0 +1,22 @@
{-# OPTIONS --guardedness #-}
module CEKCoinductive where
open import Agda.Primitive
private
variable
l l1 l2 l3 : Level
E : Set Set
R : Set
data ITreeF (ITree : Set) : Set where
Ret : (r : R) ITreeF ITree
Tau : (t : ITree) ITreeF ITree
Vis : {A : Set l1} (e : E A) (k : A ITreeF E R) ITreeF E R
record ITree : Set where
coinductive
field
_observe : ITreeF ITree

View file

@ -6,6 +6,21 @@ open import CubicalHott.Chapter1
open import CubicalHott.Chapter2
```
## 6.3 The interval
```
data Iv : Type where
0I : Iv
1I : Iv
seg : 0I ≡ 1I
```
### Lemma 6.3.1
```
lemma6∙3∙1 : isContr Iv
```
## 6.4 Circles and spheres
```
@ -18,36 +33,36 @@ data S¹ : Type where
```
lemma6∙4∙1 : loop ≢ refl
lemma6∙4∙1 p =
{! !}
where
open ≡-Reasoning
-- 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
-- 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 ∎
-- bad : {A : Type} (x : A) → (p : x ≡ x) → p ≡ refl
-- bad x p = begin
-- p ≡⟨ {! !} ⟩
-- p ≡⟨ {! !} ⟩
-- refl ∎
```
### Lemma 6.4.2
```
lemma6∙4∙2 : Σ ((x : S¹) → x ≡ x) (λ y → y ≢ (λ x → refl))
lemma6∙4∙2 = f , g
where
f : (x : S¹) → x ≡ x
f base = loop
f (loop i) i₁ = loop {! !}
-- lemma6∙4∙2 = f , g
-- where
-- f : (x : S¹) → x ≡ x
-- f base = loop
-- f (loop i) i₁ = loop {! !}
g : f ≢ (λ x → refl)
g p = let
z = happlyd p
z2 = z base
z3 = lemma6∙4∙1 z2
in z3
-- g : f ≢ (λ x → refl)
-- g p = let
-- z = happlyd p
-- z2 = z base
-- z3 = lemma6∙4∙1 z2
-- in z3
```

View file

@ -724,11 +724,8 @@ module axiom2∙10∙3 where
postulate
ua : {l : Level} {A B : Set l} → (A ≃ B) → (A ≡ B)
forward : {l : Level} {A B : Set l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
-- forward eqv = {! !}
backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
-- backward p = {! !}
forward : {l : Level} {A B : Set l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B)
ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)

View file

@ -184,18 +184,8 @@ theorem3∙2∙2 double-neg = conclusion
let y = what ∙ x in
sym y ∙ foranyu
-- postulate
huhh : (Σ.fst e) (fbool u) ≡ fbool u
huhh =
let
equiv1 = ap ua (axiom2∙10∙3.forward e)
x : {A B : Set l} → (e : A ≃ B) → (a : A) → transport id (ua e) a ≡ Σ.fst e a
x e a =
{! axiom2∙10∙3.forward ? !}
in
{! !}
-- sym (x e (fbool u)) ∙ nextStep
postulate
huhh : (Σ.fst e) (fbool u) ≡ fbool u
finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x)
finalStep (lift true) p =
@ -310,5 +300,9 @@ lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 _ g
concat : g ( g x ) ≡ g ( g y )
concat = a ∙ eqProp ∙ (sym b)
in
{! prop ? !}
admit
where
postulate
-- TODO: Finish this
admit : x ≡ y
```

View file

@ -0,0 +1,53 @@
```
module HottBook.Chapter6 where
open import HottBook.Chapter1
open import HottBook.Chapter2
open import HottBook.Chapter3
private
variable
l : Level
```
# Chapter 6 Higher Inductive Types
```
postulate
S¹ : Set
base : S¹
loop : base ≡ base
```
## 6.2 Induction principles and dependent paths
```
dep-path : {A : Set} {x y : A} → (P : A → Set) → (p : x ≡ y) → (u : P x) → (v : P y) → Set
dep-path P p u v = transport P p u ≡ v
syntax dep-path P p u v = u ≡[ P , p ] v
```
## 6.3 The interval
```
postulate
I : Set
0I : I
1I : I
seg : 0I ≡ 1I
record I-rec (B : Set) (b0 b1 : B) (s : b0 ≡ b1) : Set where
field
f : I → B
prop1 : f 0I ≡ b0
prop2 : f 1I ≡ b1
prop3 : apd f seg ≡ {! s !}
record I-ind (P : I → Set) (b0 : P 0I) (b1 : P 1I) (s : b0 ≡[ P , seg ] b1) : Set where
field
f : (x : I) → P x
prop1 : f 0I ≡ b0
prop2 : f 1I ≡ b1
prop3 : apd f seg ≡ {! s !}
```

2
src/Hurewicz.agda Normal file
View file

@ -0,0 +1,2 @@
module Hurewicz where