### Nuprl Lemma : term-A-face_wf

`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[i:ℕ2].`
`  (term-A-face(a;I;alpha;i) ∈ A-face(X;A;[fresh-cname(I) / I];iota(fresh-cname(I))(alpha)))`

Proof

Definitions occuring in Statement :  term-A-face: `term-A-face(a;I;alpha;i)` A-face: `A-face(X;A;I;alpha)` cubical-term: `{X ⊢ _:AF}` cubical-type: `{X ⊢ _}` cube-set-restriction: `f(s)` I-cube: `X(I)` cubical-set: `CubicalSet` iota: `iota(x)` fresh-cname: `fresh-cname(I)` coordinate_name: `Cname` cons: `[a / b]` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` member: `t ∈ T` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` term-A-face: `term-A-face(a;I;alpha;i)` A-face: `A-face(X;A;I;alpha)` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` or: `P ∨ Q` prop: `ℙ` nameset: `nameset(L)` squash: `↓T` uimplies: `b supposing a` guard: `{T}` true: `True` iota': `iota'(I)`
Lemmas referenced :  cons_member fresh-cname_wf l_member_wf coordinate_name_wf cons_wf not_wf cubical-type-at_wf add-remove-fresh-sq equal_wf I-cube_wf cube-set-restriction-comp list-diff_wf cname_deq_wf nil_wf iota_wf face-map_wf2 subtype_rel-equal iff_weakening_equal cubical-term-at_wf cube-set-restriction_wf int_seg_wf list_wf cubical-term_wf cubical-type_wf cubical-set_wf face-map_wf iota'-identity squash_wf true_wf cube-set-restriction-id
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_pairEquality extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache dependent_functionElimination hypothesisEquality hypothesis applyEquality sqequalRule productElimination independent_functionElimination inlFormation dependent_set_memberEquality lambdaEquality setElimination rename setEquality imageElimination independent_isectElimination imageMemberEquality baseClosed equalityTransitivity equalitySymmetry natural_numberEquality hyp_replacement productEquality axiomEquality isect_memberEquality applyLambdaEquality universeEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[i:\mBbbN{}2].
(term-A-face(a;I;alpha;i)  \mmember{}  A-face(X;A;[fresh-cname(I)  /  I];iota(fresh-cname(I))(alpha)))

Date html generated: 2017_10_05-PM-04_05_01
Last ObjectModification: 2017_07_28-AM-11_28_57

Theory : cubical!sets

Home Index