### Nuprl Lemma : comma-slice-cat_wf

`∀[A,C:SmallCategory]. ∀[S:Functor(A;C)]. ∀[x:cat-ob(C)].  ((S ↓ x) ∈ SmallCategory)`

Proof

Definitions occuring in Statement :  comma-slice-cat: `(S ↓ x)` cat-functor: `Functor(C1;C2)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` comma-slice-cat: `(S ↓ x)`
Lemmas referenced :  comma-cat_wf unit-cat_wf const-functor_wf cat-ob_wf cat-functor_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[A,C:SmallCategory].  \mforall{}[S:Functor(A;C)].  \mforall{}[x:cat-ob(C)].    ((S  \mdownarrow{}  x)  \mmember{}  SmallCategory)

Date html generated: 2020_05_20-AM-07_56_38
Last ObjectModification: 2017_01_13-PM-04_49_15

Theory : small!categories

Home Index