Nuprl Definition : counit-unit-equations

counit-unit-equations(D;C;F;G;eps;eta) ==
  (∀d:cat-ob(D)
     ((cat-comp(C) (F d) (F (G (F d))) (F d) (F d (G (F d)) (eta d)) (eps (F d)))
     = (cat-id(C) (F d))
     ∈ (cat-arrow(C) (F d) (F d))))
  ∧ (∀c:cat-ob(C)
       ((cat-comp(D) (G c) (G (F (G c))) (G c) (eta (G c)) (G (F (G c)) c (eps c)))
       = (cat-id(D) (G c))
       ∈ (cat-arrow(D) (G c) (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 : and: P ∧ Q, all: ∀x:A. B[x], cat-ob: cat-ob(C), equal: s = t ∈ T, cat-arrow: cat-arrow(C), cat-comp: cat-comp(C), functor-arrow: arrow(F), cat-id: cat-id(C), apply: f a, functor-ob: ob(F)
FDL editor aliases : counit-unit-equations

Latex:
counit-unit-equations(D;C;F;G;eps;eta) == (\mforall{}d:cat-ob(D) ((cat-comp(C) (F d) (F (G (F d))) (F d) (F d (G (F d)) (eta d)) (eps (F d))) = (cat-id(C) (F d)))) \mwedge{} (\mforall{}c:cat-ob(C) ((cat-comp(D) (G c) (G (F (G c))) (G c) (eta (G c)) (G (F (G c)) c (eps c))) = (cat-id(D) (G c)))) Date html generated: 2020_05_20-AM-07_58_04 Last ObjectModification: 2017_01_16-PM-00_13_54 Theory : small!categories Home Index