---

Step * 1 1 2 1 of Lemma pcw-path-copathAgree

.....truecase..... 
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path
5. StepAgree(path 0;⋅;w)
6. i : ℕ
7. pcw-path-coPath(i;path) ∈ copath(a.B[a];w)
8. pcw-path-coPath(i + 1;path) ∈ copath(a.B[a];w)
9. copath-length(pcw-path-coPath(i + 1;path)) = (i + 1) ∈ ℤ
10. copath-at(w;pcw-path-coPath(i + 1;path)) = (fst(snd((path (i + 1))))) ∈ coW(A;a.B[a])
11. copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ
12. copath-at(w;pcw-path-coPath(i;path)) = (fst(snd((path i)))) ∈ coW(A;a.B[a])
13. ¬((i + 1) = 0 ∈ ℤ)
14. p : Unit
15. w1 : pco-W p
16. x : B[fst(w1)]
17. (path i) = <p, w1, inl x> ∈ pcw-step(Unit;p.A;p,a.B[a];p,a,b.⋅)
18. copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ
⊢ ↓copathAgree(a.B[a];w;pcw-path-coPath(i;path);copath-extend(pcw-path-coPath(i;path);x))
BY
{ ((GenConclTerm ⌜pcw-path-coPath(i;path)⌝⋅ THENA Auto) THEN D -2 THEN RepUR ``copathAgree`` 0) }

1
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path
5. StepAgree(path 0;⋅;w)
6. i : ℕ
7. pcw-path-coPath(i;path) ∈ copath(a.B[a];w)
8. pcw-path-coPath(i + 1;path) ∈ copath(a.B[a];w)
9. copath-length(pcw-path-coPath(i + 1;path)) = (i + 1) ∈ ℤ
10. copath-at(w;pcw-path-coPath(i + 1;path)) = (fst(snd((path (i + 1))))) ∈ coW(A;a.B[a])
11. copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ
12. copath-at(w;pcw-path-coPath(i;path)) = (fst(snd((path i)))) ∈ coW(A;a.B[a])
13. ¬((i + 1) = 0 ∈ ℤ)
14. p : Unit
15. w1 : pco-W p
16. x : B[fst(w1)]
17. (path i) = <p, w1, inl x> ∈ pcw-step(Unit;p.A;p,a.B[a];p,a,b.⋅)
18. copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ
19. n : ℕ
20. v1 : coPath(a.B[a];w;n)
21. pcw-path-coPath(i;path) = <n, v1> ∈ copath(a.B[a];w)
⊢ ↓if (n) < (n + 1)
      then coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;x))
      else coPathAgree(a.B[a];n + 1;w;v1;coPath-extend(n;v1;x))

---

Latex:

---

Latex:
.....truecase..... 
1.  [A]  :  \mBbbU{}'
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  path  :  Path
5.  StepAgree(path  0;\mcdot{};w)
6.  i  :  \mBbbN{}
7.  pcw-path-coPath(i;path)  \mmember{}  copath(a.B[a];w)
8.  pcw-path-coPath(i  +  1;path)  \mmember{}  copath(a.B[a];w)
9.  copath-length(pcw-path-coPath(i  +  1;path))  =  (i  +  1)
10.  copath-at(w;pcw-path-coPath(i  +  1;path))  =  (fst(snd((path  (i  +  1)))))
11.  copath-length(pcw-path-coPath(i;path))  =  i
12.  copath-at(w;pcw-path-coPath(i;path))  =  (fst(snd((path  i))))
13.  \mneg{}((i  +  1)  =  0)
14.  p  :  Unit
15.  w1  :  pco-W  p
16.  x  :  B[fst(w1)]
17.  (path  i)  =  <p,  w1,  inl  x>
18.  copath-length(pcw-path-coPath(i;path))  =  i
\mvdash{}  \mdownarrow{}copathAgree(a.B[a];w;pcw-path-coPath(i;path);copath-extend(pcw-path-coPath(i;path);x))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}pcw-path-coPath(i;path)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  RepUR  ``copathAgree``  0)

---

Home Index