Nuprl Lemma : csm-sigma_comp3

[H,A',X,cA,cB,A,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-comp: F csm-id-adjoin: [u] csm-ap-type: (AF)s 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{}[H,A',X,cA,cB,A,tau:Top].    ((sigma\_comp(cA;cB))tau  \msim{}  sigma\_comp((cA)tau;(cB)tau+))



Date html generated: 2017_01_10-AM-09_54_17
Last ObjectModification: 2016_12_24-PM-00_40_36

Theory : cubical!type!theory


Home Index