Nuprl Definition : cat-monad

Monad(C) ==
  {M:T:Functor(C;C) × nat-trans(C;C;1;T) × nat-trans(C;C;functor-comp(T;T);T)| 
   let T,u,m = M in 
   (∀X:cat-ob(C)
      ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (u (ob(T) X)) (m X))
      = (cat-id(C) (ob(T) X))
      ∈ (cat-arrow(C) (ob(T) X) (ob(T) X))))
   ∧ (∀X:cat-ob(C)
        ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (arrow(T) X (ob(T) X) (u X)) (m X))
        = (cat-id(C) (ob(T) X))
        ∈ (cat-arrow(C) (ob(T) X) (ob(T) X))))
   ∧ (∀X:cat-ob(C)
        ((cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) (m (ob(T) X)) (m X))
        = (cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) 
           (arrow(T) (ob(T) (ob(T) X)) (ob(T) X) (m X)) 
           (m X))
        ∈ (cat-arrow(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) X))))} 


Definitions occuring in Statement :  id_functor: 1,  functor-comp: functor-comp(F;G),  nat-trans: nat-trans(C;D;F;G),  functor-arrow: arrow(F),  functor-ob: ob(F),  cat-functor: Functor(C1;C2),  cat-comp: cat-comp(C),  cat-id: cat-id(C),  cat-arrow: cat-arrow(C),  cat-ob: cat-ob(C),  spreadn: spread3,  all: ∀x:A. B[x],  and: P ∧ Q,  set: {x:A| B[x]} ,  apply: f a,  product: x:A × B[x],  equal: s = t ∈ T
Definitions occuring in definition :  set: {x:A| B[x]} ,  cat-functor: Functor(C1;C2),  product: x:A × B[x],  id_functor: 1,  nat-trans: nat-trans(C;D;F;G),  functor-comp: functor-comp(F;G),  spreadn: spread3,  and: P ∧ Q,  functor-arrow: arrow(F),  cat-id: cat-id(C),  all: ∀x:A. B[x],  cat-ob: cat-ob(C),  equal: s = t ∈ T,  cat-arrow: cat-arrow(C),  cat-comp: cat-comp(C),  apply: f a,  functor-ob: ob(F)
FDL editor aliases :  cat-monad
Latex:
Monad(C)  ==
    \{M:T:Functor(C;C)  \mtimes{}  nat-trans(C;C;1;T)  \mtimes{}  nat-trans(C;C;functor-comp(T;T);T)| 
      let  T,u,m  =  M  in 
      (\mforall{}X:cat-ob(C)
            ((cat-comp(C)  (ob(T)  X)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (u  (ob(T)  X))  (m  X))
            =  (cat-id(C)  (ob(T)  X))))
      \mwedge{}  (\mforall{}X:cat-ob(C)
                ((cat-comp(C)  (ob(T)  X)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (arrow(T)  X  (ob(T)  X)  (u  X))  (m  X))
                =  (cat-id(C)  (ob(T)  X))))
      \mwedge{}  (\mforall{}X:cat-ob(C)
                ((cat-comp(C)  (ob(T)  (ob(T)  (ob(T)  X)))  (ob(T)  (ob(T)  X))  (ob(T)  X)  (m  (ob(T)  X))  (m  X))
                =  (cat-comp(C)  (ob(T)  (ob(T)  (ob(T)  X)))  (ob(T)  (ob(T)  X))  (ob(T)  X) 
                      (arrow(T)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (m  X)) 
                      (m  X))))\} 


Date html generated: 2017_01_19-PM-02_57_43
Last ObjectModification: 2017_01_16-PM-07_38_20

Theory : small!categories


Home Index