Nuprl Lemma : discrete-fun-at-app
∀[f,a,alpha,I:Top]. (app(f; discr(a))(alpha) ~ discrete-fun(f)(alpha) a)
Proof
Definitions occuring in Statement :
discrete-fun: discrete-fun(f),
discrete-cubical-term: discr(t),
cubical-app: app(w; u),
cubical-term-at: u(a),
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
cubical-app: app(w; u),
discrete-cubical-term: discr(t),
cubical-term-at: u(a),
discrete-fun: discrete-fun(f)
Lemmas referenced :
top_wf
Rules used in proof :
because_Cache,
hypothesisEquality,
thin,
isectElimination,
isect_memberEquality,
sqequalHypSubstitution,
hypothesis,
extract_by_obid,
sqequalAxiom,
cut,
introduction,
isect_memberFormation,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
\mforall{}[f,a,alpha,I:Top]. (app(f; discr(a))(alpha) \msim{} discrete-fun(f)(alpha) a)
Date html generated:
2017_02_21-AM-10_43_16
Last ObjectModification:
2017_02_10-PM-11_26_41
Theory : cubical!type!theory
Home
Index