### Nuprl Lemma : unit-functor-is-const

`∀[A:SmallCategory]. ∀f:Functor(1;A). ∃a:cat-ob(A). (f = const-functor(A;a) ∈ Functor(1;A))`

Proof

Definitions occuring in Statement :  const-functor: `const-functor(A;a)` cat-functor: `Functor(C1;C2)` unit-cat: `1` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` unit: `Unit` cat-ob: `cat-ob(C)` pi1: `fst(t)` unit-cat: `1` discrete-cat: `discrete-cat(X)` mk-cat: mk-cat prop: `ℙ` uimplies: `b supposing a` cat-functor: `Functor(C1;C2)` and: `P ∧ Q` top: `Top` const-functor: `const-functor(A;a)` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` it: `⋅` squash: `↓T` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  functor-ob_wf unit-cat_wf it_wf subtype_rel_self equal-wf-base equal-functors const-functor_wf cat_ob_pair_lemma cat_arrow_triple_lemma cat_comp_tuple_lemma cat_id_tuple_lemma ob_pair_lemma ob_mk_functor_lemma cat-ob_wf arrow_pair_lemma arrow_mk_functor_lemma cat-arrow_wf equal_wf cat-functor_wf small-category_wf equal-unit squash_wf true_wf unit_wf2 cat-id_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation dependent_pairFormation applyEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality sqequalRule intEquality baseClosed because_Cache independent_isectElimination setElimination rename productElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality equalityElimination lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality functionExtensionality natural_numberEquality imageMemberEquality independent_functionElimination

Latex:
\mforall{}[A:SmallCategory].  \mforall{}f:Functor(1;A).  \mexists{}a:cat-ob(A).  (f  =  const-functor(A;a))

Date html generated: 2020_05_20-AM-07_53_41
Last ObjectModification: 2017_07_28-AM-09_19_43

Theory : small!categories

Home Index