Nuprl Lemma : functor-curry_wf
∀[A,B,C:SmallCategory].  (functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C))))
Proof
Definitions occuring in Statement : 
functor-curry: functor-curry(A;B)
, 
product-cat: A × B
, 
functor-cat: FUN(C1;C2)
, 
cat-functor: Functor(C1;C2)
, 
small-category: SmallCategory
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
functor-curry: functor-curry(A;B)
, 
so_lambda: λ2x.t[x]
, 
all: ∀x:A. B[x]
, 
top: Top
, 
so_apply: x[s]
, 
so_lambda: so_lambda(x,y,z.t[x; y; z])
, 
subtype_rel: A ⊆r B
, 
cat-arrow: cat-arrow(C)
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
product-cat: A × B
, 
cat-ob: cat-ob(C)
, 
so_apply: x[s1;s2;s3]
, 
uimplies: b supposing a
, 
squash: ↓T
, 
prop: ℙ
, 
implies: P 
⇒ Q
, 
true: True
, 
guard: {T}
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
rev_implies: P 
⇐ Q
, 
nat-trans: nat-trans(C;D;F;G)
, 
trans-comp: t1 o t2
, 
identity-trans: identity-trans(C;D;F)
Lemmas referenced : 
mk-functor_wf, 
functor-cat_wf, 
product-cat_wf, 
functor_cat_ob_lemma, 
istype-void, 
functor-ob_wf, 
ob_product_lemma, 
cat-ob_wf, 
functor-arrow_wf, 
cat-id_wf, 
subtype_rel_self, 
cat-arrow_wf, 
equal_wf, 
squash_wf, 
true_wf, 
istype-universe, 
cat-comp_wf, 
functor-arrow-prod-comp, 
iff_weakening_equal, 
cat-comp-ident1, 
functor-arrow-prod-id, 
functor_cat_arrow_lemma, 
mk-nat-trans_wf, 
ob_mk_functor_lemma, 
arrow_mk_functor_lemma, 
functor_cat_comp_lemma, 
functor_cat_id_lemma, 
trans_comp_ap_lemma, 
ident_trans_ap_lemma, 
small-category_wf, 
cat-comp-ident2, 
cat-functor_wf, 
ap_mk_nat_trans_lemma, 
nat-trans-equation, 
nat-trans-assoc-equation, 
cat-comp-assoc, 
nat-trans-comp-equation, 
nat-trans-assoc-comp-equation
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
introduction, 
cut, 
sqequalRule, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
hypothesis, 
because_Cache, 
lambdaEquality_alt, 
dependent_functionElimination, 
isect_memberEquality_alt, 
voidElimination, 
applyEquality, 
independent_pairEquality, 
universeIsType, 
independent_isectElimination, 
lambdaFormation_alt, 
imageElimination, 
equalityTransitivity, 
equalitySymmetry, 
inhabitedIsType, 
instantiate, 
universeEquality, 
productElimination, 
equalityIstype, 
independent_functionElimination, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
setElimination, 
rename, 
axiomEquality, 
isectIsTypeImplies, 
functionEquality, 
functionIsType
Latex:
\mforall{}[A,B,C:SmallCategory].    (functor-curry(A;B)  \mmember{}  Functor(FUN(A  \mtimes{}  B;C);FUN(A;FUN(B;C))))
Date html generated:
2019_10_31-AM-07_24_35
Last ObjectModification:
2018_12_13-PM-03_03_44
Theory : small!categories
Home
Index