Nuprl Lemma : functor_ob_pair_lemma
∀y,x:Top. (functor-ob(mk-functor(x;y)) ~ x)
Proof
Definitions occuring in Statement :
functor-ob: functor-ob(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],
pi1: fst(t),
functor-ob: functor-ob(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-ob(mk-functor(x;y)) \msim{} x)
Date html generated:
2017_01_11-AM-09_17_52
Last ObjectModification:
2017_01_10-PM-00_19_06
Theory : small!categories
Home
Index