Nuprl Lemma : all-value-type

[A:Type]. ∀[a:A]. ∀[B:A ⟶ Type].  value-type(∀a:A. B[a]) supposing value-type(B[a])


Proof




Definitions occuring in Statement :  value-type: value-type(T) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] exists: x:A. B[x] squash: T all: x:A. B[x] value-type: value-type(T) has-value: (a)↓
Lemmas referenced :  function-value-type value-type_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :lambdaEquality_alt,  applyEquality Error :inhabitedIsType,  independent_isectElimination Error :dependent_pairFormation_alt,  hypothesis Error :universeIsType,  imageMemberEquality baseClosed Error :isect_memberEquality_alt,  axiomSqleEquality Error :isectIsTypeImplies,  Error :functionIsType,  instantiate universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[a:A].  \mforall{}[B:A  {}\mrightarrow{}  Type].    value-type(\mforall{}a:A.  B[a])  supposing  value-type(B[a])



Date html generated: 2019_06_20-AM-11_21_30
Last ObjectModification: 2019_01_28-PM-03_33_44

Theory : call!by!value_1


Home Index