---

Step * 2 1 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)))
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')
BY
{ (D -3
   THEN RepUR ``copath-length copath-nil`` -2
   THEN HypSubst' (-2) (-1)
   THEN RepUR ``copath-at`` -1
   THEN Unfold `coPath-at` -1
   THEN Reduce -1
   THEN EAuto 1) }

---

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)))
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))
\mvdash{}  coW-equiv(a.B[a];w;w')


By

---

Latex:
(D  -3
  THEN  RepUR  ``copath-length  copath-nil``  -2
  THEN  HypSubst'  (-2)  (-1)
  THEN  RepUR  ``copath-at``  -1
  THEN  Unfold  `coPath-at`  -1
  THEN  Reduce  -1
  THEN  EAuto  1)

---

Home Index