### Nuprl Lemma : canonicalizable-function

`∀[T:Type]`
`  ∀[B:T ⟶ Type]. retractible(T) `` canonicalizable(x:T ⟶ B[x]) supposing ∀x:T. (B[x] ⊆r Base) `
`  supposing (T ⊆r Base) ∧ value-type(T)`

Proof

Definitions occuring in Statement :  retractible: `retractible(T)` canonicalizable: `canonicalizable(T)` value-type: `value-type(T)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` base: `Base` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` and: `P ∧ Q` subtype_rel: `A ⊆r B` value-type: `value-type(T)` has-value: `(a)↓` all: `∀x:A. B[x]` implies: `P `` Q` retractible: `retractible(T)` exists: `∃x:A. B[x]` canonicalizable: `canonicalizable(T)` prop: `ℙ` so_apply: `x[s]`
Lemmas referenced :  base_wf retractible_wf subtype_rel_wf value-type_wf equal-wf-base subtype_rel-equal has-value_wf_base is-exception_wf sqle_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality hypothesis Error :isect_memberEquality_alt,  isectElimination hypothesisEquality axiomSqleEquality Error :equalityIsType4,  Error :universeIsType,  because_Cache equalityTransitivity equalitySymmetry extract_by_obid rename Error :lambdaEquality_alt,  dependent_functionElimination Error :lambdaFormation_alt,  Error :dependent_pairFormation_alt,  independent_isectElimination Error :functionIsType,  applyEquality Error :inhabitedIsType,  Error :productIsType,  universeEquality pointwiseFunctionality baseApply closedConclusion baseClosed sqequalSqle divergentSqle callbyvalueCallbyvalue callbyvalueReduce independent_functionElimination functionExtensionality cumulativity Error :equalityIsType1,  sqleReflexivity hyp_replacement applyLambdaEquality callbyvalueExceptionCases exceptionSqequal Error :equalityIsType2

Latex:
\mforall{}[T:Type]
\mforall{}[B:T  {}\mrightarrow{}  Type].  retractible(T)  {}\mRightarrow{}  canonicalizable(x:T  {}\mrightarrow{}  B[x])  supposing  \mforall{}x:T.  (B[x]  \msubseteq{}r  Base)
supposing  (T  \msubseteq{}r  Base)  \mwedge{}  value-type(T)

Date html generated: 2019_06_20-AM-11_28_26
Last ObjectModification: 2018_09_28-PM-02_49_59

Theory : call!by!value_2

Home Index