---

Step * 1 of Lemma coW-wfdd_functionality

.....assertion..... 
1. [A] : 𝕌'
2. B : A ⟶ Type
⊢ ∀w,w':coW(A;a.B[a]).  (coW-equiv(a.B[a];w;w') ⇒ coW-wfdd(a.B[a];w) ⇒ coW-wfdd(a.B[a];w'))
BY
{ (Auto THEN ParallelLast THEN 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:{p:n:ℕ ⟶ copath(a.B[a];w)| 
       ∀i:ℕ
         ((copath-length(p i) = i ∈ ℤ)
         ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ)
         ⇒ copathAgree(a.B[a];w;p i;p (i + 1)))} 
     (↓∃i:ℕ. (¬(copath-length(p i) = i ∈ ℤ)))
7. p : {p:n:ℕ ⟶ copath(a.B[a];w')| 
        ∀i:ℕ
          ((copath-length(p i) = i ∈ ℤ)
          ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ)
          ⇒ copathAgree(a.B[a];w';p i;p (i + 1)))} 
⊢ ↓∃i:ℕ. (¬(copath-length(p i) = i ∈ ℤ))

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
\mvdash{}  \mforall{}w,w':coW(A;a.B[a]).    (coW-equiv(a.B[a];w;w')  {}\mRightarrow{}  coW-wfdd(a.B[a];w)  {}\mRightarrow{}  coW-wfdd(a.B[a];w'))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  Auto)

---

Home Index