### Nuprl Lemma : functor-curry-iso

`∀A,B,C:SmallCategory.  cat-isomorphic(Cat;FUN(A × B;C);FUN(A;FUN(B;C)))`

Proof

Definitions occuring in Statement :  product-cat: `A × B` cat-cat: `Cat` functor-cat: `FUN(C1;C2)` cat-isomorphic: `cat-isomorphic(C;x;y)` small-category: `SmallCategory` all: `∀x:A. B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` top: `Top` subtype_rel: `A ⊆r B` uimplies: `b supposing a` functor-uncurry: `functor-uncurry(C)` functor-curry: `functor-curry(A;B)` functor-comp: `functor-comp(F;G)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` pi1: `fst(t)` pi2: `snd(t)` cat-isomorphic: `cat-isomorphic(C;x;y)` exists: `∃x:A. B[x]` guard: `{T}` cat-functor: `Functor(C1;C2)` cat-arrow: `cat-arrow(C)` cat-cat: `Cat` and: `P ∧ Q` prop: `ℙ` cat-isomorphism: `cat-isomorphism(C;x;y;f)` cand: `A c∧ B` cat-inverse: `fg=1` cat-ob: `cat-ob(C)` implies: `P `` Q` true: `True` squash: `↓T` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` nat-trans: `nat-trans(C;D;F;G)` id_functor: `1` label: `...\$L... t`
Lemmas referenced :  functor-uncurry_wf functor-curry_wf equal-functors product-cat_wf functor-ob_wf functor-cat_wf functor-comp_wf functor_cat_ob_lemma cat-ob_wf ob_product_lemma ob_mk_functor_lemma arrow_mk_functor_lemma arrow_prod_lemma ap_mk_nat_trans_lemma cat-arrow_wf cat-functor_wf subtype_rel_self all_wf equal_wf cat-id_wf cat-comp_wf cat_arrow_triple_lemma cat_comp_tuple_lemma cat_id_tuple_lemma cat-inverse_wf cat-cat_wf cat_ob_pair_lemma cat-isomorphism_wf small-category_wf functor-arrow_wf pi2_wf functor_cat_arrow_lemma squash_wf true_wf functor-arrow-prod-comp cat-comp-ident2 cat-comp-ident1 iff_weakening_equal functor-arrow-id nat-trans-equation functor_cat_id_lemma ident_trans_ap_lemma id_functor_wf nat-trans_wf nat-trans-equal2 member_wf subtype_rel-equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache hypothesis applyEquality sqequalRule dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaEquality independent_isectElimination productElimination independent_pairEquality dependent_pairFormation equalityTransitivity equalitySymmetry setEquality productEquality functionEquality functionExtensionality independent_pairFormation instantiate independent_functionElimination natural_numberEquality imageElimination universeEquality imageMemberEquality baseClosed setElimination rename hyp_replacement

Latex:
\mforall{}A,B,C:SmallCategory.    cat-isomorphic(Cat;FUN(A  \mtimes{}  B;C);FUN(A;FUN(B;C)))

Date html generated: 2017_10_05-AM-00_48_56
Last ObjectModification: 2017_07_28-AM-09_20_02

Theory : small!categories

Home Index