Nuprl Lemma : wfterm-accum_wf_ctt1
∀[m:X:?CubicalContext
⟶ vs:(varname() List)
⟶ f:CttOp
⟶ L:{L:CttMeaningTriple List|
vdf-eq(?CubicalContext;ctt-binder-context X vs f;L)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);mkterm(f;map(λx.(fst(snd(x)));L))))}
⟶ [[X;mkterm(f;map(λx.(fst(snd(x)));L))]]]. ∀[varcase:X:?CubicalContext
⟶ vs:(varname() List)
⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}
⟶ [[X;varterm(v)]]]. ∀[X:?CubicalContext]. ∀[t:CttTerm].
(wfterm-accum(X;t)
p,vs,v.varcase[p;vs;v]
prm,vs,f,L.m[prm;vs;f;L]
p0,ws,op,sofar,bt.ctt-binder-context[p0;ws;op;sofar;bt] ∈ [[X;t]])
Proof
Definitions occuring in Statement :
ctt-binder-context: ctt-binder-context,
ctt-meaning-triple: CttMeaningTriple,
ctt_meaning: [[ctxt;t]],
ctt-term: CttTerm,
ctt-arity: ctt-arity(x),
ctt-kind: ctt-kind(t),
ctt-op: CttOp,
cubical-context: ?CubicalContext,
wfterm-accum: wfterm-accum,
wf-term: wf-term(arity;sort;t),
mkterm: mkterm(opr;bts),
varterm: varterm(v),
nullvar: nullvar(),
varname: varname(),
vdf-eq: vdf-eq(A;f;L),
map: map(f;as),
list: T List,
assert: ↑b,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3;s4;s5],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
pi1: fst(t),
pi2: snd(t),
not: ¬A,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x y.t[x; y],
ctt-term: CttTerm,
so_apply: x[s1;s2],
ctt-meaning-triple: CttMeaningTriple
Lemmas referenced :
wfterm-accum_wf,
ctt-op_wf,
ctt-kind_wf,
term_wf,
ctt-arity_wf,
cubical-context_wf,
ctt_meaning_wf,
wfterm_wf,
ctt-binder-context_wf
Rules used in proof :
cut,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
cumulativity,
hypothesis,
lambdaEquality_alt,
hypothesisEquality,
universeIsType,
sqequalRule
Latex:
\mforall{}[m:X:?CubicalContext
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} f:CttOp
{}\mrightarrow{} L:\{L:CttMeaningTriple List|
vdf-eq(?CubicalContext;ctt-binder-context X vs f;L)
\mwedge{} (\muparrow{}wf-term(\mlambda{}f.ctt-arity(f);\mlambda{}t.ctt-kind(t);mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))))\}
{}\mrightarrow{} [[X;mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))]]]. \mforall{}[varcase:X:?CubicalContext
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} v:\{v:varname()| \mneg{}(v = nullvar())\}
{}\mrightarrow{} [[X;varterm(v)]]].
\mforall{}[X:?CubicalContext]. \mforall{}[t:CttTerm].
(wfterm-accum(X;t)
p,vs,v.varcase[p;vs;v]
prm,vs,f,L.m[prm;vs;f;L]
p0,ws,op,sofar,bt.ctt-binder-context[p0;ws;op;sofar;bt] \mmember{} [[X;t]])
Date html generated:
2020_05_21-AM-10_38_41
Last ObjectModification:
2020_03_18-PM-03_37_53
Theory : cubical!type!theory
Home
Index