---

Step * of Lemma coW-equiv-iff2

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
    (coW-equiv(a.B[a];w;w')
    ⇐⇒ ∀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))))
BY
{ Auto }

1
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. coW-equiv(a.B[a];w;w')
6. 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)))

2
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')

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}']
    \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w,w':coW(A;a.B[a]).
        (coW-equiv(a.B[a];w;w')
        \mLeftarrow{}{}\mRightarrow{}  \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))))


By

---

Latex:
Auto

---

Home Index