---

Step * 1 of Lemma copathAgree-last

.....assertion..... 
1. [A] : 𝕌'
2. [B] : A ⟶ Type
⊢ ∀n:ℕ
    ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
      (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
         ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
         ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
         copathAgree(a.B[a];w;p;q) and 
         (copath-length(q) ≤ n))
BY
{ (InductionOnNat THEN RepeatFor 6 (Intro)) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ
4. [w] : coW(A;a.B[a])
5. [p] : copath(a.B[a];w)
6. [q] : copath(a.B[a];w)
7. [%] : copath-length(q) ≤ 0
8. [%1] : copathAgree(a.B[a];w;p;q)
9. [%2] : copath-length(q) = (copath-length(p) + 1) ∈ ℤ
⊢ ((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))

2
1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ
4. 0 < n
5. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
     (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
        ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
        ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
        copathAgree(a.B[a];w;p;q) and 
        (copath-length(q) ≤ (n - 1)))
6. [w] : coW(A;a.B[a])
7. [p] : copath(a.B[a];w)
8. [q] : copath(a.B[a];w)
9. [%2] : copath-length(q) ≤ n
10. [%3] : copathAgree(a.B[a];w;p;q)
11. [%4] : copath-length(q) = (copath-length(p) + 1) ∈ ℤ
⊢ ((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  \mBbbU{}'
2.  [B]  :  A  {}\mrightarrow{}  Type
\mvdash{}  \mforall{}n:\mBbbN{}
        \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p,q:copath(a.B[a];w)].
            (((fst(copath-last(w;q)))  =  copath-at(w;p))
                  \mwedge{}  (copath-at(w;q)  =  coW-item(copath-at(w;p);snd(copath-last(w;q)))))  supposing 
                  ((copath-length(q)  =  (copath-length(p)  +  1))  and 
                  copathAgree(a.B[a];w;p;q)  and 
                  (copath-length(q)  \mleq{}  n))


By

---

Latex:
(InductionOnNat  THEN  RepeatFor  6  (Intro))

---

Home Index