{-# OPTIONS --without-K #-} 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} {y} p {z} {w} q = ap (λ b → f x b) q ∙ ap (λ a → f a w) p -- 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} {m : 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 = ap2 (λ x y → x ∙ y) (lemma₀ p) (ap-id q) {- 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 = ap2 (λ x y → x ∙ y) (ap-id q) (lemma₀ p) {- 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 = ! (task1-3 p q) ∙ task1-5 (λ x y → x ∙ y) p q ∙ task1-4 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 = !-inv-l (replacement₁ dec 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 dec {x} {y} p q with dec x y ... | inl _ = refl ... | inr ¬p = abort (¬p p) {- 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 dec x y p q = ! (task2-1 dec p) ∙ task2-2 dec p q ∙ task2-1 dec q {- 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.