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 ⊆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: supposing a squash: T prop: implies:  Q true: True guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q nat-trans: nat-trans(C;D;F;G) trans-comp: t1 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