Dans cet exposé je présenterai la notion de catégorie mu-bicomplète, et instancierai cette notion avec la catégorie des ensembles, via la notion de jeu de parité. J'expliquerai ensuite l'importance de chercher un syntaxe adéquate pour dénoter toutes les flèches d'une catégorie mu-bicomplète libre. Je proposerai donc la notion de preuve circulaire (avec la condition sur les cycles qu'elle doit satisfaire) comme une telle syntaxe ; je justifierai cette proposition par les résultats de correction et complétude (fortes, catégoriels) du calcul, par rapport à la sémantique catégorielle envisagée. Nous montrerons qu'un théorème d’élimination des coupures vaut, car on peut éliminer les coupures d'un preuve circulaire finie avec cut, pour obtenir un arbre de preuve infini sans cut. Nous montrerons comment ce processus d’élimination des coupures amène à caractériser toutes les fonctions d'ensembles qui sont l'image d'une flèche d'une catégorie mu-bicomplete libre.