---

Step * 2 of Lemma param-W-ext

.....subterm..... T:t
1:n
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. p : P
7. x : a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b]))
⊢ x ∈ pW p
BY
{ (D (-1) THEN Fold `pW-sup` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  P  :  Type
2.  A  :  P  {}\mrightarrow{}  Type
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  pco-W  \mmember{}  P  {}\mrightarrow{}  Type
6.  p  :  P
7.  x  :  a:A[p]  \mtimes{}  (b:B[p;a]  {}\mrightarrow{}  (pW  C[p;a;b]))
\mvdash{}  x  \mmember{}  pW  p


By

---

Latex:
(D  (-1)  THEN  Fold  `pW-sup`  0  THEN  Auto)\mcdot{}

---

Home Index