---

Step * 2 of Lemma coW-equiv-iff2


1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀p:copath(a.B[a];w')
     ∃q:copath(a.B[a];w). ((copath-length(q) = copath-length(p) ∈ ℤ) ∧ coW-equiv(a.B[a];copath-at(w';p);copath-at(w;q)))
⊢ coW-equiv(a.B[a];w;w')
BY
{ ((InstHyp [⌜()⌝] (-1)⋅ THENA Auto) THEN ExRepD) }

1
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀p:copath(a.B[a];w')
     ∃q:copath(a.B[a];w). ((copath-length(q) = copath-length(p) ∈ ℤ) ∧ coW-equiv(a.B[a];copath-at(w';p);copath-at(w;q)))
6. q : copath(a.B[a];w)
7. copath-length(q) = copath-length(()) ∈ ℤ
8. coW-equiv(a.B[a];copath-at(w';());copath-at(w;q))
⊢ coW-equiv(a.B[a];w;w')

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  w'  :  coW(A;a.B[a])
5.  \mforall{}p:copath(a.B[a];w')
          \mexists{}q:copath(a.B[a];w)
            ((copath-length(q)  =  copath-length(p))  \mwedge{}  coW-equiv(a.B[a];copath-at(w';p);copath-at(w;q)))
\mvdash{}  coW-equiv(a.B[a];w;w')


By

---

Latex:
((InstHyp  [\mkleeneopen{}()\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index