Nuprl Lemma : functor_arrow_pair_lemma
∀y,x:Top. (functor-arrow(mk-functor(x;y)) ~ y)
Proof
Definitions occuring in Statement :
functor-arrow: functor-arrow(F),
mk-functor: mk-functor(ob;arrow),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
all: ∀x:A. B[x],
pi2: snd(t),
functor-arrow: functor-arrow(F),
mk-functor: mk-functor(ob;arrow)
Lemmas referenced :
top_wf
Rules used in proof :
hypothesis,
extract_by_obid,
introduction,
cut,
lambdaFormation,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
\mforall{}y,x:Top. (functor-arrow(mk-functor(x;y)) \msim{} y)
Date html generated:
2017_01_11-AM-09_17_54
Last ObjectModification:
2017_01_10-PM-00_19_51
Theory : small!categories
Home
Index