Nuprl Lemma : csm-ap-comp-type-sq
∀[Gamma:CubicalSet]. ∀[Delta,Z,s1,s2:Top]. ∀A:{Gamma ⊢ _}. ((A)s2 o s1 ~ ((A)s2)s1)
Proof
Definitions occuring in Statement :
csm-ap-type: (AF)s,
cubical-type: {X ⊢ _},
csm-comp: G o F,
cubical-set: CubicalSet,
uall: ∀[x:A]. B[x],
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
cubical-type: {X ⊢ _},
csm-ap-type: (AF)s,
csm-comp: G o F,
csm-ap: (s)x,
type-cat: TypeCat,
trans-comp: trans-comp(C;D;F;G;H;t1;t2),
cat-comp: cat-comp(C),
pi2: snd(t),
compose: f o g,
member: t ∈ T
Lemmas referenced :
cubical-set_wf,
top_wf,
cubical-type_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
setElimination,
thin,
rename,
cut,
productElimination,
sqequalRule,
hypothesis,
lemma_by_obid,
isectElimination,
hypothesisEquality,
because_Cache
Latex:
\mforall{}[Gamma:CubicalSet]. \mforall{}[Delta,Z,s1,s2:Top]. \mforall{}A:\{Gamma \mvdash{} \_\}. ((A)s2 o s1 \msim{} ((A)s2)s1)
Date html generated:
2016_06_16-PM-05_39_47
Last ObjectModification:
2016_03_28-PM-09_46_48
Theory : cubical!sets
Home
Index