---

Step * of Lemma pcw-path-coPath_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:Path].
  ∀[n:ℕ]
    ((pcw-path-coPath(n;p) ∈ copath(a.B[a];w))
    ∧ ((copath-length(pcw-path-coPath(n;p)) = n ∈ ℤ)
      ⇒ (copath-at(w;pcw-path-coPath(n;p)) = (fst(snd((p n)))) ∈ coW(A;a.B[a])))) 
  supposing StepAgree(p 0;⋅;w)
BY
{ (Intros THEN UseWitness ⌜<Ax, λx.Ax>⌝⋅ THEN NatInd (-1)) }

1
.....basecase..... 
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. p : Path
5. StepAgree(p 0;⋅;w)
6. n : ℤ
⊢ <Ax, λx.Ax> ∈ (pcw-path-coPath(0;p) ∈ copath(a.B[a];w))
  ∧ ((copath-length(pcw-path-coPath(0;p)) = 0 ∈ ℤ)
    ⇒ (copath-at(w;pcw-path-coPath(0;p)) = (fst(snd((p 0)))) ∈ coW(A;a.B[a])))

2
.....upcase..... 
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. p : Path
5. StepAgree(p 0;⋅;w)
6. n : ℤ
7. 0 < n
8. <Ax, λx.Ax> ∈ (pcw-path-coPath(n - 1;p) ∈ copath(a.B[a];w))
   ∧ ((copath-length(pcw-path-coPath(n - 1;p)) = (n - 1) ∈ ℤ)
     ⇒ (copath-at(w;pcw-path-coPath(n - 1;p)) = (fst(snd((p (n - 1))))) ∈ coW(A;a.B[a])))
⊢ <Ax, λx.Ax> ∈ (pcw-path-coPath(n;p) ∈ copath(a.B[a];w))
  ∧ ((copath-length(pcw-path-coPath(n;p)) = n ∈ ℤ)
    ⇒ (copath-at(w;pcw-path-coPath(n;p)) = (fst(snd((p n)))) ∈ coW(A;a.B[a])))

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p:Path].
    \mforall{}[n:\mBbbN{}]
        ((pcw-path-coPath(n;p)  \mmember{}  copath(a.B[a];w))
        \mwedge{}  ((copath-length(pcw-path-coPath(n;p))  =  n)
            {}\mRightarrow{}  (copath-at(w;pcw-path-coPath(n;p))  =  (fst(snd((p  n))))))) 
    supposing  StepAgree(p  0;\mcdot{};w)


By

---

Latex:
(Intros  THEN  UseWitness  \mkleeneopen{}<Ax,  \mlambda{}x.Ax>\mkleeneclose{}\mcdot{}  THEN  NatInd  (-1))

---

Home Index