Nuprl Definition : small-category
SmallCategory ==
{cat:ob:Type
× arrow:ob ⟶ ob ⟶ Type
× x:ob ⟶ (arrow x x)
× (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))|
let ob,arrow,id,comp = cat
in (∀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))))
∧ (∀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))) }
Definitions occuring in Statement :
spreadn: spread4,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
universe: Type,
product: x:A × B[x],
function: x:A ⟶ B[x],
spreadn: spread4,
and: P ∧ Q,
all: ∀x:A. B[x],
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
s-cat
Latex:
SmallCategory ==
\{cat:ob:Type
\mtimes{} arrow:ob {}\mrightarrow{} ob {}\mrightarrow{} Type
\mtimes{} x:ob {}\mrightarrow{} (arrow x x)
\mtimes{} (x:ob {}\mrightarrow{} y:ob {}\mrightarrow{} z:ob {}\mrightarrow{} (arrow x y) {}\mrightarrow{} (arrow y z) {}\mrightarrow{} (arrow x z))|
let ob,arrow,id,comp = cat
in (\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)))
\mwedge{} (\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)))) \}
Date html generated:
2016_05_18-AM-11_51_53
Last ObjectModification:
2015_09_23-AM-09_29_03
Theory : small!categories
Home
Index