Nuprl Definition : mk-adjunction
mk-adjunction(b.eps[b];a.eta[a]) == <b |→ eps[b], a |→ eta[a]>
Definitions occuring in Statement :
mk-nat-trans: x |→ T[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
mk-nat-trans: x |→ T[x]
FDL editor aliases :
mk-adjunction
Latex:
mk-adjunction(b.eps[b];a.eta[a]) == <b |\mrightarrow{} eps[b], a |\mrightarrow{} eta[a]>
Date html generated:
2020_05_20-AM-07_58_17
Last ObjectModification:
2017_01_16-PM-00_08_06
Theory : small!categories
Home
Index