Nuprl Definition : counit-unit-equations

counit-unit-equations(D;C;F;G;eps;eta) ==
  (∀d:cat-ob(D)
     ((cat-comp(C) (ob(F) d) (ob(F) (ob(G) (ob(F) d))) (ob(F) d) (arrow(F) d (ob(G) (ob(F) d)) (eta d)) (eps (ob(F) d)))
     = (cat-id(C) (ob(F) d))
     ∈ (cat-arrow(C) (ob(F) d) (ob(F) d))))
  ∧ (∀c:cat-ob(C)
       ((cat-comp(D) (ob(G) c) (ob(G) (ob(F) (ob(G) c))) (ob(G) c) (eta (ob(G) c)) 
         (arrow(G) (ob(F) (ob(G) c)) c (eps c)))
       = (cat-id(D) (ob(G) c))
       ∈ (cat-arrow(D) (ob(G) c) (ob(G) c))))


Definitions occuring in Statement :  functor-arrow: arrow(F),  functor-ob: ob(F),  cat-comp: cat-comp(C),  cat-id: cat-id(C),  cat-arrow: cat-arrow(C),  cat-ob: cat-ob(C),  all: ∀x:A. B[x],  and: P ∧ Q,  apply: f a,  equal: s = t ∈ T
Definitions occuring in definition :  functor-ob: ob(F),  apply: f a,  cat-id: cat-id(C),  functor-arrow: arrow(F),  cat-comp: cat-comp(C),  cat-arrow: cat-arrow(C),  equal: s = t ∈ T,  cat-ob: cat-ob(C),  all: ∀x:A. B[x],  and: P ∧ Q
FDL editor aliases :  counit-unit-equations
Latex:
counit-unit-equations(D;C;F;G;eps;eta)  ==
    (\mforall{}d:cat-ob(D)
          ((cat-comp(C)  (ob(F)  d)  (ob(F)  (ob(G)  (ob(F)  d)))  (ob(F)  d) 
              (arrow(F)  d  (ob(G)  (ob(F)  d))  (eta  d)) 
              (eps  (ob(F)  d)))
          =  (cat-id(C)  (ob(F)  d))))
    \mwedge{}  (\mforall{}c:cat-ob(C)
              ((cat-comp(D)  (ob(G)  c)  (ob(G)  (ob(F)  (ob(G)  c)))  (ob(G)  c)  (eta  (ob(G)  c)) 
                  (arrow(G)  (ob(F)  (ob(G)  c))  c  (eps  c)))
              =  (cat-id(D)  (ob(G)  c))))


Date html generated: 2017_01_19-PM-02_57_17
Last ObjectModification: 2017_01_16-PM-00_13_54

Theory : small!categories


Home Index