Nuprl Lemma : trivial-cube-set_wf

() ∈ CubicalSet


Proof




Definitions occuring in Statement :  trivial-cube-set: () cubical-set: CubicalSet member: t ∈ T
Definitions unfolded in proof :  trivial-cube-set: () member: t ∈ T cubical-set: CubicalSet uall: [x:A]. B[x] subtype_rel: A ⊆B top: Top and: P ∧ Q cand: c∧ B all: x:A. B[x] compose: g so_lambda: λ2x.t[x] so_apply: x[s] prop:
Lemmas referenced :  id-morph_wf equal-wf-T-base compose_wf name-comp_wf equal_wf all_wf equal-unit name-morph_wf top_wf it_wf coordinate_name_wf list_wf unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_set_memberEquality dependent_pairEquality lambdaEquality cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin applyEquality sqequalRule hypothesisEquality isect_memberEquality voidElimination voidEquality functionEquality lambdaFormation functionExtensionality because_Cache independent_pairFormation productElimination productEquality baseClosed

Latex:
()  \mmember{}  CubicalSet



Date html generated: 2016_06_16-PM-05_38_17
Last ObjectModification: 2016_01_18-PM-04_56_53

Theory : cubical!sets


Home Index