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_lambda3,
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:
2020_05_20-AM-07_54_47
Last ObjectModification:
2017_07_28-AM-09_20_02
Theory : small!categories
Home
Index