Boarders@julesh one thing I’d like to know is how one relates ”cut elimination” for algebraic structures - e.g. cut elimination says that the definitionally defined free group is isomorphic to the normalized word free group (and same for categorical structures) - to sequent calculus style “cut elimination” (which inevitably involves some extremely nasty induction proof and feels magic) - are these just supposed to be superficially similar or is the proof theory ideally meant to fit into the story about free algebraic structures?
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.