rewrite verbose J
This commit is contained in:
parent
bab1fe0d9f
commit
18e037341a
|
@ -841,30 +841,19 @@ module lemma2∙11∙2 where
|
||||||
→ (p : x1 ≡ x2)
|
→ (p : x1 ≡ x2)
|
||||||
→ (q : a ≡ x1)
|
→ (q : a ≡ x1)
|
||||||
→ transport (λ y → a ≡ y) p q ≡ q ∙ p
|
→ transport (λ y → a ≡ y) p q ≡ q ∙ p
|
||||||
i {l} {A} {a} {x1} {x2} p q =
|
i {l} {A} {a} {x1} {x2} refl refl = refl
|
||||||
J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1)
|
|
||||||
(λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → lemma2∙1∙4.i1 q1) a x3 q1)
|
|
||||||
x1 x2 p q
|
|
||||||
|
|
||||||
ii : {l : Level} {A : Set l} {a x1 x2 : A}
|
ii : {l : Level} {A : Set l} {a x1 x2 : A}
|
||||||
→ (p : x1 ≡ x2)
|
→ (p : x1 ≡ x2)
|
||||||
→ (q : x1 ≡ a)
|
→ (q : x1 ≡ a)
|
||||||
→ transport (λ y → y ≡ a) p q ≡ sym p ∙ q
|
→ transport (λ y → y ≡ a) p q ≡ sym p ∙ q
|
||||||
ii {l} {A} {a} {x1} {x2} p q =
|
ii {l} {A} {a} {x1} {x2} refl refl = refl
|
||||||
J (λ x y p → (q1 : x ≡ a) → transport (λ y → y ≡ a) p q1 ≡ sym p ∙ q1)
|
|
||||||
(λ x q1 → J (λ x y p → transport (λ y → y ≡ a) refl q1 ≡ sym refl ∙ q1) (λ x → lemma2∙1∙4.i2 q1) x a q1)
|
|
||||||
x1 x2 p q
|
|
||||||
|
|
||||||
iii : {l : Level} {A : Set l} {a x1 x2 : A}
|
iii : {l : Level} {A : Set l} {a x1 x2 : A}
|
||||||
→ (p : x1 ≡ x2)
|
→ (p : x1 ≡ x2)
|
||||||
→ (q : x1 ≡ x1)
|
→ (q : x1 ≡ x1)
|
||||||
→ transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
|
→ transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
|
||||||
iii {l} {A} {a} {x1} {x2} p q =
|
iii {l} {A} {a} {x1} {x2} refl refl = refl
|
||||||
J (λ x y p → (q1 : x ≡ x) → transport (λ y → y ≡ y) p q1 ≡ sym p ∙ q1 ∙ p)
|
|
||||||
(λ x q1 → J (λ x y p → transport (λ y → y ≡ y) refl q1 ≡ sym refl ∙ q1 ∙ refl)
|
|
||||||
(λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper)
|
|
||||||
x x q1)
|
|
||||||
x1 x2 p q
|
|
||||||
```
|
```
|
||||||
|
|
||||||
### Theorem 2.11.3
|
### Theorem 2.11.3
|
||||||
|
@ -1010,7 +999,7 @@ module theorem2∙13∙1 where
|
||||||
c ∎
|
c ∎
|
||||||
|
|
||||||
forward : (m n : ℕ) → (p : m ≡ n) → decode m n (encode m n p) ≡ p
|
forward : (m n : ℕ) → (p : m ≡ n) → decode m n (encode m n p) ≡ p
|
||||||
forward m n p = J (λ x y p → decode x y (encode x y p) ≡ p) f m n p
|
forward m n refl = f m
|
||||||
where
|
where
|
||||||
f : (x : ℕ) → decode x x (r x) ≡ refl
|
f : (x : ℕ) → decode x x (r x) ≡ refl
|
||||||
f zero = refl
|
f zero = refl
|
||||||
|
|
Loading…
Reference in a new issue