Geodesic
A practical type theory for symmetric monoidal categories
Theory and applications of categories, Tome 37 (2021), pp. 863-907

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

We give a natural-deduction-style type theory for symmetric monoidal categories whose judgmental structure directly represents morphisms with tensor products in their codomain as well as their domain. The syntax is inspired by Sweedler notation for coalgebras, with variables associated to types in the domain and terms associated to types in the codomain, allowing types to be treated informally like "sets with elements" subject to global linearity-like restrictions. We illustrate the usefulness of this type theory with various applications to duality, traces, Frobenius monoids, and (weak) Hopf monoids.

Publié le :
Classification : 18M05, 18M85, 03B47
Keywords: type theory, symmetric monoidal category, prop, coalgebra 
Michael Shulman. A practical type theory for symmetric monoidal categories. Theory and applications of categories, Tome 37 (2021), pp. 863-907. http://geodesic.mathdoc.fr/item/TAC_2021_37_a24/
@article{TAC_2021_37_a24,
     author = {Michael Shulman},
     title = {A practical type theory for symmetric monoidal categories},
     journal = {Theory and applications of categories},
     pages = {863--907},
     year = {2021},
     volume = {37},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2021_37_a24/}
}
TY  - JOUR
AU  - Michael Shulman
TI  - A practical type theory for symmetric monoidal categories
JO  - Theory and applications of categories
PY  - 2021
SP  - 863
EP  - 907
VL  - 37
UR  - http://geodesic.mathdoc.fr/item/TAC_2021_37_a24/
LA  - en
ID  - TAC_2021_37_a24
ER  - 
%0 Journal Article
%A Michael Shulman
%T A practical type theory for symmetric monoidal categories
%J Theory and applications of categories
%D 2021
%P 863-907
%V 37
%U http://geodesic.mathdoc.fr/item/TAC_2021_37_a24/
%G en
%F TAC_2021_37_a24