---

Step * of Lemma copathAgree-extend

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].
  ∀p:copath(a.B[a];w). ∀b:coW-dom(a.B[a];copath-at(w;p)).  copathAgree(a.B[a];w;p;copath-extend(p;b))
BY
{ (Auto
   THEN Unhide
   THEN Auto
   THEN (D -2 THEN RepUR ``copathAgree copath-extend`` 0)
   THEN LessCases 0
   THEN Auto
   THEN Thin (-1)
   THEN RepUR ``copath-at`` -1) }

1
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))

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].
    \mforall{}p:copath(a.B[a];w).  \mforall{}b:coW-dom(a.B[a];copath-at(w;p)).
        copathAgree(a.B[a];w;p;copath-extend(p;b))


By

---

Latex:
(Auto
  THEN  Unhide
  THEN  Auto
  THEN  (D  -2  THEN  RepUR  ``copathAgree  copath-extend``  0)
  THEN  LessCases  0
  THEN  Auto
  THEN  Thin  (-1)
  THEN  RepUR  ``copath-at``  -1)

---

Home Index