Step
*
2
2
of Lemma
coW-corec
1. A : 𝕌'
2. B : A ⟶ Type
3. corec(T.a:A × (B[a] ⟶ T)) ∈ 𝕌'
4. x : corec(C.a:A × (B[a] ⟶ C))
5. ∀n:ℕ. (corec(C.a:A × (B[a] ⟶ C)) ⊆r (λC,p. (a:A × (b:B[a] ⟶ (C ⋅)))^n (λp.Top) ⋅))
⊢ x ∈ coW(A;a.B[a])
BY
{ RepUR ``coW param-co-W corec-family isect-family`` 0 }
1
1. A : 𝕌'
2. B : A ⟶ Type
3. corec(T.a:A × (B[a] ⟶ T)) ∈ 𝕌'
4. x : corec(C.a:A × (B[a] ⟶ C))
5. ∀n:ℕ. (corec(C.a:A × (B[a] ⟶ C)) ⊆r (λC,p. (a:A × (b:B[a] ⟶ (C ⋅)))^n (λp.Top) ⋅))
⊢ x ∈ ⋂n:ℕ. (λW,p. (a:A × (b:B[a] ⟶ (W ⋅)))^n (λp.Top) ⋅)
Latex:
Latex:
1. A : \mBbbU{}'
2. B : A {}\mrightarrow{} Type
3. corec(T.a:A \mtimes{} (B[a] {}\mrightarrow{} T)) \mmember{} \mBbbU{}'
4. x : corec(C.a:A \mtimes{} (B[a] {}\mrightarrow{} C))
5. \mforall{}n:\mBbbN{}. (corec(C.a:A \mtimes{} (B[a] {}\mrightarrow{} C)) \msubseteq{}r (\mlambda{}C,p. (a:A \mtimes{} (b:B[a] {}\mrightarrow{} (C \mcdot{})))\^{}n (\mlambda{}p.Top) \mcdot{}))
\mvdash{} x \mmember{} coW(A;a.B[a])
By
Latex:
RepUR ``coW param-co-W corec-family isect-family`` 0
Home
Index