Nuprl Lemma : cube+_interval-1
∀[I:fset(ℕ)]. ∀[i:ℕ]. (cube+(I;i) o [1(𝕀)] = <(i1)> ∈ formal-cube(I) j⟶ formal-cube(I+i))
Proof
Definitions occuring in Statement :
cube+: cube+(I;i),
interval-1: 1(𝕀),
interval-type: 𝕀,
csm-id-adjoin: [u],
cube-context-adjoin: X.A,
csm-comp: G o F,
context-map: <rho>,
cube_set_map: A ⟶ B,
formal-cube: formal-cube(I),
nc-1: (i1),
add-name: I+i,
fset: fset(T),
nat: ℕ,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
I_cube: A(I),
functor-ob: ob(F),
pi1: fst(t),
formal-cube: formal-cube(I),
names-hom: I ⟶ J,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
context-map: <rho>,
cube+: cube+(I;i),
interval-1: 1(𝕀),
csm-id-adjoin: [u],
csm-comp: G o F,
compose: f o g,
csm-adjoin: (s;u),
csm-id: 1(X),
csm-ap: (s)x,
nc-1: (i1),
names: names(I),
nat: ℕ,
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
and: P ∧ Q,
ifthenelse: if b then t else f fi ,
bfalse: ff,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
false: False
Lemmas referenced :
istype-nat,
fset_wf,
nat_wf,
csm-equal,
formal-cube_wf1,
add-name_wf,
csm-comp_wf,
cube-context-adjoin_wf,
interval-type_wf,
csm-id-adjoin_wf,
interval-1_wf,
cube+_wf,
context-map_wf,
nc-1_wf,
I_cube_wf,
I_cube_pair_redex_lemma,
arrow_pair_lemma,
names_wf,
nh-comp-sq,
eq_int_wf,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
dM1-sq-singleton-empty,
dM-lift-1,
subtype_rel_self,
names-hom_wf,
not-added-name,
dM-lift-inc
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
hypothesis,
extract_by_obid,
sqequalRule,
sqequalHypSubstitution,
isect_memberEquality_alt,
isectElimination,
thin,
hypothesisEquality,
axiomEquality,
isectIsTypeImplies,
inhabitedIsType,
universeIsType,
instantiate,
dependent_functionElimination,
because_Cache,
applyEquality,
independent_isectElimination,
functionExtensionality,
Error :memTop,
setElimination,
rename,
lambdaFormation_alt,
unionElimination,
equalityElimination,
equalityTransitivity,
equalitySymmetry,
productElimination,
dependent_pairFormation_alt,
equalityIstype,
promote_hyp,
cumulativity,
independent_functionElimination,
voidElimination
Latex:
\mforall{}[I:fset(\mBbbN{})]. \mforall{}[i:\mBbbN{}]. (cube+(I;i) o [1(\mBbbI{})] = <(i1)>)
Date html generated:
2020_05_20-PM-02_39_23
Last ObjectModification:
2020_04_04-PM-02_52_43
Theory : cubical!type!theory
Home
Index