Nuprl Lemma : W-ext

[A:Type]. ∀[B:A ⟶ Type].  W(A;a.B[a]) ≡ a:A × (B[a] ⟶ W(A;a.B[a]))


Proof




Definitions occuring in Statement :  W: W(A;a.B[a]) ext-eq: A ≡ B uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] ext-family: F ≡ G all: x:A. B[x] W: W(A;a.B[a]) ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B
Lemmas referenced :  param-W-ext unit_wf2 it_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis sqequalRule lambdaEquality hypothesisEquality applyEquality dependent_functionElimination productElimination independent_pairEquality axiomEquality functionEquality cumulativity universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    W(A;a.B[a])  \mequiv{}  a:A  \mtimes{}  (B[a]  {}\mrightarrow{}  W(A;a.B[a]))



Date html generated: 2018_05_21-PM-00_05_34
Last ObjectModification: 2018_05_14-AM-10_38_01

Theory : co-recursion


Home Index