### 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