wip
This commit is contained in:
parent
81fb1d0c77
commit
9e1da47565
3 changed files with 235 additions and 18 deletions
160
src/HDTT/hw2-handout.agda
Normal file
160
src/HDTT/hw2-handout.agda
Normal file
|
|
@ -0,0 +1,160 @@
|
|||
{-# OPTIONS --without-K #-}
|
||||
|
||||
module HDTT.hw2-handout where
|
||||
|
||||
Type = Set₀
|
||||
|
||||
record Σ (A : Type) (B : A → Type) : Type where
|
||||
constructor _,_
|
||||
field
|
||||
fst : A
|
||||
snd : B fst
|
||||
open Σ public
|
||||
infixr 60 _,_
|
||||
|
||||
data _⊔_ (A : Type) (B : Type) : Type where
|
||||
inl : A → A ⊔ B
|
||||
inr : B → A ⊔ B
|
||||
infixr 4 _⊔_
|
||||
|
||||
data ⊥ : Type where
|
||||
|
||||
abort : ∀ {A : Type} → ⊥ → A
|
||||
abort ()
|
||||
|
||||
data ℕ : Type where
|
||||
zero : ℕ
|
||||
suc : (n : ℕ) → ℕ
|
||||
{-# BUILTIN NATURAL ℕ #-}
|
||||
|
||||
data _≡_ {A : Type} (x : A) : A → Type where
|
||||
refl : x ≡ x
|
||||
|
||||
_∙_ : ∀ {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
|
||||
refl ∙ q = q
|
||||
infixr 80 _∙_
|
||||
|
||||
!_ : ∀ {A : Type} {x y : A} → x ≡ y → y ≡ x
|
||||
! refl = refl
|
||||
infixr 100 !_
|
||||
|
||||
{- Lots of lemmas which may or may not be useful. -}
|
||||
|
||||
∙-unit-r : ∀ {A : Type} {x y : A} (q : x ≡ y) → q ∙ refl ≡ q
|
||||
∙-unit-r refl = refl
|
||||
|
||||
∙-unit-l : ∀ {A : Type} {x y : A} (q : x ≡ y) → refl ∙ q ≡ q
|
||||
∙-unit-l q = refl
|
||||
|
||||
!-inv-l : ∀ {A : Type} {x y : A} (p : x ≡ y) → (! p) ∙ p ≡ refl
|
||||
!-inv-l refl = refl
|
||||
|
||||
!-inv-r : ∀ {A : Type} {x y : A} (p : x ≡ y) → p ∙ (! p) ≡ refl
|
||||
!-inv-r refl = refl
|
||||
|
||||
!-! : ∀ {A : Type} {x y : A} (p : x ≡ y) → ! (! p) ≡ p
|
||||
!-! refl = refl
|
||||
|
||||
∙-assoc : ∀ {A : Type} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
|
||||
→ (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
|
||||
∙-assoc refl q r = refl
|
||||
|
||||
ap : ∀ {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
|
||||
ap f refl = refl
|
||||
|
||||
ap-∙ : ∀ {A B : Type} (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
|
||||
→ ap f (p ∙ q) ≡ ap f p ∙ ap f q
|
||||
ap-∙ f refl q = refl
|
||||
|
||||
ap-! : ∀ {A B : Type} (f : A → B) {x y : A} (p : x ≡ y) → ap f (! p) ≡ ! (ap f p)
|
||||
ap-! f refl = refl
|
||||
|
||||
------------------------------------------------------------------------------------
|
||||
{- Task 1 -}
|
||||
------------------------------------------------------------------------------------
|
||||
|
||||
-- loop spaces
|
||||
Ω² : ∀ (A : Type) → A → Type
|
||||
Ω² A x = (refl {x = x}) ≡ refl
|
||||
|
||||
{- Task 1.1: prove this lemma -}
|
||||
ap-id : ∀ {A : Type} {x y : A} (p : x ≡ y) → ap (λ x → x) p ≡ p
|
||||
ap-id refl = refl
|
||||
|
||||
-- binary version of ap
|
||||
ap2 : ∀ {A B C : Type} (f : A → B → C) {x y : A} → x ≡ y → {z w : B} → z ≡ w → f x z ≡ f y w
|
||||
ap2 f {x} {y} p {z} {w} q = ap (λ a → f a z) p ∙ ap (λ b → f y b) q
|
||||
|
||||
{- Task 1.2: find another way to implement ap2 that is "symmetric" to the above ap2 -}
|
||||
ap2' : ∀ {A B C : Type} (f : A → B → C) {x y : A} → x ≡ y → {z w : B} → z ≡ w → f x z ≡ f y w
|
||||
ap2' f {x} refl q = ap (f x) q
|
||||
|
||||
-- You might find this useful in Tasks 1.3 and 1.4
|
||||
lemma₀ : ∀ {A : Type} {x : A} (p : Ω² A x) → ap (λ x → x ∙ refl) p ≡ p
|
||||
lemma₀ {x = x} p = lemma₀' p ∙ ∙-unit-r p where
|
||||
lemma₀' : ∀ {l : x ≡ x} (p : refl ≡ l) → ap (λ x → x ∙ refl) p ≡ p ∙ ! (∙-unit-r l)
|
||||
lemma₀' refl = refl
|
||||
|
||||
{- Task 1.3: check the definition of `ap2` and prove this lemma -}
|
||||
task1-3 : ∀ {A : Type} {x : A} (p q : Ω² A x) → ap2 (λ x y → x ∙ y) p q ≡ p ∙ q
|
||||
task1-3 p q = {! !} where
|
||||
{- Hints:
|
||||
1. What are the implicit arguments x, y, z, and w when applying ap2?
|
||||
2. What's the relation between λ x → x and λ x → refl ∙ x? -}
|
||||
|
||||
{- Task 1.4: prove this lemma -}
|
||||
task1-4 : ∀ {A : Type} {x : A} (p q : Ω² A x) → ap2' (λ x y → x ∙ y) p q ≡ q ∙ p
|
||||
task1-4 p q = {! !}
|
||||
|
||||
{- Task 1.5: prove that ap2 f p q ≡ ap2' f p q -}
|
||||
task1-5 : ∀ {A B C : Type} (f : A → B → C) {x y : A} (p : x ≡ y) {z w : B} (q : z ≡ w) → ap2 f p q ≡ ap2' f p q
|
||||
task1-5 f refl refl = refl
|
||||
|
||||
{- Task 1.6: the final theorem -}
|
||||
eckmann-hilton : ∀ {A : Type} {x : A} (p q : Ω² A x) → p ∙ q ≡ q ∙ p
|
||||
eckmann-hilton p q = {! !}
|
||||
|
||||
------------------------------------------------------------------------------------
|
||||
{- Task 2 -}
|
||||
------------------------------------------------------------------------------------
|
||||
|
||||
¬_ : Type → Type
|
||||
¬ A = A → ⊥
|
||||
|
||||
has-all-paths : Type → Type
|
||||
has-all-paths A = (x y : A) → x ≡ y
|
||||
|
||||
{- This version is different from what we had on 2/13.
|
||||
One can show "has-all-paths" and "is-prop" are equivalent. -}
|
||||
is-set : Type → Type
|
||||
is-set A = (x y : A) → has-all-paths (x ≡ y)
|
||||
{- for comparison: the one on 2/13 was: is-set A = (x y : A) → is-prop (x ≡ y) -}
|
||||
|
||||
has-dec-eq : Type → Type
|
||||
has-dec-eq A = (x y : A) → (x ≡ y) ⊔ (¬ (x ≡ y))
|
||||
|
||||
replacement₁ : ∀ {A : Type} → has-dec-eq A → {x y : A} → x ≡ y → x ≡ y
|
||||
replacement₁ dec {x} {y} p with dec x y
|
||||
... | inl q = q
|
||||
... | inr ¬p = abort (¬p p)
|
||||
|
||||
replacement₂ : ∀ {A : Type} → has-dec-eq A → {x y : A} → x ≡ y → x ≡ y
|
||||
replacement₂ dec p = ! (replacement₁ dec refl) ∙ replacement₁ dec p
|
||||
|
||||
{- Task 2.1: the replacement is an identity function -}
|
||||
task2-1 : ∀ {A : Type} (dec : has-dec-eq A) {x y : A} (p : x ≡ y) → replacement₂ dec p ≡ p
|
||||
task2-1 dec refl = {! refl !}
|
||||
|
||||
{- Task 2.2: the replacement is (weakly) constant -}
|
||||
task2-2 : ∀ {A : Type} (dec : has-dec-eq A) {x y : A} (p q : x ≡ y) → replacement₂ dec p ≡ replacement₂ dec q
|
||||
task2-2 = {! !}
|
||||
{- hints: start with "task2-2 dec {x} {y} p q with dec x y".
|
||||
Agda will simplify the goal with the knowledge obtained from the pattern matching. -}
|
||||
|
||||
{- Task 2.3: so... A is a set! -}
|
||||
hedberg : ∀ {A : Type} → has-dec-eq A → is-set A
|
||||
hedberg = {! !}
|
||||
{- hints: if you are lost, start with "hedberg dec x y p q = {!!}" and use "C-c C-e"
|
||||
to see the type of the hole in Emacs. -}
|
||||
|
||||
-- Done? Remove the definition of "magic" to make sure you did not forget anything.
|
||||
|
|
@ -97,14 +97,8 @@ Use funExt⁻ to prove isSetΠ:
|
|||
|
||||
```agda
|
||||
isSetΠ : (h : (x : A) → isSet (B x)) → isSet ((x : A) → B x)
|
||||
isSetΠ h =
|
||||
λ p q → -- p, q : (x : A) → B x
|
||||
λ r s → -- r, s : p ≡ q
|
||||
λ i j → -- j : p ≡ q, i : r j ≡ s j
|
||||
λ x →
|
||||
let
|
||||
test = funExt⁻ r x
|
||||
in {! !}
|
||||
isSetΠ h = λ f g → λ p q → λ i j → λ x →
|
||||
(h x) (f x) (g x) (funExt⁻ p x) (funExt⁻ q x) i j
|
||||
```
|
||||
|
||||
### Exercise 7 (★★★): alternative contractibility of singletons
|
||||
|
|
@ -121,7 +115,7 @@ Prove the corresponding version of contractibility of singetons for
|
|||
|
||||
```agda
|
||||
isContrSingl' : (x : A) → isContr (singl' x)
|
||||
isContrSingl' x = {!!}
|
||||
isContrSingl' x = (x , refl) , λ (y , p) i → p (~ i) , λ j → p (~ i ∨ j)
|
||||
```
|
||||
|
||||
## Part III: Equality in Σ-types
|
||||
|
|
@ -146,10 +140,10 @@ module _ {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} where
|
|||
PathPΣ p = (λ i → Σ.fst (p i)) , (λ i → Σ.snd (p i))
|
||||
|
||||
ΣPathP-PathPΣ : ∀ p → PathPΣ (ΣPathP p) ≡ p
|
||||
ΣPathP-PathPΣ = {!!}
|
||||
ΣPathP-PathPΣ (p , p2) i = p , p2
|
||||
|
||||
PathPΣ-ΣPathP : ∀ p → ΣPathP (PathPΣ p) ≡ p
|
||||
PathPΣ-ΣPathP = {!!}
|
||||
PathPΣ-ΣPathP p i = p
|
||||
```
|
||||
|
||||
If one looks carefully the proof of prf in Lecture 7 uses ΣPathP
|
||||
|
|
@ -182,7 +176,26 @@ Prove
|
|||
|
||||
```agda
|
||||
suspUnitChar : Susp Unit ≡ Interval
|
||||
suspUnitChar = {!!}
|
||||
suspUnitChar = isoToPath (iso f g fg gf) where
|
||||
f : Susp Unit → Interval
|
||||
f north = zero
|
||||
f south = one
|
||||
f (merid a i) = seg i
|
||||
|
||||
g : Interval → Susp Unit
|
||||
g zero = north
|
||||
g one = south
|
||||
g (seg i) = merid ⋆ i
|
||||
|
||||
fg : section f g
|
||||
fg zero = refl
|
||||
fg one = refl
|
||||
fg (seg i) j = seg i
|
||||
|
||||
gf : retract f g
|
||||
gf north = refl
|
||||
gf south = refl
|
||||
gf (merid ⋆ i) j = merid ⋆ i
|
||||
```
|
||||
|
||||
|
||||
|
|
@ -197,11 +210,6 @@ Define suspension using the Pushout HIT and prove that it's equal to Susp.
|
|||
|
||||
The goal of this exercise is to prove
|
||||
|
||||
```agda
|
||||
suspBoolChar : Susp Bool ≡ S¹
|
||||
suspBoolChar = {!!}
|
||||
```
|
||||
|
||||
For the map `Susp Bool → S¹`, we have to specify the behavior of two
|
||||
path constructors. The idea is to map one to `loop` and one to `refl`.
|
||||
|
||||
|
|
@ -249,3 +257,52 @@ result, that is a direct consequence of `comp-filler` in `Cubical Agda`
|
|||
rUnit : {x y : A} (p : x ≡ y) → p ∙ refl ≡ p
|
||||
rUnit p = sym (comp-filler p refl)
|
||||
```
|
||||
|
||||
```agda
|
||||
suspBoolChar : Susp Bool ≡ S¹
|
||||
suspBoolChar = isoToPath (iso f g fg gf) where
|
||||
f : Susp Bool → S¹
|
||||
f north = base
|
||||
f south = base
|
||||
f (merid true i) = loop i
|
||||
f (merid false i) = refl {x = base} i
|
||||
|
||||
g : S¹ → Susp Bool
|
||||
g base = north
|
||||
g (loop i) = (merid true ∙ sym (merid false)) i
|
||||
|
||||
q = ap
|
||||
|
||||
fg : section f g -- f(g(x)) ≡ x
|
||||
fg base = refl
|
||||
fg (loop i) k =
|
||||
-- f(g(loop)) ≡ loop
|
||||
-- f(merid true ∙ sym (merid false)) ≡ loop
|
||||
-- ap f (merid true) ∙ ap f (sym (merid false)) ≡ loop
|
||||
-- (loop) ∙ (refl) ≡ loop
|
||||
let
|
||||
-- bottomFace = λ j =
|
||||
-- let u = λ k → λ where
|
||||
-- (i = i0) → f (refl {x = north} j)
|
||||
-- (i = i1) → f (merid false (~ j))
|
||||
-- in hfill u (inS (f (merid true i))) j
|
||||
|
||||
-- leftFace =
|
||||
-- let u = λ j → λ where
|
||||
-- (i = i0) → f (refl {x = north} j)
|
||||
-- (i = i1) → f (merid false (~ j))
|
||||
-- in hfill u (inS (f (merid true i))) {! !}
|
||||
|
||||
u = λ j → λ where
|
||||
(i = i0) → base
|
||||
(i = i1) → f (merid false (~ j))
|
||||
(k = i0) → comp-filler (λ i → f (merid true i)) (λ j → f (merid false (~ j))) j i
|
||||
(k = i1) → loop i
|
||||
in hcomp u (f (merid true i))
|
||||
|
||||
gf : retract f g -- g(f(x)) ≡ x
|
||||
gf north = refl
|
||||
gf south = merid false
|
||||
gf (merid false i) j = merid false (i ∧ j)
|
||||
gf (merid true i) j = {! !}
|
||||
```
|
||||
|
|
@ -40,7 +40,7 @@ Prove the propositional computation law for `J`:
|
|||
```agda
|
||||
JRefl : {A : Type ℓ} {x : A} (P : (z : A) → x ≡ z → Type ℓ'')
|
||||
(d : P x refl) → J P d refl ≡ d
|
||||
JRefl P d = {!!}
|
||||
JRefl P d i = {! !}
|
||||
```
|
||||
|
||||
### Exercise 2 (★★)
|
||||
|
|
|
|||
Loading…
Reference in a new issue