more progress ch4

This commit is contained in:
Michael Zhang 2024-07-12 04:37:26 -05:00
parent ab09089eb9
commit c966fa9b4f

View file

@ -6,6 +6,7 @@ open import HottBook.Chapter1Util
open import HottBook.Chapter2
open import HottBook.Chapter2Exercises
open import HottBook.Chapter3
open import HottBook.CoreUtil
private
variable
@ -119,16 +120,16 @@ There exist types A and B and a function f : A → B such that qinv( f ) is not
```
theorem4∙1∙3 : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
-- theorem4∙1∙3 {l} = goal
-- where
-- goal : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
-- where
-- goal : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
-- goal2 : ∀ {l} → Σ (Set l) (λ X → isProp ((x : X) → x ≡ x) → ⊥)
-- goal {l} = Σ.fst (goal2 {l}) , {! !} , {! !} , {! !}
-- goal2 : ∀ {l} → Σ (Set l) (λ X → isProp ((x : X) → x ≡ x) → ⊥)
-- goal {l} = Σ.fst (goal2 {l}) , {! !} , {! !} , {! !}
-- X : ∀ {l} → Set (lsuc l)
-- X {l} = Σ (Set l) (λ A → ∥ Lift 𝟚 ≡ A ∥)
-- X : ∀ {l} → Set (lsuc l)
-- X {l} = Σ (Set l) (λ A → ∥ Lift 𝟚 ≡ A ∥)
-- goal2 {l} = X {l} , ?
-- goal2 {l} = X {lsuc l} , ?
```
## 4.2 Half adjoint equivalences
@ -148,6 +149,17 @@ record ishae {A B : Set} (f : A → B) : Set where
### Lemma 4.2.2
```
lemma4∙2∙2 : ∀ {A B}
→ (f : A → B) → (g : B → A)
→ (η : (g ∘ f) id)
→ (ε : (f ∘ g) id)
→ ((x : A) → ap f (η x) ≡ ε (f x)) ≃ ((y : B) → ap g (ε y) ≡ η (g y))
lemma4∙2∙2 f g η ε = {! !}
```
```
ishae→qinv : {A B : Set} (f : A → B) → ishae f → qinv f
ishae→qinv f (mkIshae g η ε _) = mkQinv g ε η
```
### Theorem 4.2.3
@ -169,6 +181,13 @@ theorem4∙2∙3 {A} {B} f (mkQinv g ε η) = mkIshae g' η' ε' τ
τ x = {! !}
```
### Definition 4.2.4
```
fib : ∀ {A B} → (f : A → B) → (y : B) → Set
fib {A = A} f y = Σ A (λ x → f x ≡ y)
```
### Definition 4.2.7
```
@ -178,6 +197,14 @@ module definition4∙2∙7 where
rinv : ∀ {A B} (f : A → B) → Set
rinv {A} {B} f = Σ (B → A) (λ g → (f ∘ g) id)
open definition4∙2∙7
```
### Lemma 4.2.9
```
lemma4∙2∙9 : ∀ {A B} (f : A → B) → qinv f → isContr (linv f) × isContr (rinv f)
lemma4∙2∙9 f q = ({! !} , {! !}) , ({! !} , {! !})
```
### Definition 4.2.10
@ -194,4 +221,20 @@ module definition4∙2∙10 where
```
theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f)
```
## 4.3 Bi-invertible maps
### Definition 4.3.1
```
biinv : {A B : Set} (f : A → B) → Set
biinv f = linv f × rinv f
```
### Theorem 4.3.2
```
theorem4∙3∙2 : ∀ {A B} → (f : A → B) → isProp (biinv f)
theorem4∙3∙2 f = {! !}
```