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-comp: G o F,
csm-ap: (s)x,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
csm-ap: (s)x,
pscm-ap: (s)x,
csm-comp: G o F,
pscm-comp: G o F
Lemmas referenced :
pscm-ap-pscm-comp
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalRule,
sqequalReflexivity,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
hypothesis
Latex:
\mforall{}Gamma,Delta,Z,s1,s2,I,alpha:Top. ((s2 o s1)alpha \msim{} (s2)(s1)alpha)
Date html generated:
2018_05_23-AM-08_36_31
Last ObjectModification:
2018_05_20-PM-05_49_13
Theory : cubical!type!theory
Home
Index