From 890485ab2ea94f6da98c6a6090a2325491fc71a9 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 31 May 2024 20:27:41 -0500 Subject: [PATCH] replace more usage of J with just refl pattern matching --- src/HottBook/Chapter2.lagda.md | 173 ++++++++++----------------------- 1 file changed, 53 insertions(+), 120 deletions(-) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index a02609b..9a24e62 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -19,23 +19,15 @@ open import HottBook.Util ### Lemma 2.1.1 ``` -sym : {l : Level} {A : Set l} {x y : A} - → (x ≡ y) → y ≡ x -sym {l} {A} {x} {y} p = J (λ x y p → y ≡ x) (λ x → refl) x y p +sym : {l : Level} {A : Set l} {x y : A} → (x ≡ y) → y ≡ x +sym {l} {A} {x} {y} refl = refl ``` ### Lemma 2.1.2 ``` -trans : {l : Level} {A : Set l} {x y z : A} - → (x ≡ y) - → (y ≡ z) - → (x ≡ z) -trans {l} {A} {x} {y} {z} p q = - let - func1 x y p = J (λ a b p → a ≡ b) (λ x → refl) x y p - func2 = J (λ a b p → (z : A) → (q : b ≡ z) → a ≡ z) func1 x y p - in func2 z q +trans : {l : Level} {A : Set l} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z) +trans {l} {A} {x} {y} {z} refl refl = refl infixr 30 _∙_ _∙_ = trans @@ -67,33 +59,22 @@ module ≡-Reasoning where ``` module lemma2∙1∙4 {l : Level} {A : Set l} where i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl - i1 {x} {y} p = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p + i1 {x} {y} refl = refl i2 : {x y : A} (p : x ≡ y) → p ≡ refl ∙ p - i2 {x} {y} p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p + i2 {x} {y} refl = refl ii1 : {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl - ii1 {x} {y} p = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p + ii1 {x} {y} refl = refl ii2 : {x y : A} (p : x ≡ y) → p ∙ (sym p) ≡ refl - ii2 {x} {y} p = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p + ii2 {x} {y} refl = refl iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p - iii {x} {y} p = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p + iii {x} {y} refl = refl iv : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r - iv {x} {y} {z} {w} p q r = let - open ≡-Reasoning - - C : (x y : A) → (p : x ≡ y) → Set l - C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r - - c : (x : A) → C x x refl - c x q1 = begin - refl ∙ (q1 ∙ r) ≡⟨ sym (i2 (q1 ∙ r)) ⟩ - (q1 ∙ r) ≡⟨ ap (λ p → p ∙ r) (i2 q1) ⟩ - (refl ∙ q1) ∙ r ∎ - in J C c x y p q + iv {x} {y} {z} {w} refl refl refl = refl ``` ### Definition 2.1.7 (pointed type) @@ -144,21 +125,16 @@ module lemma2∙2∙2 {A B C : Set} where open ≡-Reasoning i : {f : A → B} {x y z : A} (p : x ≡ y) (q : y ≡ z) → ap f (p ∙ q) ≡ ap f p ∙ ap f q - i {f} {x} {y} {z} p q = J - ((λ x1 y1 p1 → (q1 : y1 ≡ z) → ap f (p1 ∙ q1) ≡ ap f p1 ∙ ap f q1)) - (λ x1 q1 → J - (λ x2 y2 p2 → ap f (refl ∙ p2) ≡ ap f refl ∙ ap f p2) - (λ x2 → refl) x1 z q1 - ) x y p q + i {f} {x} {y} {z} refl refl = refl ii : {f : A → B} {x y : A} (p : x ≡ y) → ap f (sym p) ≡ sym (ap f p) - ii {f} {x} {y} p = J (λ x1 y1 p1 → ap f (sym p1) ≡ sym (ap f p1)) (λ x1 → refl) x y p + ii {f} {x} {y} refl = refl iii : (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) → ap g (ap f p) ≡ ap (g ∘ f) p - iii f g {x} {y} p = J (λ x1 y1 p1 → ap g (ap f p1) ≡ ap (g ∘ f) p1) (λ x1 → refl) x y p + iii f g {x} {y} refl = refl iv : {x y : A} (p : x ≡ y) → ap id p ≡ p - iv {x} {y} p = J (λ x1 y1 p1 → ap id p1 ≡ p1) (λ x1 → refl) x y p + iv {x} {y} refl = refl ``` ## 2.3 Type families are fibrations @@ -170,24 +146,19 @@ transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A} → (P : A → Set l₂) → (p : x ≡ y) → P x → P y -transport {l₁} {l₂} {A} {x} {y} P p = J (λ x y p → P x → P y) (λ x → id) x y p +transport {l₁} {l₂} {A} {x} {y} P refl = id ``` ### Lemma 2.3.2 (Path lifting property) -``` -lift : {A : Set} {P : A → Set} {x y : A} - → (u : P x) - → (p : x ≡ y) - → (x , u) ≡ (y , transport P p u) -lift {A} {P} {x} {y} u p = - J (λ x1 y1 p1 → (u1 : P x1) → (x1 , u1) ≡ (y1 , transport P p1 u1)) (λ x1 u1 → refl) x y p u -``` - -Verifying its property: - ``` module lemma2∙3∙2 where + lift : {A : Set} {P : A → Set} {x y : A} + → (u : P x) + → (p : x ≡ y) + → (x , u) ≡ (y , transport P p u) + lift {A} {P} {x} {y} u refl = refl + pr₁ : {A : Set} {P : A → Set} {x y : A} {u : P x} {v : P y} @@ -199,8 +170,7 @@ module lemma2∙3∙2 where lift-prop : {A : Set} {P : A → Set} {x y : A} (u : P x) → (p : x ≡ y) → pr₁ (lift {A} {P} u p) ≡ p - lift-prop {A} {P} {x} {y} u p = - J (λ x1 y1 p1 → (u1 : P x1) → pr₁ (lift {A} {P} u1 p1) ≡ p1) (λ x1 u1 → refl) x y p u + lift-prop {A} {P} {x} {y} u refl = refl ``` ### Lemma 2.3.4 (Dependent map) @@ -210,8 +180,7 @@ apd : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} {x y : A} → (f : (x : A) → P x) → (p : x ≡ y) → transport P p (f x) ≡ f y -apd {l₁} {l₂} {A} {P} {x} {y} f p = - J (λ x y p → transport P p (f x) ≡ f y) (λ x → refl) x y p +apd {l₁} {l₂} {A} {P} {x} {y} f refl = refl ``` ### Lemma 2.3.5 @@ -222,8 +191,7 @@ transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A} → (p : x ≡ y) → (b : B) → transport (λ _ → B) p b ≡ b -transportconst {l₁} {l₂} {A} {x} {y} B p b = - J (λ x y p → transport (λ _ → B) p b ≡ b) (λ x → refl) x y p +transportconst {l₁} {l₂} {A} {x} {y} B refl b = refl ``` ### Equation 2.3.6 @@ -252,8 +220,7 @@ lemma2∙3∙8 : {l : Level} {A B : Set l} → {x y : A} → (p : x ≡ y) → apd f p ≡ transportconst B p (f x) ∙ ap f p -lemma2∙3∙8 {l} {A} {B} f {x} {y} p = - J (λ x y p → apd f p ≡ transportconst B p (f x) ∙ ap f p) (λ x → refl) x y p +lemma2∙3∙8 {l} {A} {B} f {x} {y} refl = refl ``` ### Lemma 2.3.9 @@ -264,13 +231,7 @@ lemma2∙3∙9 : {A : Set} → (P : A → Set) → (p : x ≡ y) → (q : y ≡ z) → (u : P x) → transport P q (transport P p u) ≡ transport P (p ∙ q) u -lemma2∙3∙9 {A} {x} {y} {z} P p q u = - let - f2 : (x1 : A) → (q1 : x1 ≡ z) (u1 : P x1) → transport P q1 u1 ≡ transport P (refl ∙ q1) u1 - f2 x1 q1 u1 = - ap (λ x → transport P x u1) (lemma2∙1∙4.i2 q1) - f1 = J (λ x1 y1 p1 → (q1 : y1 ≡ z) → (u1 : P x1) → transport P q1 (transport P p1 u1) ≡ transport P (p1 ∙ q1) u1) f2 x y p - in f1 q u +lemma2∙3∙9 {A} {x} {y} {z} P refl refl u = refl ``` ### Lemma 2.3.10 @@ -283,9 +244,7 @@ lemma2∙3∙10 : {l1 l2 : Level} {A B : Set l1} → (p : x ≡ y) → (u : P (f x)) → transport (P ∘ f) p u ≡ transport P (ap f p) u -lemma2∙3∙10 {l} {A} {B} f P {x} {y} p u = - J (λ x1 y1 p1 → (u1 : P (f x1)) → transport (P ∘ f) p1 u1 ≡ transport P (ap f p1) u1) - (λ x1 u1 → refl) x y p u +lemma2∙3∙10 {l} {A} {B} f P {x} {y} refl u = refl ``` ### Lemma 2.3.11 @@ -295,9 +254,7 @@ lemma2∙3∙11 : {A : Set} {P Q : A → Set} → (f : (x : A) → P x → Q x) → {x y : A} (p : x ≡ y) → (u : P x) → transport Q p (f x u) ≡ f y (transport P p u) -lemma2∙3∙11 {A} {P} {Q} f {x} {y} p u = - J (λ x1 y1 p1 → (u1 : P x1) → transport Q p1 (f x1 u1) ≡ f y1 (transport P p1 u1)) - (λ x1 u1 → refl) x y p u +lemma2∙3∙11 {A} {P} {Q} f {x} {y} refl u = refl ``` ## 2.4 Homotopies and equivalences @@ -340,16 +297,14 @@ Homotopy forms an equivalence relation: ``` lemma2∙4∙3 : {A B : Set} {f g : A → B} (H : f ∼ g) {x y : A} (p : x ≡ y) → H x ∙ ap g p ≡ ap f p ∙ H y -lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} p = let - open ≡-Reasoning - in - J (λ x1 y1 p1 → (H x1 ∙ ap g p1 ≡ ap f p1 ∙ H y1)) (λ x1 → begin - H x1 ∙ ap g refl ≡⟨⟩ - H x1 ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (H x1)) ⟩ - H x1 ≡⟨ lemma2∙1∙4.i2 (H x1) ⟩ - refl ∙ H x1 ≡⟨⟩ - ap f refl ∙ H x1 ∎ - ) x y p +lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} refl = + let open ≡-Reasoning in + begin + H x ∙ ap g refl ≡⟨⟩ + H x ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (H x)) ⟩ + H x ≡⟨ lemma2∙1∙4.i2 (H x) ⟩ + refl ∙ H x ≡⟨⟩ + ap f refl ∙ H x ∎ ``` ### Corollary 2.4.4 @@ -704,9 +659,7 @@ equation2∙9∙4 : {l1 l2 : Level} {X : Set l1} {x1 x2 : X} → (f : A x1 → B x1) → (p : x1 ≡ x2) → transport (λ x → A x → B x) p f ≡ λ x → transport B p (f (transport A (sym p) x)) -equation2∙9∙4 {l1} {l2} {X} {x1} {x2} {A} {B} f p = - J (λ x3 y3 p1 → (f1 : A x3 → B x3) → (transport (λ x → A x → B x) p1 f1 ≡ λ x → transport B p1 (f1 (transport A (sym p1) x)))) - (λ x3 f1 → refl) x1 x2 p f +equation2∙9∙4 {l1} {l2} {X} {x1} {x2} {A} {B} f refl = refl ``` ### Equation 2.9.5 @@ -730,9 +683,7 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where → (p : x1 ≡ x2) → (a : A x2) → transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡-d (sym p) refl)) (f (transport A (sym p) a)) - equation2∙9∙5 A B f p a = - J (λ x1' x2' p' → (f' : (a : A x1') → B x1' a) → (a' : A x2') → transport (Π A B) p' f' a' ≡ transport (hat B) (sym (pair-≡-d (sym p') refl)) (f' (transport A (sym p') a'))) - (λ x' f' a' → refl) x1 x2 p f a + equation2∙9∙5 A B f refl a = refl ``` ### Lemma 2.9.6 @@ -761,13 +712,6 @@ idtoeqv : {l : Level} {A B : Set l} → (A ≡ B) → (A ≃ B) idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A --- idtoeqv {l} {A} {B} p = J C c A B p - -- where - -- C : (x y : Set l) (p : x ≡ y) → Set l - -- C x y p = x ≃ y - - -- c : (x : Set l) → C x x refl - -- c x = id , qinv-to-isequiv id-qinv ``` ### Axiom 2.10.3 (Univalence) @@ -863,13 +807,9 @@ theorem2∙11∙3 : {A B : Set} → {f g : A → B} → {a a' : A} → (p : a ≡ a') → (q : f a ≡ g a) → transport (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ (ap g p) -theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} p q = - J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (ap f p) ∙ q1 ∙ (ap g p)) - (λ x q1 → - J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (ap f refl) ∙ q1 ∙ ap g refl) - (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper) - (f a) (g a) q) - a a' p q +theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} refl q = + let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q) in + lemma2∙1∙4.i2 q ∙ helper ``` ### Theorem 2.11.4 @@ -879,25 +819,18 @@ theorem2∙11∙4 : {A : Set} {B : A → Set} {f g : (x : A) → B x} {a a' : A} → (p : a ≡ a') → (q : f a ≡ g a) → transport (λ x → f x ≡ g x) p q ≡ sym (apd f p) ∙ ap (transport B p) q ∙ apd g p -theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} p q = - let open ≡-Reasoning in - J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (apd f p) ∙ ap (transport B p) q1 ∙ apd g p) - (λ x q1 → - J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (apd f refl) ∙ ap (transport B refl) q1 ∙ apd g refl) - (λ y → - let - q2 = ap id q1 - q1≡q2 : q1 ≡ q2 - q1≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f x) (g x) q1 - in - begin - transport (λ z → f z ≡ g z) refl q1 ≡⟨⟩ - q1 ≡⟨ q1≡q2 ⟩ - q2 ≡⟨ (let helper = ap (λ p → refl ∙ p) (lemma2∙1∙4.i1 q2) in lemma2∙1∙4.i2 q2 ∙ helper) ⟩ - refl ∙ ap (transport B refl) q1 ∙ refl ∎ - ) - (f a) (g a) q) - a a' p q +theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q = + let + open ≡-Reasoning + q2 = ap id q + q≡q2 : q ≡ q2 + q≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f a) (g a) q + in + begin + transport (λ z → f z ≡ g z) refl q ≡⟨⟩ + q ≡⟨ q≡q2 ⟩ + q2 ≡⟨ (let helper = ap (λ p → refl ∙ p) (lemma2∙1∙4.i1 q2) in lemma2∙1∙4.i2 q2 ∙ helper) ⟩ + refl ∙ ap (transport B refl) q ∙ refl ∎ ``` ### Theorem 2.11.5