Nuprl Lemma : cubes-arrow
∀[X:Top]. (cat-arrow(cubes(X)) ~ λAa,Bb. let A,a = Aa in let B,b = Bb in {f:A ⟶ B| f(b) = a ∈ (X A)} )
Proof
Definitions occuring in Statement :
cubes: cubes(X),
cube-set-restriction: f(s),
names-hom: I ⟶ J,
functor-ob: ob(F),
cat-arrow: cat-arrow(C),
uall: ∀[x:A]. B[x],
top: Top,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
spread: spread def,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cubes: cubes(X),
cube-cat: CubeCat,
all: ∀x:A. B[x],
top: Top,
cube-set-restriction: f(s),
psc-restriction: f(s)
Lemmas referenced :
sets-arrow,
cube-cat_wf,
cat_arrow_triple_lemma
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
sqequalRule,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}[X:Top]. (cat-arrow(cubes(X)) \msim{} \mlambda{}Aa,Bb. let A,a = Aa in let B,b = Bb in \{f:A {}\mrightarrow{} B| f(b) = a\} )
Date html generated:
2018_05_23-AM-08_33_24
Last ObjectModification:
2018_05_20-PM-05_46_27
Theory : cubical!type!theory
Home
Index