updates
This commit is contained in:
parent
c7f4ee0708
commit
6d0e500a59
23
src/HottBook/Chapter1.lagda.md
Normal file
23
src/HottBook/Chapter1.lagda.md
Normal file
|
@ -0,0 +1,23 @@
|
||||||
|
```
|
||||||
|
module HottBook.Chapter1 where
|
||||||
|
|
||||||
|
open import Data.Empty
|
||||||
|
open import Data.Sum
|
||||||
|
|
||||||
|
Type = Set
|
||||||
|
```
|
||||||
|
|
||||||
|
## 1.7 Coproduct types
|
||||||
|
|
||||||
|
```
|
||||||
|
infixl 6 _+_
|
||||||
|
_+_ : (A B : Type) → Type
|
||||||
|
A + B = A ⊎ B
|
||||||
|
```
|
||||||
|
|
||||||
|
## 1.11 Propositions as types
|
||||||
|
|
||||||
|
```
|
||||||
|
¬_ : (A : Type) → Type
|
||||||
|
¬ A = A → ⊥
|
||||||
|
```
|
|
@ -145,7 +145,7 @@ _∼_ {A} f g = (x : A) → f x ≡ g x
|
||||||
|
|
||||||
### Lemma 2.4.2
|
### Lemma 2.4.2
|
||||||
|
|
||||||
Homotopy forms an equivalence:
|
Homotopy forms an equivalence relation:
|
||||||
|
|
||||||
```
|
```
|
||||||
∼-refl : {A : Type} {P : A → Type} (f : (x : A) → P x) → f ∼ f
|
∼-refl : {A : Type} {P : A → Type} (f : (x : A) → P x) → f ∼ f
|
||||||
|
@ -189,6 +189,26 @@ id-qinv = record
|
||||||
}
|
}
|
||||||
```
|
```
|
||||||
|
|
||||||
|
### Definition 2.4.10
|
||||||
|
|
||||||
|
```
|
||||||
|
linv : {A B : Type} (f : A → B) → Type
|
||||||
|
linv {A} {B} f = Σ[ g ∈ (B → A) ] (f ∘ g) ∼ id
|
||||||
|
|
||||||
|
rinv : {A B : Type} (f : A → B) → Type
|
||||||
|
rinv {A} {B} f = Σ[ h ∈ (B → A) ] (h ∘ f) ∼ id
|
||||||
|
|
||||||
|
isEquiv : {A B : Type} (f : A → B) → Type
|
||||||
|
isEquiv f = linv f × rinv f
|
||||||
|
```
|
||||||
|
|
||||||
|
### Definition 2.4.11
|
||||||
|
|
||||||
|
```
|
||||||
|
_≃_ : (A B : Type) → Type
|
||||||
|
A ≃ B = Σ[ f ∈ (A → B) ] isEquiv f
|
||||||
|
```
|
||||||
|
|
||||||
## 2.8 The unit type
|
## 2.8 The unit type
|
||||||
|
|
||||||
```
|
```
|
||||||
|
@ -239,3 +259,19 @@ happly f g {x} p =
|
||||||
postulate
|
postulate
|
||||||
funext : {A B : Type} → (f g : A → B) → {x : A} → (p : f x ≡ g x) → f ≡ g
|
funext : {A B : Type} → (f g : A → B) → {x : A} → (p : f x ≡ g x) → f ≡ g
|
||||||
```
|
```
|
||||||
|
|
||||||
|
## 2.10 Universes and the univalence axiom
|
||||||
|
|
||||||
|
### Lemma 2.10.1
|
||||||
|
|
||||||
|
```
|
||||||
|
-- idToEquiv : {A B : Type} → (A ≡ B) → A ≃ B
|
||||||
|
-- idToEquiv p = ? , ?
|
||||||
|
```
|
||||||
|
|
||||||
|
### Axiom 2.10.3 (Univalence)
|
||||||
|
|
||||||
|
```
|
||||||
|
postulate
|
||||||
|
ua : {A B : Type} (eqv : A ≃ B) → (A ≡ B)
|
||||||
|
```
|
||||||
|
|
80
src/HottBook/Chapter3.lagda.md
Normal file
80
src/HottBook/Chapter3.lagda.md
Normal file
|
@ -0,0 +1,80 @@
|
||||||
|
```
|
||||||
|
module HottBook.Chapter3 where
|
||||||
|
|
||||||
|
open import Relation.Binary.PropositionalEquality
|
||||||
|
open import Data.Sum
|
||||||
|
open import Data.Empty
|
||||||
|
open import HottBook.Chapter1
|
||||||
|
|
||||||
|
```
|
||||||
|
|
||||||
|
## 3.1 Sets and n-types
|
||||||
|
|
||||||
|
### Definition 3.1.1
|
||||||
|
|
||||||
|
```
|
||||||
|
isSet : (A : Type) → Type
|
||||||
|
isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
|
||||||
|
```
|
||||||
|
|
||||||
|
## 3.2 Propositions as types?
|
||||||
|
|
||||||
|
## 3.4 Classical vs. intuitionistic logic
|
||||||
|
|
||||||
|
### Definition 3.4.3
|
||||||
|
|
||||||
|
#### i. Decidability of types
|
||||||
|
|
||||||
|
```
|
||||||
|
decidable : (A : Type) → Type
|
||||||
|
decidable A = A ⊎ ¬ A
|
||||||
|
```
|
||||||
|
|
||||||
|
#### ii. Decidability of type families
|
||||||
|
|
||||||
|
```
|
||||||
|
dep-decidable : {A : Type} → (B : A → Type) → Type
|
||||||
|
dep-decidable {A} B = (a : A) → (B a ⊎ ¬ B a)
|
||||||
|
```
|
||||||
|
|
||||||
|
#### iii. Decidable equality
|
||||||
|
|
||||||
|
```
|
||||||
|
decidable-equality : (A : Type) → Type
|
||||||
|
decidable-equality A = (a b : A) → (a ≡ b) ⊎ ¬ (a ≡ b)
|
||||||
|
```
|
||||||
|
|
||||||
|
So I think the interesting property about this is that normally a function f
|
||||||
|
would return something of the type a ≡ b, which for any a and b would always
|
||||||
|
produce that one path. But there could exist other functions that produce
|
||||||
|
different paths, like (g : ... → a ≡ b).
|
||||||
|
|
||||||
|
What this (a ≡ b) ⊎ ¬ (a ≡ b) business is saying is: if f couldn't produce a
|
||||||
|
path, then **NO** other functions will ever be able to produce paths (along with
|
||||||
|
a proof that this is true). This means f is _exclusively_ the deciding factor
|
||||||
|
for whether a and b are equal under this type, and it's the only one that mints
|
||||||
|
paths for a ≡ b.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
> 2. In case you are looking for advanced exercises, you can try to prove that
|
||||||
|
> any type with decidable equality is a set.
|
||||||
|
|
||||||
|
```
|
||||||
|
decidable-equality-is-set : (A : Type) → decidable-equality A → isSet A
|
||||||
|
decidable-equality-is-set A f x y p q =
|
||||||
|
let
|
||||||
|
res = f x y
|
||||||
|
|
||||||
|
-- We can eliminate the bottom case because if p and q exist, it must be inj₁
|
||||||
|
center : x ≡ y
|
||||||
|
center = [ (λ p′ → p′) , (λ p′ → ⊥-elim (p′ _)) ] (f x y)
|
||||||
|
|
||||||
|
-- What i want is: given any path x ≡ y, prove that it equals this inj₁ (res f x y)
|
||||||
|
guarantee : (p′ : x ≡ y) → center ≡ p′
|
||||||
|
guarantee p′ = J (λ the what → the ≡ p′) ? ?
|
||||||
|
|
||||||
|
info = ?
|
||||||
|
in
|
||||||
|
J (λ the what → p ≡ ?) refl ?
|
||||||
|
```
|
Loading…
Reference in a new issue