Nuprl Lemma : p-csm+-type

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


Proof




Definitions occuring in Statement :  csm+: tau+ cc-fst: p csm-ap-type: (AF)s uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  csm-ap-type: (AF)s pscm-ap-type: (AF)s csm-ap: (s)x pscm-ap: (s)x cc-fst: p psc-fst: p csm+: tau+ pscm+: tau+ csm-adjoin: (s;u) pscm-adjoin: (s;u) csm-comp: F pscm-comp: F cc-snd: q psc-snd: q
Lemmas referenced :  p-pscm+-type
Rules used in proof :  cut introduction extract_by_obid sqequalRule sqequalReflexivity sqequalSubstitution sqequalTransitivity computationStep hypothesis

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



Date html generated: 2018_05_23-AM-08_52_54
Last ObjectModification: 2018_05_20-PM-06_01_54

Theory : cubical!type!theory


Home Index