replace more usage of J with just refl pattern matching
This commit is contained in:
parent
18e037341a
commit
890485ab2e
1 changed files with 53 additions and 120 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue