---

Step * of Lemma W-type-ext

∀[A:Type]. ∀[B:A ⟶ Type]. W-type(A; a.B[a]) ≡ a:A × (B[a] ⟶ W-type(A; a.B[a])) supposing ∀x,y:A.  Dec(x = y ∈ A)
BY
{ (Auto
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN Try (((D (-1) THEN Fold `W-sup` 0) THEN Auto))
   THEN D (-1)
   THEN co_WD (-2)
   THEN D -2
   THEN Auto
   THEN (ExtWith [`b'] [⌜B[a] ⟶ co-W(A;a.B[a])⌝]⋅ THENA Auto)
   THEN MemTypeCD⋅
   THEN Auto
   THEN (TACTIC:(FLemma `deq-exists` [2] THENM RenameVar `eq' (-1)) THENA Auto)) }

1
1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. B : A ⟶ Type
4. a : A
5. x1 : B[a] ⟶ co-W(A;a.B[a])
6. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(<a, x1>;p)
7. b : B[a]
8. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
9. eq : EqDecider(A)
⊢ W-bars(x1 b;p)

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}[B:A  {}\mrightarrow{}  Type].  W-type(A;  a.B[a])  \mequiv{}  a:A  \mtimes{}  (B[a]  {}\mrightarrow{}  W-type(A;  a.B[a])) 
    supposing  \mforall{}x,y:A.    Dec(x  =  y)


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  Try  (((D  (-1)  THEN  Fold  `W-sup`  0)  THEN  Auto))
  THEN  D  (-1)
  THEN  co\_WD  (-2)
  THEN  D  -2
  THEN  Auto
  THEN  (ExtWith  [`b']  [\mkleeneopen{}B[a]  {}\mrightarrow{}  co-W(A;a.B[a])\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MemTypeCD\mcdot{}
  THEN  Auto
  THEN  (TACTIC:(FLemma  `deq-exists`  [2]  THENM  RenameVar  `eq'  (-1))  THENA  Auto))

---

Home Index