Step
*
1
1
1
2
1
1
1
1
1
of Lemma
W-wfdd
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. p : n:ℕ ⟶ copath(a.B[a];w)
5. ∀i:ℕ
((copath-length(p i) = i ∈ ℤ) ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ) ⇒ copathAgree(a.B[a];w;p i;p (i + 1)))
6. copath-length(p 0) = 0 ∈ ℤ
7. i : ℕ
8. a : A
9. v1 : B[a] ⟶ coW(A;a.B[a])
10. copath-at(w;p i) = <a, v1> ∈ coW(A;a.B[a])
11. copath-length(p i) = i ∈ ℤ
12. copath-length(p (i + 1)) = (i + 1) ∈ ℤ
13. copathAgree(a.B[a];w;p i;p (i + 1))
14. w' : coW(A;a.B[a])
15. v2 : coW-dom(a.B[a];w')
16. copath-last(w;p (i + 1)) = <w', v2> ∈ (w':coW(A;a.B[a]) × coW-dom(a.B[a];w'))
17. w' = copath-at(w;p i) ∈ coW(A;a.B[a])
18. v2 ∈ B[a]
⊢ coW-item(copath-at(w;p i);v2) = (v1 v2) ∈ coW(A;a.B[a])
BY
{ (StrengthenEquation (-9) THEN ApFunToHypEquands `Z' ⌜coW-item(Z;v2)⌝ coW(A;a.B[a]) (-1)⋅) }
1
.....fun wf.....
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. p : n:ℕ ⟶ copath(a.B[a];w)
5. ∀i:ℕ
((copath-length(p i) = i ∈ ℤ) ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ) ⇒ copathAgree(a.B[a];w;p i;p (i + 1)))
6. copath-length(p 0) = 0 ∈ ℤ
7. i : ℕ
8. a : A
9. v1 : B[a] ⟶ coW(A;a.B[a])
10. copath-at(w;p i) = <a, v1> ∈ coW(A;a.B[a])
11. copath-length(p i) = i ∈ ℤ
12. copath-length(p (i + 1)) = (i + 1) ∈ ℤ
13. copathAgree(a.B[a];w;p i;p (i + 1))
14. w' : coW(A;a.B[a])
15. v2 : coW-dom(a.B[a];w')
16. copath-last(w;p (i + 1)) = <w', v2> ∈ (w':coW(A;a.B[a]) × coW-dom(a.B[a];w'))
17. w' = copath-at(w;p i) ∈ coW(A;a.B[a])
18. v2 ∈ B[a]
19. copath-at(w;p i)
= <a, v1>
∈ {z:coW(A;a.B[a])| (z = copath-at(w;p i) ∈ coW(A;a.B[a])) ∧ (z = <a, v1> ∈ coW(A;a.B[a]))}
20. Z : {z:coW(A;a.B[a])| (z = copath-at(w;p i) ∈ coW(A;a.B[a])) ∧ (z = <a, v1> ∈ coW(A;a.B[a]))}
⊢ coW-item(Z;v2) = coW-item(Z;v2) ∈ coW(A;a.B[a])
2
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. p : n:ℕ ⟶ copath(a.B[a];w)
5. ∀i:ℕ
((copath-length(p i) = i ∈ ℤ) ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ) ⇒ copathAgree(a.B[a];w;p i;p (i + 1)))
6. copath-length(p 0) = 0 ∈ ℤ
7. i : ℕ
8. a : A
9. v1 : B[a] ⟶ coW(A;a.B[a])
10. copath-at(w;p i) = <a, v1> ∈ coW(A;a.B[a])
11. copath-length(p i) = i ∈ ℤ
12. copath-length(p (i + 1)) = (i + 1) ∈ ℤ
13. copathAgree(a.B[a];w;p i;p (i + 1))
14. w' : coW(A;a.B[a])
15. v2 : coW-dom(a.B[a];w')
16. copath-last(w;p (i + 1)) = <w', v2> ∈ (w':coW(A;a.B[a]) × coW-dom(a.B[a];w'))
17. w' = copath-at(w;p i) ∈ coW(A;a.B[a])
18. v2 ∈ B[a]
19. copath-at(w;p i)
= <a, v1>
∈ {z:coW(A;a.B[a])| (z = copath-at(w;p i) ∈ coW(A;a.B[a])) ∧ (z = <a, v1> ∈ coW(A;a.B[a]))}
20. coW-item(copath-at(w;p i);v2) = coW-item(<a, v1>;v2) ∈ coW(A;a.B[a])
⊢ coW-item(copath-at(w;p i);v2) = (v1 v2) ∈ coW(A;a.B[a])
Latex:
Latex:
1. A : \mBbbU{}'
2. B : A {}\mrightarrow{} Type
3. w : coW(A;a.B[a])
4. p : n:\mBbbN{} {}\mrightarrow{} copath(a.B[a];w)
5. \mforall{}i:\mBbbN{}
((copath-length(p i) = i)
{}\mRightarrow{} (copath-length(p (i + 1)) = (i + 1))
{}\mRightarrow{} copathAgree(a.B[a];w;p i;p (i + 1)))
6. copath-length(p 0) = 0
7. i : \mBbbN{}
8. a : A
9. v1 : B[a] {}\mrightarrow{} coW(A;a.B[a])
10. copath-at(w;p i) = <a, v1>
11. copath-length(p i) = i
12. copath-length(p (i + 1)) = (i + 1)
13. copathAgree(a.B[a];w;p i;p (i + 1))
14. w' : coW(A;a.B[a])
15. v2 : coW-dom(a.B[a];w')
16. copath-last(w;p (i + 1)) = <w', v2>
17. w' = copath-at(w;p i)
18. v2 \mmember{} B[a]
\mvdash{} coW-item(copath-at(w;p i);v2) = (v1 v2)
By
Latex:
(StrengthenEquation (-9) THEN ApFunToHypEquands `Z' \mkleeneopen{}coW-item(Z;v2)\mkleeneclose{} coW(A;a.B[a]) (-1)\mcdot{})
Home
Index