Nuprl Definition : small-category

SmallCategory ==
  {cat:ob:Type
   × arrow:ob ⟶ ob ⟶ Type
   × x:ob ⟶ (arrow x)
   × (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow y) ⟶ (arrow z) ⟶ (arrow z))| 
   let ob,arrow,id,comp cat 
   in (∀x,y:ob. ∀f:arrow y.  (((comp (id x) f) f ∈ (arrow y)) ∧ ((comp (id y)) f ∈ (arrow y))))
      ∧ (∀x,y,z,w:ob. ∀f:arrow y. ∀g:arrow z. ∀h:arrow w.
           ((comp (comp g) h) (comp (comp h)) ∈ (arrow w)))  



Definitions occuring in Statement :  spreadn: spread4 all: x:A. B[x] and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] product: x:A × B[x] universe: Type equal: 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: t ∈ T apply: 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: 2020_05_20-AM-07_49_22
Last ObjectModification: 2015_09_23-AM-09_29_03

Theory : small!categories


Home Index