Nuprl Lemma : sets-arrow
∀[C:SmallCategory]. ∀[X:Top].
  (cat-arrow(sets(C; X)) ~ λAa,Bb. let A,a = Aa in let B,b = Bb in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} )
Proof
Definitions occuring in Statement : 
sets: sets(C; X)
, 
psc-restriction: f(s)
, 
functor-ob: ob(F)
, 
cat-arrow: cat-arrow(C)
, 
small-category: SmallCategory
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
lambda: λx.A[x]
, 
spread: spread def, 
sqequal: s ~ t
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
small-category: SmallCategory
, 
spreadn: spread4, 
psc-restriction: f(s)
, 
sets: sets(C; X)
, 
all: ∀x:A. B[x]
, 
top: Top
, 
presheaf-elements: el(P)
, 
mk-cat: mk-cat, 
and: P ∧ Q
, 
functor-arrow: arrow(F)
, 
pi2: snd(t)
Lemmas referenced : 
cat_arrow_triple_lemma, 
op-cat-arrow, 
top_wf, 
small-category_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
hypothesisEquality, 
sqequalHypSubstitution, 
setElimination, 
thin, 
rename, 
productElimination, 
sqequalRule, 
extract_by_obid, 
dependent_functionElimination, 
isect_memberEquality, 
voidElimination, 
voidEquality, 
hypothesis, 
equalityTransitivity, 
equalitySymmetry, 
isectElimination, 
sqequalAxiom, 
because_Cache
Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:Top].
    (cat-arrow(sets(C;  X))  \msim{}  \mlambda{}Aa,Bb.  let  A,a  =  Aa  in  let  B,b  =  Bb  in  \{f:cat-arrow(C)  A  B|  f(b)  =  a\}  )
Date html generated:
2018_05_22-PM-09_59_17
Last ObjectModification:
2018_05_20-PM-09_42_07
Theory : presheaf!models!of!type!theory
Home
Index