Nuprl Lemma : cat-comp_wf

`∀[C:SmallCategory]`
`  (cat-comp(C) ∈ x:cat-ob(C)`
`   ⟶ y:cat-ob(C)`
`   ⟶ z:cat-ob(C)`
`   ⟶ (cat-arrow(C) x y)`
`   ⟶ (cat-arrow(C) y z)`
`   ⟶ (cat-arrow(C) x z))`

Proof

Definitions occuring in Statement :  cat-comp: `cat-comp(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  pi2: `snd(t)` top: `Top` all: `∀x:A. B[x]` cat-comp: `cat-comp(C)` and: `P ∧ Q` spreadn: spread4 small-category: `SmallCategory` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  small-category_wf cat_arrow_triple_lemma cat_ob_pair_lemma
Rules used in proof :  hypothesisEquality hypothesis voidEquality voidElimination isect_memberEquality dependent_functionElimination extract_by_obid introduction sqequalRule productElimination rename thin setElimination sqequalHypSubstitution cut isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C:SmallCategory]
(cat-comp(C)  \mmember{}  x:cat-ob(C)
{}\mrightarrow{}  y:cat-ob(C)
{}\mrightarrow{}  z:cat-ob(C)
{}\mrightarrow{}  (cat-arrow(C)  x  y)
{}\mrightarrow{}  (cat-arrow(C)  y  z)
{}\mrightarrow{}  (cat-arrow(C)  x  z))

Date html generated: 2017_01_11-AM-09_17_41
Last ObjectModification: 2017_01_10-PM-06_15_40

Theory : small!categories

Home Index