---

Step * 1 of Lemma copathAgree-extend


1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. n : ℕ@i
5. p1 : coPath(a.B[a];w;n)@i
6. b : coW-dom(a.B[a];coPath-at(n;w;p1))@i
⊢ coPathAgree(a.B[a];n;w;p1;coPath-extend(n;p1;b))
BY
{ (MoveToConcl 3 THEN NatInd (-1) THEN Auto) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])@i'
4. p1 : coPath(a.B[a];w;0)@i
5. b : coW-dom(a.B[a];coPath-at(0;w;p1))@i
⊢ coPathAgree(a.B[a];0;w;p1;coPath-extend(0;p1;b))

2
1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ@i
4. [%1] : 0 < n@i
5. ∀w:coW(A;a.B[a]). ∀p1:coPath(a.B[a];w;n - 1). ∀b:coW-dom(a.B[a];coPath-at(n - 1;w;p1)).
     coPathAgree(a.B[a];n - 1;w;p1;coPath-extend(n - 1;p1;b))
6. w : coW(A;a.B[a])@i'
7. p1 : coPath(a.B[a];w;n)@i
8. b : coW-dom(a.B[a];coPath-at(n;w;p1))@i
⊢ coPathAgree(a.B[a];n;w;p1;coPath-extend(n;p1;b))

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  n  :  \mBbbN{}@i
5.  p1  :  coPath(a.B[a];w;n)@i
6.  b  :  coW-dom(a.B[a];coPath-at(n;w;p1))@i
\mvdash{}  coPathAgree(a.B[a];n;w;p1;coPath-extend(n;p1;b))


By

---

Latex:
(MoveToConcl  3  THEN  NatInd  (-1)  THEN  Auto)

---

Home Index