Nuprl Lemma : param-W-ext

[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
  pW ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))


Proof




Definitions occuring in Statement :  param-W: pW ext-family: F ≡ G uall: [x:A]. B[x] so_apply: x[s1;s2;s3] so_apply: x[s1;s2] so_apply: x[s] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ext-family: F ≡ G all: x:A. B[x] ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B 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] param-W: pW implies:  Q squash: T pcw-path: Path nat: le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A prop: exists: x:A. B[x] pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]) pcw-step-agree: StepAgree(s;p1;w) spreadn: spread3 bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a pi1: fst(t) bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b ge: i ≥  int_upper: {i...} decidable: Dec(P) iff: ⇐⇒ Q rev_implies:  Q sq_stable: SqStable(P) subtract: m top: Top true: True eq_int: (i =z j) cand: c∧ B pcw-steprel: StepRel(s1;s2) nequal: a ≠ b ∈  pcw-pp-barred: Barred(pp) pcw-partial: pcw-partial(path;n) isr: isr(x) pW-sup: pW-sup(a;f)
Lemmas referenced :  param-co-W_wf param-W_wf param-co-W-ext pcw-step-agree_wf istype-void le_wf pcw-path_wf squash_wf exists_wf nat_wf pcw-pp-barred_wf pcw-partial_wf eq_int_wf eqtt_to_assert assert_of_eq_int unit_wf2 eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int upper_subtype_nat nat_properties nequal-le-implies zero-add subtract_wf decidable__le istype-false not-le-2 sq_stable__le condition-implies-le minus-one-mul minus-one-mul-top istype-int minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le le-add-cancel pcw-steprel_wf add-zero le_antisymmetry_iff int_subtype_base general_arith_equation1 not-equal-2 less-iff-le assert_wf bnot_wf not_wf equal-wf-T-base bool_cases iff_transitivity iff_weakening_uiff assert_of_bnot decidable__lt not-lt-2 minus-zero le-add-cancel-alt pW-sup_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality Error :lambdaFormation_alt,  independent_pairFormation sqequalRule Error :lambdaEquality_alt,  Error :universeIsType,  applyEquality cumulativity functionExtensionality because_Cache Error :inhabitedIsType,  hypothesis Error :productIsType,  Error :functionIsType,  dependent_functionElimination productElimination independent_pairEquality axiomEquality Error :isect_memberEquality_alt,  universeEquality setElimination rename hypothesis_subsumption Error :dependent_pairEquality_alt,  Error :functionExtensionality_alt,  Error :dependent_set_memberEquality_alt,  imageElimination imageMemberEquality baseClosed natural_numberEquality Error :equalityIsType1,  equalityTransitivity equalitySymmetry independent_functionElimination unionElimination equalityElimination independent_isectElimination Error :inlEquality_alt,  Error :unionIsType,  Error :dependent_pairFormation_alt,  promote_hyp instantiate voidElimination addEquality minusEquality intEquality hyp_replacement applyLambdaEquality Error :equalityIsType4

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].
    pW  \mequiv{}  \mlambda{}p.(a:A[p]  \mtimes{}  (b:B[p;a]  {}\mrightarrow{}  (pW  C[p;a;b])))



Date html generated: 2019_06_20-PM-00_35_51
Last ObjectModification: 2018_10_02-AM-10_40_38

Theory : co-recursion


Home Index