Nuprl Lemma : csm+-p-type

[C,H,K,A,B,tau:Top].  (((A)p)(tau+ p;q) ((A)tau+)p)


Proof




Definitions occuring in Statement :  csm+: tau+ csm-adjoin: (s;u) cc-snd: q cc-fst: p cube-context-adjoin: X.A csm-ap-type: (AF)s csm-comp: F uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  csm-ap-type: (AF)s uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) member: t ∈ T so_apply: x[s1;s2;s3;s4] so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] uimplies: supposing a csm-ap: (s)x cc-fst: p pi1: fst(t) csm-adjoin: (s;u) csm-comp: F compose: g csm+: tau+ cc-snd: q pi2: snd(t)
Lemmas referenced :  lifting-strict-spread strict4-spread top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination hypothesis because_Cache isect_memberFormation sqequalAxiom hypothesisEquality

Latex:
\mforall{}[C,H,K,A,B,tau:Top].    (((A)p)(tau+  o  p;q)  \msim{}  ((A)tau+)p)



Date html generated: 2017_01_09-AM-09_14_50
Last ObjectModification: 2016_12_15-PM-03_07_14

Theory : cubical!type!theory


Home Index