---

Step * 1 1 of Lemma copathAgree-extend


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))
BY
{ ((Unfold `coPathAgree` 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  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
\mvdash{}  coPathAgree(a.B[a];0;w;p1;coPath-extend(0;p1;b))


By

---

Latex:
((Unfold  `coPathAgree`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index