### Nuprl Lemma : functor-is-isomorphism

`∀[A,B:SmallCategory].`
`  ∀f:Functor(A;B)`
`    (cat-isomorphism(Cat;A;B;f)`
`    `⇐⇒` Bij(cat-ob(A);cat-ob(B);ob(f)) ∧ (∀x,y:cat-ob(A).  Bij(cat-arrow(A) x y;cat-arrow(B) (f x) (f y);f x y)))`

Proof

Definitions occuring in Statement :  cat-cat: `Cat` functor-arrow: `arrow(F)` functor-ob: `ob(F)` cat-functor: `Functor(C1;C2)` cat-isomorphism: `cat-isomorphism(C;x;y;f)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` biject: `Bij(A;B;f)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` apply: `f a`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` cat-cat: `Cat` cat-isomorphism: `cat-isomorphism(C;x;y;f)` member: `t ∈ T` top: `Top` cat-inverse: `fg=1` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` exists: `∃x:A. B[x]` id_functor: `1` functor-comp: `functor-comp(F;G)` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` biject: `Bij(A;B;f)` inject: `Inj(A;B;f)` surject: `Surj(A;B;f)` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` cand: `A c∧ B` pi1: `fst(t)`
Lemmas referenced :  cat_arrow_triple_lemma cat_comp_tuple_lemma cat_id_tuple_lemma exists_wf cat-functor_wf equal-wf-T-base functor-comp_wf biject_wf cat-ob_wf functor-ob_wf all_wf cat-arrow_wf functor-arrow_wf small-category_wf ob_mk_functor_lemma equal_wf squash_wf true_wf iff_weakening_equal arrow_mk_functor_lemma subtype_rel-equal biject-inverse small-category-subtype subtype_rel_dep_function mk-functor_wf functor-arrow-comp cat-comp_wf functor-arrow-id cat-id_wf id_functor_wf equal-functors
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalRule cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis independent_pairFormation isectElimination hypothesisEquality lambdaEquality productEquality baseClosed because_Cache applyEquality productElimination applyLambdaEquality hyp_replacement equalitySymmetry imageElimination equalityTransitivity universeEquality natural_numberEquality imageMemberEquality independent_isectElimination independent_functionElimination dependent_pairFormation dependent_set_memberEquality setElimination rename instantiate functionExtensionality functionEquality cumulativity promote_hyp

Latex:
\mforall{}[A,B:SmallCategory].
\mforall{}f:Functor(A;B)
(cat-isomorphism(Cat;A;B;f)
\mLeftarrow{}{}\mRightarrow{}  Bij(cat-ob(A);cat-ob(B);ob(f))
\mwedge{}  (\mforall{}x,y:cat-ob(A).    Bij(cat-arrow(A)  x  y;cat-arrow(B)  (f  x)  (f  y);f  x  y)))

Date html generated: 2020_05_20-AM-07_53_56
Last ObjectModification: 2017_07_28-AM-09_19_47

Theory : small!categories

Home Index