Notices by Boarders (boarders@mathstodon.xyz)

@julesh in mother Russia etc etc

@jonmsterling saw this via @timhenke

@julesh is that different than terms of a codata type (type that you interact with as codomains)?

@julesh it is striking to me that Google was easily at its most innovative when it had “20% time”, “authors at Google”, “flat management structure”, “Google summer of code” etc. etc. and whilst I am sure that created many seeming problems with how they have developed (perceived disorganization), they are left with the remnants of something wildly innovative dying to a new culture of growth-at-all-costs management which is positively contemptuous of all that built the company. A tech company that so disrespects its programmers/researchers will not remain innovative for long - who would want to work in such a place when your talents will be actually appreciated elsewhere?

@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?