Nuprl Lemma : csm-ap-context-map
∀[I,J,a,rho,G:Top].  ((<rho>)a ~ a(rho))
Proof
Definitions occuring in Statement : 
csm-ap: (s)x
, 
context-map: <rho>
, 
cube-set-restriction: f(s)
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
sqequal: s ~ t
Definitions unfolded in proof : 
csm-ap: (s)x
, 
pscm-ap: (s)x
, 
context-map: <rho>
, 
ps-context-map: <rho>
, 
cube-set-restriction: f(s)
, 
psc-restriction: f(s)
Lemmas referenced : 
pscm-ap-context-map
Rules used in proof : 
cut, 
introduction, 
extract_by_obid, 
sqequalRule, 
sqequalReflexivity, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
hypothesis
Latex:
\mforall{}[I,J,a,rho,G:Top].    ((<rho>)a  \msim{}  a(rho))
Date html generated:
2018_05_23-AM-08_35_25
Last ObjectModification:
2018_05_20-PM-05_48_37
Theory : cubical!type!theory
Home
Index