### Nuprl Lemma : functor-uncurry_wf

`∀[A,B,C:SmallCategory].  (functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C)))`

Proof

Definitions occuring in Statement :  functor-uncurry: `functor-uncurry(C)` 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-uncurry: `functor-uncurry(C)` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` pi1: `fst(t)` subtype_rel: `A ⊆r B` cat-ob: `cat-ob(C)` functor-cat: `FUN(C1;C2)` cat-functor: `Functor(C1;C2)` pi2: `snd(t)` so_apply: `x[s]` so_lambda: so_lambda3 nat-trans: `nat-trans(C;D;F;G)` so_apply: `x[s1;s2;s3]` uimplies: `b supposing a` squash: `↓T` cat-arrow: `cat-arrow(C)` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` trans-comp: `t1 o t2` identity-trans: `identity-trans(C;D;F)` prop: `ℙ`
Lemmas referenced :  mk-functor_wf functor-cat_wf product-cat_wf functor_cat_ob_lemma ob_product_lemma functor-ob_wf subtype_rel_self cat-functor_wf cat-ob_wf arrow_prod_lemma cat-comp_wf functor-arrow_wf functor_cat_arrow_lemma cat-arrow_wf pi1_wf_top pi2_wf comp_product_cat_lemma functor-arrow-prod-comp equal_wf functor-arrow-comp cat-comp-assoc nat-trans-equation nat-trans_wf functor_cat_comp_lemma trans_comp_ap_lemma nat-trans-comp-equation nat-trans-assoc-comp-equation nat-trans-assoc-equation iff_weakening_equal id_prod_cat_lemma functor_cat_id_lemma ident_trans_ap_lemma functor-arrow-id cat-comp-ident2 cat-id_wf mk-nat-trans_wf ob_mk_functor_lemma arrow_mk_functor_lemma ap_mk_nat_trans_lemma cat-comp-ident1 small-category_wf squash_wf true_wf istype-universe trans-comp_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache dependent_functionElimination Error :memTop,  lambdaEquality_alt applyEquality productElimination productIsType universeIsType setElimination rename inhabitedIsType equalityTransitivity equalitySymmetry independent_pairEquality independent_isectElimination lambdaFormation_alt imageElimination natural_numberEquality imageMemberEquality baseClosed independent_functionElimination axiomEquality isect_memberEquality_alt isectIsTypeImplies applyLambdaEquality instantiate universeEquality functionExtensionality

Latex:
\mforall{}[A,B,C:SmallCategory].    (functor-uncurry(C)  \mmember{}  Functor(FUN(A;FUN(B;C));FUN(A  \mtimes{}  B;C)))

Date html generated: 2020_05_20-AM-07_54_41
Last ObjectModification: 2019_12_30-PM-07_28_13

Theory : small!categories

Home Index