Nuprl Lemma : pscm-ap-pscm-comp
∀Gamma,Delta,Z,s1,s2,I,alpha:Top. ((s2 o s1)alpha ~ (s2)(s1)alpha)
Proof
Definitions occuring in Statement :
pscm-comp: G o F,
pscm-ap: (s)x,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
pscm-ap: (s)x,
pscm-comp: G o F,
compose: f o g,
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
hypothesis,
introduction,
extract_by_obid
Latex:
\mforall{}Gamma,Delta,Z,s1,s2,I,alpha:Top. ((s2 o s1)alpha \msim{} (s2)(s1)alpha)
Date html generated:
2018_05_22-PM-10_00_34
Last ObjectModification:
2018_05_20-PM-09_43_57
Theory : presheaf!models!of!type!theory
Home
Index