Nuprl Lemma : csm-canonical-section-face
∀[X,I,rho,phi,s:Top]. ((canonical-section(X;𝔽;I;rho;phi))s ~ λJ,a. (phi)<(s)a>)
Proof
Definitions occuring in Statement :
face-type: 𝔽,
csm-ap-term: (t)s,
canonical-section: canonical-section(Gamma;A;I;rho;a),
fl-morph: <f>,
csm-ap: (s)x,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
lambda: λx.A[x],
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
canonical-section: canonical-section(Gamma;A;I;rho;a),
csm-ap-term: (t)s,
member: t ∈ T,
top: Top
Lemmas referenced :
face-type-ap-morph,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
because_Cache
Latex:
\mforall{}[X,I,rho,phi,s:Top]. ((canonical-section(X;\mBbbF{};I;rho;phi))s \msim{} \mlambda{}J,a. (phi)<(s)a>)
Date html generated:
2018_05_23-AM-09_24_15
Last ObjectModification:
2018_05_20-PM-06_23_01
Theory : cubical!type!theory
Home
Index