Nuprl Lemma : cubical-app_wf

[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠB}]. ∀[u:{X ⊢ _:A}].  (app(w; u) ∈ {X ⊢ _:(B)[u]})


Proof




Definitions occuring in Statement :  cubical-app: app(w; u) cubical-pi: ΠB csm-id-adjoin: [u] cube-context-adjoin: X.A cubical-term: {X ⊢ _:AF} csm-ap-type: (AF)s cubical-type: {X ⊢ _} cubical-set: CubicalSet uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cubical-term: {X ⊢ _:AF} all: x:A. B[x] implies:  Q cubical-type: {X ⊢ _} pi1: fst(t) cubical-app: app(w; u) cubical-type-at: A(a) csm-ap-type: (AF)s true: True subtype_rel: A ⊆B uimplies: supposing a squash: T prop: guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q cubical-pi: ΠB cubical-pi-family: cubical-pi-family(X;A;B;I;a) pi2: snd(t) cubical-type-ap-morph: (u f) top: Top cube-set-restriction: f(s) type-cat: TypeCat cat-id: cat-id(C) mk-nat-trans: |→ T[x] identity-trans: identity-trans(C;D;F) csm-id: 1(X) cc-adjoin-cube: (v;u) csm-adjoin: (s;u) csm-ap: (s)x csm-id-adjoin: [u] so_apply: x[s] so_lambda: λ2x.t[x] cand: c∧ B
Lemmas referenced :  csm-ap-type_wf cube-context-adjoin_wf csm-id-adjoin_wf list_wf coordinate_name_wf name-morph_wf I-cube_wf cube-set-restriction_wf cubical-term_wf cubical-pi_wf cubical-type_wf cubical-set_wf id-morph_wf csm-ap_wf subtype_rel-equal cubical-type-at_wf cube-set-restriction-id cc-adjoin-cube_wf equal_wf squash_wf true_wf istype-universe subtype_rel_self iff_weakening_equal csm-id-adjoin-ap subtype_rel_weakening ext-eq_weakening subtype_rel_wf cubical-pi-family_wf cc-adjoin-cube-restriction name-comp_wf subtype_rel_dep_function name-comp-id-left csm-ap-restriction ap_mk_nat_trans_lemma name-comp-id-right
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis inhabitedIsType lambdaFormation_alt setElimination rename productElimination sqequalRule functionIsType universeIsType because_Cache equalityIstype applyEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality_alt isectIsTypeImplies lambdaEquality_alt natural_numberEquality independent_isectElimination imageElimination imageMemberEquality baseClosed instantiate universeEquality lambdaFormation promote_hyp applyLambdaEquality functionEquality lambdaEquality voidEquality voidElimination isect_memberEquality comment productEquality independent_pairFormation dependent_set_memberEquality functionExtensionality hyp_replacement setEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:\mPi{}A  B\}].  \mforall{}[u:\{X  \mvdash{}  \_:A\}].
    (app(w;  u)  \mmember{}  \{X  \mvdash{}  \_:(B)[u]\})



Date html generated: 2020_05_21-AM-10_51_11
Last ObjectModification: 2020_01_01-PM-02_49_36

Theory : cubical!sets


Home Index