Compare commits
2 commits
663827023b
...
a44ff3cd4f
Author | SHA1 | Date | |
---|---|---|---|
Michael Zhang | a44ff3cd4f | ||
Michael Zhang | 0a5abb61e4 |
2
.vscode/settings.json
vendored
2
.vscode/settings.json
vendored
|
@ -5,6 +5,6 @@
|
||||||
"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
|
"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
|
||||||
"agdaMode.connection.commandLineOptions": "",
|
"agdaMode.connection.commandLineOptions": "",
|
||||||
"search.exclude": {
|
"search.exclude": {
|
||||||
"src/HottBook/**": true
|
"src/CubicalHott/**": true
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -253,26 +253,26 @@ open axiom2∙10∙3
|
||||||
### Theorem 2.11.2
|
### Theorem 2.11.2
|
||||||
|
|
||||||
```
|
```
|
||||||
module lemma2∙11∙2 where
|
-- module lemma2∙11∙2 where
|
||||||
open ≡-Reasoning
|
-- open ≡-Reasoning
|
||||||
|
|
||||||
i : {l : Level} {A : Type l} {a x1 x2 : A}
|
-- i : {l : Level} {A : Type l} {a x1 x2 : A}
|
||||||
→ (p : x1 ≡ x2)
|
-- → (p : x1 ≡ x2)
|
||||||
→ (q : a ≡ x1)
|
-- → (q : a ≡ x1)
|
||||||
→ transport (λ y → a ≡ y) p q ≡ q ∙ p
|
-- → transport (λ y → a ≡ y) p q ≡ q ∙ p
|
||||||
i {l} {A} {a} {x1} {x2} p q j = {! !}
|
-- i {l} {A} {a} {x1} {x2} p q j = {! !}
|
||||||
|
|
||||||
ii : {l : Level} {A : Type l} {a x1 x2 : A}
|
-- ii : {l : Level} {A : Type l} {a x1 x2 : A}
|
||||||
→ (p : x1 ≡ x2)
|
-- → (p : x1 ≡ x2)
|
||||||
→ (q : x1 ≡ a)
|
-- → (q : x1 ≡ a)
|
||||||
→ transport (λ y → y ≡ a) p q ≡ sym p ∙ q
|
-- → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
|
||||||
ii {l} {A} {a} {x1} {x2} p q = {! !}
|
-- ii {l} {A} {a} {x1} {x2} p q = {! !}
|
||||||
|
|
||||||
iii : {l : Level} {A : Type l} {a x1 x2 : A}
|
-- iii : {l : Level} {A : Type l} {a x1 x2 : A}
|
||||||
→ (p : x1 ≡ x2)
|
-- → (p : x1 ≡ x2)
|
||||||
→ (q : x1 ≡ x1)
|
-- → (q : x1 ≡ x1)
|
||||||
→ transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
|
-- → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
|
||||||
iii {l} {A} {a} {x1} {x2} p q = {! !}
|
-- iii {l} {A} {a} {x1} {x2} p q = {! !}
|
||||||
```
|
```
|
||||||
|
|
||||||
### Remark 2.12.6
|
### Remark 2.12.6
|
||||||
|
|
|
@ -39,6 +39,14 @@ module section3∙7 where
|
||||||
data ∥_∥ (A : Type) : Type where
|
data ∥_∥ (A : Type) : Type where
|
||||||
∣_∣ : (a : A) → ∥ A ∥
|
∣_∣ : (a : A) → ∥ A ∥
|
||||||
witness : (x y : ∥ A ∥) → x ≡ y
|
witness : (x y : ∥ A ∥) → x ≡ y
|
||||||
|
|
||||||
|
rec-∥_∥ : (A : Type) → {B : Type} → isProp B → (f : A → B)
|
||||||
|
→ Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
|
||||||
|
rec-∥ A ∥ {B} BisProp f = g , λ _ → refl
|
||||||
|
where
|
||||||
|
g : ∥ A ∥ → B
|
||||||
|
g ∣ a ∣ = f a
|
||||||
|
g (witness x y i) = BisProp (g x) (g y) i
|
||||||
open section3∙7
|
open section3∙7
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -64,5 +72,8 @@ postulate
|
||||||
|
|
||||||
```
|
```
|
||||||
lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥
|
lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥
|
||||||
lemma3∙9∙1 prop = ∣_∣ , {! !}
|
lemma3∙9∙1 {P} prop = ∣_∣ , qinv-to-isequiv (mkQinv inv {! !} {! !})
|
||||||
|
where
|
||||||
|
inv : ∥ P ∥ → P
|
||||||
|
inv = {! rec-∥ P ∥ !}
|
||||||
```
|
```
|
|
@ -5,7 +5,11 @@
|
||||||
module HottBook.Chapter1 where
|
module HottBook.Chapter1 where
|
||||||
|
|
||||||
open import Agda.Primitive public
|
open import Agda.Primitive public
|
||||||
open import Agda.Primitive.Cubical public
|
open import HottBook.CoreUtil
|
||||||
|
|
||||||
|
private
|
||||||
|
variable
|
||||||
|
l : Level
|
||||||
```
|
```
|
||||||
|
|
||||||
</details>
|
</details>
|
||||||
|
@ -21,7 +25,7 @@ open import Agda.Primitive.Cubical public
|
||||||
## 1.4 Dependent function types (Π-types)
|
## 1.4 Dependent function types (Π-types)
|
||||||
|
|
||||||
```
|
```
|
||||||
id : {l : Level} {A : Set l} → A → A
|
id : {A : Set l} → A → A
|
||||||
id x = x
|
id x = x
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -94,10 +98,10 @@ rec-+ C f g (inr x) = g x
|
||||||
```
|
```
|
||||||
|
|
||||||
```
|
```
|
||||||
data ⊥ {l : Level} : Set l where
|
data ⊥ : Set where
|
||||||
|
|
||||||
rec-⊥ : {l : Level} → {C : Set l} → (x : ⊥ {l}) → C
|
rec-⊥ : {C : Set l} → (x : ⊥) → C
|
||||||
rec-⊥ {C} ()
|
rec-⊥ ()
|
||||||
```
|
```
|
||||||
|
|
||||||
## 1.8 The type of booleans
|
## 1.8 The type of booleans
|
||||||
|
@ -131,22 +135,22 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
|
||||||
|
|
||||||
```
|
```
|
||||||
infix 3 ¬_
|
infix 3 ¬_
|
||||||
¬_ : ∀ {l : Level} (A : Set l) → Set l
|
¬_ : (A : Set l) → Set l
|
||||||
¬_ {l} A = A → ⊥ {l}
|
¬_ A = A → ⊥
|
||||||
```
|
```
|
||||||
|
|
||||||
## 1.12 Identity types
|
## 1.12 Identity types
|
||||||
|
|
||||||
```
|
```
|
||||||
infix 4 _≡_
|
infix 4 _≡_
|
||||||
data _≡_ {l} {A : Set l} : (a b : A) → Set l where
|
data _≡_ {A : Set l} : (a b : A) → Set l where
|
||||||
instance refl : {x : A} → x ≡ x
|
instance refl : {x : A} → x ≡ x
|
||||||
```
|
```
|
||||||
|
|
||||||
### 1.12.3 Disequality
|
### 1.12.3 Disequality
|
||||||
|
|
||||||
```
|
```
|
||||||
_≢_ : {A : Set} (x y : A) → Set
|
_≢_ : {A : Set l} (x y : A) → Set l
|
||||||
_≢_ x y = (p : x ≡ y) → ⊥
|
_≢_ x y = (p : x ≡ y) → ⊥
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
|
@ -5,9 +5,12 @@
|
||||||
module HottBook.Chapter2 where
|
module HottBook.Chapter2 where
|
||||||
|
|
||||||
open import Agda.Primitive.Cubical hiding (i1)
|
open import Agda.Primitive.Cubical hiding (i1)
|
||||||
open import HottBook.Chapter1 hiding (i1)
|
open import HottBook.Chapter1
|
||||||
open import HottBook.Chapter2Lemma221 public
|
open import HottBook.Chapter2Lemma221 public
|
||||||
open import HottBook.Util
|
|
||||||
|
private
|
||||||
|
variable
|
||||||
|
l : Level
|
||||||
```
|
```
|
||||||
|
|
||||||
</details>
|
</details>
|
||||||
|
@ -632,7 +635,7 @@ postulate
|
||||||
### Lemma 2.9.2
|
### Lemma 2.9.2
|
||||||
|
|
||||||
```
|
```
|
||||||
happly : {A B : Set}
|
happly : {A B : Set l}
|
||||||
→ {f g : A → B}
|
→ {f g : A → B}
|
||||||
→ (p : f ≡ g)
|
→ (p : f ≡ g)
|
||||||
→ (x : A)
|
→ (x : A)
|
||||||
|
@ -644,7 +647,7 @@ happly {A} {B} {f} {g} p x = ap (λ h → h x) p
|
||||||
|
|
||||||
```
|
```
|
||||||
postulate
|
postulate
|
||||||
funext : {l : Level} {A B : Set l}
|
funext : {A B : Set l}
|
||||||
→ {f g : A → B}
|
→ {f g : A → B}
|
||||||
→ ((x : A) → f x ≡ g x)
|
→ ((x : A) → f x ≡ g x)
|
||||||
→ f ≡ g
|
→ f ≡ g
|
||||||
|
@ -707,10 +710,11 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
|
||||||
### Lemma 2.10.1
|
### Lemma 2.10.1
|
||||||
|
|
||||||
```
|
```
|
||||||
idtoeqv : {l : Level} {A B : Set l}
|
idtoeqv : {A B : Set l} → (A ≡ B) → (A ≃ B)
|
||||||
→ (A ≡ B)
|
idtoeqv refl = transport id refl , qinv-to-isequiv (mkQinv id id-homotopy id-homotopy)
|
||||||
→ (A ≃ B)
|
where
|
||||||
idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A
|
id-homotopy : (id ∘ id) ∼ id
|
||||||
|
id-homotopy x = refl
|
||||||
```
|
```
|
||||||
|
|
||||||
### Axiom 2.10.3 (Univalence)
|
### Axiom 2.10.3 (Univalence)
|
||||||
|
@ -726,7 +730,7 @@ module axiom2∙10∙3 where
|
||||||
backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
|
backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
|
||||||
-- backward p = {! !}
|
-- backward p = {! !}
|
||||||
|
|
||||||
ua-eqv : {l : Level} {A : Set l} {B : Set l} → (A ≃ B) ≃ (A ≡ B)
|
ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B)
|
||||||
ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
|
ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
|
||||||
|
|
||||||
open axiom2∙10∙3 hiding (forward; backward)
|
open axiom2∙10∙3 hiding (forward; backward)
|
||||||
|
@ -847,10 +851,12 @@ theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q =
|
||||||
### Theorem 2.12.5
|
### Theorem 2.12.5
|
||||||
|
|
||||||
```
|
```
|
||||||
module theorem2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where
|
module theorem2∙12∙5 {A B : Set l} (a₀ : A) where
|
||||||
|
open import HottBook.CoreUtil using (Lift)
|
||||||
|
|
||||||
code : A + B → Set l
|
code : A + B → Set l
|
||||||
code (inl a) = a₀ ≡ a
|
code (inl a) = a₀ ≡ a
|
||||||
code (inr b) = ⊥
|
code (inr b) = Lift ⊥
|
||||||
|
|
||||||
encode : (x : A + B) → (p : inl a₀ ≡ x) → code x
|
encode : (x : A + B) → (p : inl a₀ ≡ x) → code x
|
||||||
encode x p = transport code p refl
|
encode x p = transport code p refl
|
||||||
|
@ -877,8 +883,9 @@ module theorem2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where
|
||||||
### Remark 2.12.6
|
### Remark 2.12.6
|
||||||
|
|
||||||
```
|
```
|
||||||
remark2∙12∙6 : true ≢ false
|
module remark2∙12∙6 where
|
||||||
remark2∙12∙6 p = genBot tt
|
true≢false : true ≢ false
|
||||||
|
true≢false p = genBot tt
|
||||||
where
|
where
|
||||||
Bmap : 𝟚 → Set
|
Bmap : 𝟚 → Set
|
||||||
Bmap true = 𝟙
|
Bmap true = 𝟙
|
||||||
|
|
|
@ -225,21 +225,18 @@ exercise2∙13 = f , equiv
|
||||||
let p1 = ap h' p in
|
let p1 = ap h' p in
|
||||||
let p2 = trans p1 (h-id false) in
|
let p2 = trans p1 (h-id false) in
|
||||||
let p3 = trans (sym (h-id true)) p2 in
|
let p3 = trans (sym (h-id true)) p2 in
|
||||||
remark2∙12∙6 p3
|
remark2∙12∙6.true≢false p3
|
||||||
|
|
||||||
⊥-elim : {l : Level} {A : Set l} → ⊥ {l} → A
|
|
||||||
⊥-elim ()
|
|
||||||
|
|
||||||
opposite-prop : {a b : 𝟚} → (p : f' a ≡ b) → f' (neg a) ≡ neg b
|
opposite-prop : {a b : 𝟚} → (p : f' a ≡ b) → f' (neg a) ≡ neg b
|
||||||
opposite-prop {a} {b} p with f' (neg a) | inspect f' (neg a)
|
opposite-prop {a} {b} p with f' (neg a) | inspect f' (neg a)
|
||||||
opposite-prop {true} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q)))
|
opposite-prop {true} {true} p | true | ingraph q = rec-⊥ (f-codomain-is-2 (trans p (sym q)))
|
||||||
opposite-prop {true} {true} p | false | _ = refl
|
opposite-prop {true} {true} p | false | _ = refl
|
||||||
opposite-prop {true} {false} p | true | _ = refl
|
opposite-prop {true} {false} p | true | _ = refl
|
||||||
opposite-prop {true} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q)))
|
opposite-prop {true} {false} p | false | ingraph q = rec-⊥ (f-codomain-is-2 (trans p (sym q)))
|
||||||
opposite-prop {false} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p)))
|
opposite-prop {false} {true} p | true | ingraph q = rec-⊥ (f-codomain-is-2 (trans q (sym p)))
|
||||||
opposite-prop {false} {true} p | false | ingraph q = refl
|
opposite-prop {false} {true} p | false | ingraph q = refl
|
||||||
opposite-prop {false} {false} p | true | ingraph q = refl
|
opposite-prop {false} {false} p | true | ingraph q = refl
|
||||||
opposite-prop {false} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p)))
|
opposite-prop {false} {false} p | false | ingraph q = rec-⊥ (f-codomain-is-2 (trans q (sym p)))
|
||||||
|
|
||||||
f-is-id' : (f' true ≡ true) → (b : 𝟚) → f' b ≡ id b
|
f-is-id' : (f' true ≡ true) → (b : 𝟚) → f' b ≡ id b
|
||||||
f-is-id' p true = p
|
f-is-id' p true = p
|
||||||
|
|
|
@ -10,7 +10,12 @@ open import HottBook.Chapter1Util
|
||||||
open import HottBook.Chapter2
|
open import HottBook.Chapter2
|
||||||
open import HottBook.Chapter3Definition331 public
|
open import HottBook.Chapter3Definition331 public
|
||||||
open import HottBook.Chapter3Lemma333 public
|
open import HottBook.Chapter3Lemma333 public
|
||||||
|
open import HottBook.CoreUtil
|
||||||
open import HottBook.Util
|
open import HottBook.Util
|
||||||
|
|
||||||
|
private
|
||||||
|
variable
|
||||||
|
l : Level
|
||||||
```
|
```
|
||||||
|
|
||||||
</details>
|
</details>
|
||||||
|
@ -20,7 +25,7 @@ open import HottBook.Util
|
||||||
### Definition 3.1.1
|
### Definition 3.1.1
|
||||||
|
|
||||||
```
|
```
|
||||||
isSet : {l : Level} (A : Set l) → Set l
|
isSet : (A : Set l) → Set l
|
||||||
isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
|
isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -34,7 +39,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
|
||||||
### Example 3.1.3
|
### Example 3.1.3
|
||||||
|
|
||||||
```
|
```
|
||||||
⊥-is-Set : ∀ {l} → isSet (⊥ {l})
|
⊥-is-Set : isSet ⊥
|
||||||
⊥-is-Set () () p q
|
⊥-is-Set () () p q
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -76,19 +81,19 @@ is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s
|
||||||
### Lemma 3.1.8
|
### Lemma 3.1.8
|
||||||
|
|
||||||
```
|
```
|
||||||
lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
|
-- lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
|
||||||
lemma3∙1∙8 {A} A-set x y p q r s =
|
-- lemma3∙1∙8 {A} A-set x y p q r s =
|
||||||
let g = λ q → A-set x y p q in
|
-- let g = λ q → A-set x y p q in
|
||||||
let
|
-- let
|
||||||
what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q'
|
-- what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q'
|
||||||
what r =
|
-- what r =
|
||||||
let what3 = apd g r in
|
-- let what3 = apd g r in
|
||||||
let what4 = lemma2∙11∙2.i r (g q) in
|
-- let what4 = lemma2∙11∙2.i r (g q) in
|
||||||
let what5 = {! !} in
|
-- let what5 = {! !} in
|
||||||
sym what4 ∙ what3
|
-- sym what4 ∙ what3
|
||||||
in
|
-- in
|
||||||
-- let what2 = what r in
|
-- -- let what2 = what r in
|
||||||
{! !}
|
-- {! !}
|
||||||
```
|
```
|
||||||
|
|
||||||
### Example 3.1.9
|
### Example 3.1.9
|
||||||
|
@ -125,56 +130,83 @@ lemma3∙1∙8 {A} A-set x y p q r s =
|
||||||
TODO: Study this more
|
TODO: Study this more
|
||||||
|
|
||||||
```
|
```
|
||||||
postulate
|
theorem3∙2∙2 : ((A : Set l) → ¬ ¬ A → A) → ⊥
|
||||||
theorem3∙2∙2 : {l : Level} → ((A : Set l) → ¬ ¬ A → A) → ⊥ {l}
|
theorem3∙2∙2 double-neg = conclusion
|
||||||
-- theorem3∙2∙2 f = let wtf = f 𝟚 in {! !}
|
where
|
||||||
-- where
|
open axiom2∙10∙3
|
||||||
-- open axiom2∙10∙3
|
|
||||||
|
|
||||||
-- p : 𝟚 ≡ 𝟚
|
bool = Lift 𝟚
|
||||||
-- p = ua neg-equiv
|
|
||||||
|
|
||||||
-- wtf : ¬ ¬ 𝟚 → 𝟚
|
negl : bool → bool
|
||||||
-- wtf = f 𝟚
|
negl (lift true) = lift false
|
||||||
|
negl (lift false) = lift true
|
||||||
|
|
||||||
-- wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
|
negl-homotopy : (negl ∘ negl) ∼ id
|
||||||
-- wtf2 = apd f p
|
negl-homotopy (lift true) = refl
|
||||||
|
negl-homotopy (lift false) = refl
|
||||||
|
|
||||||
-- wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
|
e : bool ≃ bool
|
||||||
-- wtf3 u = happly wtf2 u
|
e = negl , qinv-to-isequiv (mkQinv negl negl-homotopy negl-homotopy)
|
||||||
|
|
||||||
-- wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u))
|
p : bool ≡ bool
|
||||||
-- wtf4 u =
|
p = ua e
|
||||||
-- 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
|
fbool : ¬ ¬ bool → bool
|
||||||
-- wtf6 u v = funext (λ x → rec-⊥ (u x))
|
fbool = double-neg bool
|
||||||
|
|
||||||
-- wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
|
apdfp : transport (λ A → ¬ ¬ A → A) p fbool ≡ fbool
|
||||||
-- wtf7 u = {! !}
|
apdfp = apd double-neg p
|
||||||
|
|
||||||
-- wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
|
u : ¬ ¬ bool
|
||||||
-- wtf8 u = {! sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
|
u = λ p → p (lift true)
|
||||||
|
|
||||||
-- wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
|
foranyu : transport (λ A → ¬ ¬ A → A) p fbool u ≡ fbool u
|
||||||
-- wtf9 = {! !}
|
foranyu = happly apdfp u
|
||||||
|
|
||||||
-- wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
|
what : transport (λ A → ¬ (¬ A) → A) p fbool u ≡ transport (λ X → X) p (fbool (transport (λ X → ¬ (¬ X)) (sym p) u))
|
||||||
-- wtf10 true p = remark2∙12∙6 (sym p)
|
what =
|
||||||
-- wtf10 false p = remark2∙12∙6 p
|
let
|
||||||
|
x = equation2∙9∙4 {A = λ X → ¬ ¬ X} {B = λ X → X} fbool p
|
||||||
|
in ap (λ f → f u) x
|
||||||
|
|
||||||
-- wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u))
|
allsame : (u v : ¬ ¬ bool) → (x : ¬ bool) → u x ≡ v x
|
||||||
-- wtf11 u = wtf10 (f 𝟚 u)
|
allsame u v x = rec-⊥ (u x)
|
||||||
|
|
||||||
-- wtf12 : (u : ¬ ¬ 𝟚) → ⊥
|
postulate
|
||||||
-- wtf12 u = wtf11 u (wtf9 u)
|
allsamef : (u v : ¬ ¬ bool) → u ≡ v
|
||||||
|
|
||||||
|
all-dn-u-same : transport (λ A → ¬ ¬ A) (sym p) u ≡ u
|
||||||
|
all-dn-u-same = allsamef (transport (λ A → ¬ ¬ A) (sym p) u) u
|
||||||
|
|
||||||
|
nextStep : transport (λ A → A) p (fbool u) ≡ fbool u
|
||||||
|
nextStep =
|
||||||
|
let x = ap (λ x → transport id p (fbool x)) all-dn-u-same in
|
||||||
|
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
|
||||||
|
|
||||||
|
finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x)
|
||||||
|
finalStep (lift true) p =
|
||||||
|
let wtf = ap (λ f → Lift.lower f) p in
|
||||||
|
remark2∙12∙6.true≢false (sym wtf)
|
||||||
|
finalStep (lift false) p =
|
||||||
|
let wtf = ap (λ f → Lift.lower f) p in
|
||||||
|
remark2∙12∙6.true≢false wtf
|
||||||
|
|
||||||
|
conclusion : ⊥
|
||||||
|
conclusion = finalStep (fbool u) huhh
|
||||||
```
|
```
|
||||||
|
|
||||||
### Corollary 3.2.7
|
### Corollary 3.2.7
|
||||||
|
@ -244,6 +276,39 @@ module definition3∙4∙3 where
|
||||||
|
|
||||||
```
|
```
|
||||||
module section3∙7 where
|
module section3∙7 where
|
||||||
data ∥_∥ (A : Set) : Set where
|
postulate
|
||||||
∣_∣ : (a : A) → ∥ A ∥
|
∥_∥ : Set → Set
|
||||||
|
∣_∣ : {A : Set} → (a : A) → ∥ A ∥
|
||||||
|
witness : {A : Set} → (x y : ∥ A ∥) → x ≡ y → Set
|
||||||
|
rec-∥_∥ : (A : Set) → {B : Set} → isProp B → (f : A → B)
|
||||||
|
→ Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
|
||||||
|
open section3∙7
|
||||||
|
```
|
||||||
|
|
||||||
|
### Definition 3.7.1
|
||||||
|
|
||||||
|
## 3.9 The principle of unique choice
|
||||||
|
|
||||||
|
### Lemma 3.9.1
|
||||||
|
|
||||||
|
```
|
||||||
|
lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
|
||||||
|
lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
|
||||||
|
where
|
||||||
|
thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ id a)
|
||||||
|
thing = rec-∥ P ∥ prop id
|
||||||
|
|
||||||
|
g = Σ.fst thing
|
||||||
|
g-prop = Σ.snd thing
|
||||||
|
|
||||||
|
prop2 : isProp ∥ P ∥
|
||||||
|
prop2 x y =
|
||||||
|
let a = g-prop (g x) in
|
||||||
|
let b = g-prop (g y) in
|
||||||
|
let eqProp = prop (g x) (g y) in
|
||||||
|
let
|
||||||
|
concat : g (∣ g x ∣) ≡ g (∣ g y ∣)
|
||||||
|
concat = a ∙ eqProp ∙ (sym b)
|
||||||
|
in
|
||||||
|
{! prop ? !}
|
||||||
```
|
```
|
|
@ -3,6 +3,10 @@ module HottBook.Chapter3Definition331 where
|
||||||
|
|
||||||
open import Agda.Primitive
|
open import Agda.Primitive
|
||||||
open import HottBook.Chapter1
|
open import HottBook.Chapter1
|
||||||
|
|
||||||
|
private
|
||||||
|
variable
|
||||||
|
l : Level
|
||||||
```
|
```
|
||||||
|
|
||||||
## Definition 3.3.1
|
## Definition 3.3.1
|
||||||
|
@ -10,7 +14,7 @@ open import HottBook.Chapter1
|
||||||
[//]: <> (ANCHOR: isProp)
|
[//]: <> (ANCHOR: isProp)
|
||||||
|
|
||||||
```
|
```
|
||||||
isProp : (P : Set) → Set
|
isProp : (P : Set l) → Set l
|
||||||
isProp P = (x y : P) → x ≡ y
|
isProp P = (x y : P) → x ≡ y
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
|
@ -4,6 +4,20 @@ module HottBook.Chapter4 where
|
||||||
open import HottBook.Chapter1
|
open import HottBook.Chapter1
|
||||||
open import HottBook.Chapter2
|
open import HottBook.Chapter2
|
||||||
open import HottBook.Chapter3
|
open import HottBook.Chapter3
|
||||||
|
|
||||||
|
private
|
||||||
|
variable
|
||||||
|
l : Level
|
||||||
|
```
|
||||||
|
|
||||||
|
# Chapter 4 Equivalences
|
||||||
|
|
||||||
|
```
|
||||||
|
record satisfies-equivalence-properties {A B : Set} {f : A → B} (isequiv : (A → B) → Set) : Set where
|
||||||
|
field
|
||||||
|
qinv→isequiv : qinv f → isequiv f
|
||||||
|
isequiv→qinv : isequiv f → qinv f
|
||||||
|
isequiv-isProp : isProp (isequiv f)
|
||||||
```
|
```
|
||||||
|
|
||||||
## 4.1 Quasi-inverses
|
## 4.1 Quasi-inverses
|
||||||
|
@ -11,14 +25,32 @@ open import HottBook.Chapter3
|
||||||
### Lemma 4.1.1
|
### Lemma 4.1.1
|
||||||
|
|
||||||
```
|
```
|
||||||
lemma4∙1∙1 : {A B : Set}
|
lemma4∙1∙1 : {A B : Set} → (f : A → B) → qinv f → qinv f ≃ ((x : A) → x ≡ x)
|
||||||
→ (f : A → B)
|
lemma4∙1∙1 {A} f q = {! !}
|
||||||
→ qinv f
|
|
||||||
→ qinv f ≃ ((x : A) → x ≡ x)
|
|
||||||
lemma4∙1∙1 f q = {! !}
|
|
||||||
where
|
where
|
||||||
ff : qinv f → (x : A) → x ≡ x
|
ff : qinv f → (x : A) → x ≡ x
|
||||||
ff
|
ff = {! !}
|
||||||
|
```
|
||||||
|
|
||||||
|
### Lemma 4.1.2
|
||||||
|
|
||||||
|
```
|
||||||
|
open section3∙7
|
||||||
|
lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a)
|
||||||
|
→ isSet (a ≡ a)
|
||||||
|
→ ((x : A) → ∥ a ≡ x ∥)
|
||||||
|
→ ((p : a ≡ a) → p ∙ q ≡ q ∙ p)
|
||||||
|
→ Σ ((x : A) → x ≡ x) (λ f → f a ≡ q)
|
||||||
|
lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {! !}) , {! !}
|
||||||
|
where
|
||||||
|
allsets : (x y : A) → isSet (x ≡ y)
|
||||||
|
allsets x .x refl refl refl refl = refl
|
||||||
|
|
||||||
|
B : (x : A) → Set
|
||||||
|
B x = Σ (x ≡ x) (λ r → (s : a ≡ x) → r ≡ (sym s) ∙ q ∙ s)
|
||||||
|
|
||||||
|
BisProp : (a : A) → isProp (B a)
|
||||||
|
BisProp a x y = {! !}
|
||||||
```
|
```
|
||||||
|
|
||||||
### Theorem 4.1.3
|
### Theorem 4.1.3
|
||||||
|
@ -26,8 +58,72 @@ lemma4∙1∙1 f q = {! !}
|
||||||
There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition.
|
There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition.
|
||||||
|
|
||||||
```
|
```
|
||||||
theorem4∙1∙3 : {A B : Set}
|
theorem4∙1∙3 : ∀ {l} {A B : Set l}
|
||||||
→ (f : A → B)
|
→ Σ (A → B) (λ f → isProp (qinv f) → ⊥)
|
||||||
→ isProp (qinv f) → ⊥
|
theorem4∙1∙3 = {! !} , {! !}
|
||||||
theorem4∙1∙3 f p = {! !}
|
where
|
||||||
|
goal : Σ (Set (lsuc l)) (λ X → isProp ((x : X) → x ≡ x) → ⊥)
|
||||||
|
|
||||||
|
```
|
||||||
|
|
||||||
|
## 4.2 Half adjoint equivalences
|
||||||
|
|
||||||
|
### Definition 4.2.1
|
||||||
|
|
||||||
|
```
|
||||||
|
record ishae {A B : Set} (f : A → B) : Set where
|
||||||
|
constructor mkIshae
|
||||||
|
field
|
||||||
|
g : B → A
|
||||||
|
η : (g ∘ f) ∼ id
|
||||||
|
ε : (f ∘ g) ∼ id
|
||||||
|
τ : (x : A) → ap f (η x) ≡ ε (f x)
|
||||||
|
```
|
||||||
|
|
||||||
|
### Lemma 4.2.2
|
||||||
|
|
||||||
|
### Theorem 4.2.3
|
||||||
|
|
||||||
|
```
|
||||||
|
theorem4∙2∙3 : {A B : Set} (f : A → B) → qinv f → ishae f
|
||||||
|
theorem4∙2∙3 {A} {B} f (mkQinv g ε η) = mkIshae g' η' ε' τ
|
||||||
|
where
|
||||||
|
g' : B → A
|
||||||
|
g' = g
|
||||||
|
|
||||||
|
η' : (g' ∘ f) ∼ id
|
||||||
|
η' = η
|
||||||
|
|
||||||
|
ε' : (f ∘ g') ∼ id
|
||||||
|
ε' x = {! !}
|
||||||
|
|
||||||
|
τ : (x : A) → ap f (η' x) ≡ ε' (f x)
|
||||||
|
τ x = {! !}
|
||||||
|
```
|
||||||
|
|
||||||
|
### Definition 4.2.7
|
||||||
|
|
||||||
|
```
|
||||||
|
module definition4∙2∙7 where
|
||||||
|
linv : ∀ {A B} (f : A → B) → Set
|
||||||
|
linv {A} {B} f = Σ (B → A) (λ g → (g ∘ f) ∼ id)
|
||||||
|
|
||||||
|
rinv : ∀ {A B} (f : A → B) → Set
|
||||||
|
rinv {A} {B} f = Σ (B → A) (λ g → (f ∘ g) ∼ id)
|
||||||
|
```
|
||||||
|
|
||||||
|
### Definition 4.2.10
|
||||||
|
|
||||||
|
```
|
||||||
|
module definition4∙2∙10 where
|
||||||
|
open definition4∙2∙7
|
||||||
|
|
||||||
|
lcoh : ∀ {A} {B} → (f : A → B) → linv f → rinv f → Set
|
||||||
|
-- lcoh f (g , η) (g , ε) = ?
|
||||||
|
```
|
||||||
|
|
||||||
|
### Theorem 4.2.13
|
||||||
|
|
||||||
|
```
|
||||||
|
theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f)
|
||||||
```
|
```
|
7
src/HottBook/CoreUtil.agda
Normal file
7
src/HottBook/CoreUtil.agda
Normal file
|
@ -0,0 +1,7 @@
|
||||||
|
module HottBook.CoreUtil where
|
||||||
|
|
||||||
|
open import Agda.Primitive
|
||||||
|
|
||||||
|
record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
|
||||||
|
constructor lift
|
||||||
|
field lower : A
|
Loading…
Reference in a new issue