---

Step * 1 1 1 1 of Lemma W-sup_wf


1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W-type(A; a.B[a])
5. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
6. W-sup(a;f) ∈ co-W(A;a.B[a])
7. n : ℕ
8. n + 1 ≠ 0
9. x : B[a]@i
10. (p 0 a) = (inl x) ∈ (B[a]?)
11. True
12. ↑isr(W-select(f x;map(λn.(p (n + 1));upto(n))))
⊢ ↑isr(W-select(f x;map(p;map(λi.(i + 1);upto((n + 1) - 1)))))
BY
{ ((RWO "map-map" 0 THENA Auto) THEN RepUR ``compose`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  a  :  A
4.  f  :  B[a]  {}\mrightarrow{}  W-type(A;  a.B[a])
5.  p  :  \mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?)@i
6.  W-sup(a;f)  \mmember{}  co-W(A;a.B[a])
7.  n  :  \mBbbN{}
8.  n  +  1  \mneq{}  0
9.  x  :  B[a]@i
10.  (p  0  a)  =  (inl  x)
11.  True
12.  \muparrow{}isr(W-select(f  x;map(\mlambda{}n.(p  (n  +  1));upto(n))))
\mvdash{}  \muparrow{}isr(W-select(f  x;map(p;map(\mlambda{}i.(i  +  1);upto((n  +  1)  -  1)))))


By

---

Latex:
((RWO  "map-map"  0  THENA  Auto)  THEN  RepUR  ``compose``  0  THEN  Auto)\mcdot{}

---

Home Index