### Nuprl Lemma : mk-cat_wf

`∀[ob:Type]. ∀[arrow:ob ⟶ ob ⟶ Type]. ∀[id:x:ob ⟶ arrow[x;x]]. ∀[comp:x:ob`
`                                                                        ⟶ y:ob`
`                                                                        ⟶ z:ob`
`                                                                        ⟶ arrow[x;y]`
`                                                                        ⟶ arrow[y;z]`
`                                                                        ⟶ arrow[x;z]].`
`  (Cat(ob = ob;`
`       arrow(x,y) = arrow[x;y];`
`       id(a) = id[a];`
`       comp(u,v,w,f,g) = comp[u;v;w;f;g]) ∈ SmallCategory) supposing `
`     ((∀x,y,z,w:ob. ∀f:arrow[x;y]. ∀g:arrow[y;z]. ∀h:arrow[z;w].`
`         (comp[x;z;w;comp[x;y;z;f;g];h] = comp[x;y;w;f;comp[y;z;w;g;h]] ∈ arrow[x;w])) and `
`     (∀x,y:ob. ∀f:arrow[x;y].  ((comp[x;x;y;id[x];f] = f ∈ arrow[x;y]) ∧ (comp[x;y;y;f;id[y]] = f ∈ arrow[x;y]))))`

Proof

Definitions occuring in Statement :  mk-cat: mk-cat small-category: `SmallCategory` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2;s3;s4;s5]` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` small-category: `SmallCategory` mk-cat: mk-cat so_apply: `x[s1;s2;s3;s4;s5]` so_apply: `x[s]` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` spreadn: spread4 and: `P ∧ Q` so_lambda: `λ2x.t[x]` prop: `ℙ` all: `∀x:A. B[x]`
Lemmas referenced :  all_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality sqequalRule dependent_pairEquality because_Cache lambdaEquality applyEquality functionExtensionality hypothesisEquality independent_pairEquality hypothesis sqequalHypSubstitution productEquality functionEquality thin cumulativity universeEquality independent_pairFormation productElimination extract_by_obid isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[ob:Type].  \mforall{}[arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  Type].  \mforall{}[id:x:ob  {}\mrightarrow{}  arrow[x;x]].  \mforall{}[comp:x:ob
{}\mrightarrow{}  y:ob
{}\mrightarrow{}  z:ob
{}\mrightarrow{}  arrow[x;y]
{}\mrightarrow{}  arrow[y;z]
{}\mrightarrow{}  arrow[x;z]].
(Cat(ob  =  ob;
arrow(x,y)  =  arrow[x;y];
id(a)  =  id[a];
comp(u,v,w,f,g)  =  comp[u;v;w;f;g])  \mmember{}  SmallCategory)  supposing
((\mforall{}x,y,z,w:ob.  \mforall{}f:arrow[x;y].  \mforall{}g:arrow[y;z].  \mforall{}h:arrow[z;w].
(comp[x;z;w;comp[x;y;z;f;g];h]  =  comp[x;y;w;f;comp[y;z;w;g;h]]))  and
(\mforall{}x,y:ob.  \mforall{}f:arrow[x;y].    ((comp[x;x;y;id[x];f]  =  f)  \mwedge{}  (comp[x;y;y;f;id[y]]  =  f))))

Date html generated: 2017_10_05-AM-00_45_34
Last ObjectModification: 2017_07_28-AM-09_18_56

Theory : small!categories

Home Index