Nuprl Lemma : csm-sigma_comp

[X,A,cA,cB,H,tau:Top].  ((sigma_comp(cA;cB))tau sigma_comp((cA)tau;(cB)tau+))


Proof




Definitions occuring in Statement :  sigma_comp: sigma_comp(cA;cB) csm-comp-structure: (cA)tau csm+: tau+ cube-context-adjoin: X.A csm-ap-type: (AF)s uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] csm-comp-structure: (cA)tau sigma_comp: sigma_comp(cA;cB) let: let csm+: tau+ csm-ap-type: (AF)s csm-comp: F csm-id-adjoin: [u] interval-1: 1(𝕀) csm-ap-term: (t)s compose: g csm-id: 1(X) csm-adjoin: (s;u) cc-snd: q cc-fst: p csm-ap: (s)x pi2: snd(t) pi1: fst(t) member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation sqequalRule because_Cache cut introduction extract_by_obid hypothesis

Latex:
\mforall{}[X,A,cA,cB,H,tau:Top].    ((sigma\_comp(cA;cB))tau  \msim{}  sigma\_comp((cA)tau;(cB)tau+))



Date html generated: 2018_05_23-AM-10_50_12
Last ObjectModification: 2018_05_20-PM-07_57_20

Theory : cubical!type!theory


Home Index