auto gitdoc commit
This commit is contained in:
parent
eb53383a78
commit
d5bbdfe962
|
@ -369,7 +369,7 @@ code (suc x) (suc y) = code x y
|
||||||
|
|
||||||
_For all $m, n : N$ we have $(m = n) \simeq \texttt{code}(m, n)$._
|
_For all $m, n : N$ we have $(m = n) \simeq \texttt{code}(m, n)$._
|
||||||
|
|
||||||
```
|
```text
|
||||||
theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n
|
theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n
|
||||||
theorem2∙13∙1 m n = encode m n , equiv
|
theorem2∙13∙1 m n = encode m n , equiv
|
||||||
where
|
where
|
||||||
|
|
33
src/HottBook/Chapter5.lagda.md
Normal file
33
src/HottBook/Chapter5.lagda.md
Normal file
|
@ -0,0 +1,33 @@
|
||||||
|
```
|
||||||
|
module HottBook.Chapter5 where
|
||||||
|
|
||||||
|
open import Agda.Primitive
|
||||||
|
open import HottBook.Chapter1
|
||||||
|
```
|
||||||
|
|
||||||
|
## 5.1 Introduction to inductive types
|
||||||
|
|
||||||
|
### Theorem 5.1.1
|
||||||
|
|
||||||
|
```
|
||||||
|
-- theorem5∙1∙1 : {E : ℕ → Set}
|
||||||
|
-- → (f g : (x : ℕ) → E x)
|
||||||
|
-- → (z : f 0 ≡ g 0)
|
||||||
|
-- → (s :
|
||||||
|
-- → f ≡ g
|
||||||
|
```
|
||||||
|
|
||||||
|
### Definition 5.4.1
|
||||||
|
|
||||||
|
```
|
||||||
|
ℕAlg : {l : Level} → Set (lsuc l)
|
||||||
|
ℕAlg {l} = Σ (Set l) (λ C → C × (C → C))
|
||||||
|
```
|
||||||
|
|
||||||
|
### Definition 5.4.2
|
||||||
|
|
||||||
|
```
|
||||||
|
ℕHom : {l : Level} → ℕAlg {l} → ℕAlg {l} → Set l
|
||||||
|
ℕHom alg1@(C , (cz , cs)) alg2@(D , (dz , ds)) =
|
||||||
|
Σ (C → D) λ h → (h cz ≡ dz) × ((c : C) → h (cs c) ≡ ds (h c))
|
||||||
|
```
|
|
@ -1,16 +1,18 @@
|
||||||
```
|
```
|
||||||
module HottBook.Chapter6 where
|
module HottBook.Chapter6 where
|
||||||
|
|
||||||
open import Relation.Binary.PropositionalEquality
|
open import HottBook.Chapter1
|
||||||
|
|
||||||
open import HottBook.Chapter2
|
open import HottBook.Chapter2
|
||||||
```
|
```
|
||||||
|
|
||||||
### Definition 6.2.2 (Dependent paths)
|
### Definition 6.2.2 (Dependent paths)
|
||||||
|
|
||||||
```
|
```
|
||||||
dep-path : {A : Type} (P : A → Type) {x y : A} (p : x ≡ y)
|
dep-path : {A : Set}
|
||||||
→ (u : P x) → (v : P y) → Type
|
→ (P : A → Set)
|
||||||
|
→ {x y : A}
|
||||||
|
→ (p : x ≡ y)
|
||||||
|
→ (u : P x) → (v : P y) → Set
|
||||||
dep-path P p u v = transport P p u ≡ v
|
dep-path P p u v = transport P p u ≡ v
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -18,17 +20,41 @@ Circle definition
|
||||||
|
|
||||||
```
|
```
|
||||||
postulate
|
postulate
|
||||||
𝕊¹ : Type
|
S¹ : Set
|
||||||
base : 𝕊¹
|
base : S¹
|
||||||
loop : base ≡ base
|
loop : base ≡ base
|
||||||
𝕊¹-elim : (P : 𝕊¹ → Type) → (p-base : P base)
|
S¹-elim : (P : S¹ → Set)
|
||||||
|
→ (p-base : P base)
|
||||||
→ (p-loop : dep-path P loop p-base p-base)
|
→ (p-loop : dep-path P loop p-base p-base)
|
||||||
→ (x : 𝕊¹) → P x
|
→ (x : S¹) → P x
|
||||||
```
|
```
|
||||||
|
|
||||||
### Lemma 6.2.5
|
### Lemma 6.2.5
|
||||||
|
|
||||||
|
```text
|
||||||
|
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 = a
|
||||||
|
|
||||||
|
p-loop : transport P loop a ≡ a
|
||||||
|
p-loop =
|
||||||
|
let wtf = {! lemma2∙3∙8 !} in
|
||||||
|
{! !}
|
||||||
```
|
```
|
||||||
lemma625 : {A : Type} (a : A) → (p : a ≡ a) → 𝕊¹ → A
|
|
||||||
lemma625 {A} a p circ = 𝕊¹-elim (λ _ → A) a ? circ
|
## 6.3 The interval
|
||||||
|
|
||||||
```
|
```
|
||||||
|
postulate
|
||||||
|
I : Set
|
||||||
|
0I : I
|
||||||
|
1I : I
|
||||||
|
seg : 0I ≡ 1I
|
||||||
|
```
|
19
src/HottBook/Chapter8.lagda.md
Normal file
19
src/HottBook/Chapter8.lagda.md
Normal file
|
@ -0,0 +1,19 @@
|
||||||
|
```
|
||||||
|
module HottBook.Chapter8 where
|
||||||
|
|
||||||
|
open import Agda.Primitive
|
||||||
|
open import HottBook.Chapter6
|
||||||
|
```
|
||||||
|
|
||||||
|
## 8.1 π₁(S¹)
|
||||||
|
|
||||||
|
### Definition 8.1.1
|
||||||
|
|
||||||
|
```
|
||||||
|
data ℤ : Set where
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
code : {l : Level} → S¹ → Set l
|
||||||
|
code {l} = S¹-elim (λ _ → Set l) ℤ (ua succ)
|
||||||
|
```
|
13
src/HottBook/Chapter9.lagda.md
Normal file
13
src/HottBook/Chapter9.lagda.md
Normal file
|
@ -0,0 +1,13 @@
|
||||||
|
```
|
||||||
|
module HottBook.Chapter9 where
|
||||||
|
|
||||||
|
open import Agda.Primitive
|
||||||
|
```
|
||||||
|
|
||||||
|
## 9.1 Categories and precategories
|
||||||
|
|
||||||
|
```
|
||||||
|
record precategory {l : Level} : Set (lsuc l) where
|
||||||
|
field
|
||||||
|
A : Set l
|
||||||
|
```
|
Loading…
Reference in a new issue