Nuprl Lemma : canonical-section-at
∀[Gamma,A,I,rho,a,J,x:Top]. (canonical-section(Gamma;A;I;rho;a)(x) ~ (a rho x))
Proof
Definitions occuring in Statement :
canonical-section: canonical-section(Gamma;A;I;rho;a),
cubical-term-at: u(a),
cubical-type-ap-morph: (u a f),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
cubical-term-at: u(a),
presheaf-term-at: u(a),
canonical-section: canonical-section(Gamma;A;I;rho;a),
ps-canonical-section: ps-canonical-section(Gamma;A;I;rho;a),
cubical-type-ap-morph: (u a f),
presheaf-type-ap-morph: (u a f)
Lemmas referenced :
ps-canonical-section-at
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalRule,
sqequalReflexivity,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
hypothesis
Latex:
\mforall{}[Gamma,A,I,rho,a,J,x:Top]. (canonical-section(Gamma;A;I;rho;a)(x) \msim{} (a rho x))
Date html generated:
2018_05_23-AM-08_46_14
Last ObjectModification:
2018_05_20-PM-05_56_10
Theory : cubical!type!theory
Home
Index