Nuprl Definition : counit-unit-adjunction
F -| G ==
{p:nat-trans(B;B;functor-comp(G;F);1) × nat-trans(A;A;1;functor-comp(F;G))|
counit-unit-equations(A;B;F;G;fst(p);snd(p))}
Definitions occuring in Statement :
counit-unit-equations: counit-unit-equations(D;C;F;G;eps;eta),
id_functor: 1,
functor-comp: functor-comp(F;G),
nat-trans: nat-trans(C;D;F;G),
pi1: fst(t),
pi2: snd(t),
set: {x:A| B[x]} ,
product: x:A × B[x]
Definitions occuring in definition :
pi2: snd(t),
pi1: fst(t),
counit-unit-equations: counit-unit-equations(D;C;F;G;eps;eta),
functor-comp: functor-comp(F;G),
id_functor: 1,
nat-trans: nat-trans(C;D;F;G),
product: x:A × B[x],
set: {x:A| B[x]}
FDL editor aliases :
counit-unit-adjunction
Latex:
F -| G ==
\{p:nat-trans(B;B;functor-comp(G;F);1) \mtimes{} nat-trans(A;A;1;functor-comp(F;G))|
counit-unit-equations(A;B;F;G;fst(p);snd(p))\}
Date html generated:
2017_01_19-PM-02_57_24
Last ObjectModification:
2017_01_16-PM-00_21_13
Theory : small!categories
Home
Index