Nuprl Lemma : csm-face-0

[s:Top]. ((0(𝔽))s 0(𝔽))


Proof




Definitions occuring in Statement :  face-0: 0(𝔽) csm-ap-term: (t)s uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  face-0: 0(𝔽) csm-ap-term: (t)s uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule isect_memberFormation introduction cut sqequalAxiom extract_by_obid hypothesis

Latex:
\mforall{}[s:Top].  ((0(\mBbbF{}))s  \msim{}  0(\mBbbF{}))



Date html generated: 2018_05_23-AM-09_19_55
Last ObjectModification: 2018_05_20-PM-06_18_06

Theory : cubical!type!theory


Home Index