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