Nuprl Lemma : csm-ap-csm-comp
∀Gamma,Delta,Z,s1,s2,I,alpha:Top. ((s2 o s1)alpha ~ (s2)(s1)alpha)
Proof
Definitions occuring in Statement :
csm-ap: (s)x,
csm-comp: G o F,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
csm-ap: (s)x,
csm-comp: G o F,
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 :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
hypothesis,
lemma_by_obid
Latex:
\mforall{}Gamma,Delta,Z,s1,s2,I,alpha:Top. ((s2 o s1)alpha \msim{} (s2)(s1)alpha)
Date html generated:
2016_06_16-PM-05_36_29
Last ObjectModification:
2015_12_28-PM-04_37_30
Theory : cubical!sets
Home
Index