---

Step * 1 of Lemma W-subtype-coW


1. A : 𝕌'
2. B : A ⟶ Type
3. x : pco-W ⋅@i'
4. ∀path:Path. (StepAgree(path 0;⋅;x) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
⊢ x ∈ coW(A;a.B[a])
BY
{ (RepUR ``coW`` 0 THEN Trivial) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  x  :  pco-W  \mcdot{}@i'
4.  \mforall{}path:Path.  (StepAgree(path  0;\mcdot{};x)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))))
\mvdash{}  x  \mmember{}  coW(A;a.B[a])


By

---

Latex:
(RepUR  ``coW``  0  THEN  Trivial)

---

Home Index