[{"id":"116424945485030920","created_at":"2026-04-18T09:14:44.769Z","in_reply_to_id":"116424907610156077","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116424945485030920","url":"https://mathstodon.xyz/@olynch/116424945485030920","replies_count":5,"reblogs_count":7,"favourites_count":23,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Sysadmin should be a first year comp sci course in the same way proof writing is sometimes a first year math course, or lab safety is a first year mech eng course.\u003c/p\u003e\u003cp\u003eGit, Linux, shell scripts, vi, ssh, how to deploy a python app on top of an nginx reverse proxy, how to set up unit tests and an auto formatter in CI...\u003c/p\u003e\u003cp\u003eAlso all incoming students should just be given a Linux laptop. Compared to the overall cost of a CS degree it\u0026#39;s not much, and it would probably pay for itself in reducing the admin time it takes to debug utterly baroque Windows install processes on student laptops.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116424850421026319","created_at":"2026-04-18T08:50:34.207Z","in_reply_to_id":"116422654677721143","in_reply_to_account_id":"113987899628157658","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116424850421026319","url":"https://mathstodon.xyz/@olynch/116424850421026319","replies_count":0,"reblogs_count":0,"favourites_count":0,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://types.pl/@constantine\" class=\"u-url mention\"\u003e@\u003cspan\u003econstantine\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://types.pl/@trebor\" class=\"u-url mention\"\u003e@\u003cspan\u003etrebor\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Really cool! I wish I knew more Agda so I could understand this better...\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"113987899628157658","username":"constantine","url":"https://types.pl/@constantine","acct":"constantine@types.pl"},{"id":"109487575099728939","username":"trebor","url":"https://types.pl/@trebor","acct":"trebor@types.pl"},{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116393021597365730","created_at":"2026-04-12T17:56:04.901Z","in_reply_to_id":"116392916740063763","in_reply_to_account_id":"109347460237678866","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116393021597365730","url":"https://mathstodon.xyz/@olynch/116393021597365730","replies_count":1,"reblogs_count":0,"favourites_count":0,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@danielgratzer\" class=\"u-url mention\"\u003e@\u003cspan\u003edanielgratzer\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://types.pl/@bentnib\" class=\"u-url mention\"\u003e@\u003cspan\u003ebentnib\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e :O so many adjoints\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109347460237678866","username":"danielgratzer","url":"https://mathstodon.xyz/@danielgratzer","acct":"danielgratzer"},{"id":"108206105447876320","username":"bentnib","url":"https://types.pl/@bentnib","acct":"bentnib@types.pl"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116392657539045836","created_at":"2026-04-12T16:23:29.812Z","in_reply_to_id":null,"in_reply_to_account_id":null,"sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116392657539045836","url":"https://mathstodon.xyz/@olynch/116392657539045836","replies_count":3,"reblogs_count":0,"favourites_count":3,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003eIs there a left adjoint to Nakano\u0026#39;s later modality? It would be nice to handle it MTT style as a positive modality, rather than just have it as an applicative functor.\u003c/p\u003e\u003cp\u003ePerhaps it needs linearity in order to work though, because it\u0026#39;s not a monad...\u003c/p\u003e\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@danielgratzer\" class=\"u-url mention\"\u003e@\u003cspan\u003edanielgratzer\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://types.pl/@bentnib\" class=\"u-url mention\"\u003e@\u003cspan\u003ebentnib\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109347460237678866","username":"danielgratzer","url":"https://mathstodon.xyz/@danielgratzer","acct":"danielgratzer"},{"id":"108206105447876320","username":"bentnib","url":"https://types.pl/@bentnib","acct":"bentnib@types.pl"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116390155487142273","created_at":"2026-04-12T05:47:11.529Z","in_reply_to_id":"116388560162882132","in_reply_to_account_id":"3032","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116390155487142273","url":"https://mathstodon.xyz/@olynch/116390155487142273","replies_count":0,"reblogs_count":0,"favourites_count":0,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@byorgey\" class=\"u-url mention\"\u003e@\u003cspan\u003ebyorgey\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e I seem to remember \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://types.pl/@JacquesC2\" class=\"u-url mention\"\u003e@\u003cspan\u003eJacquesC2\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e using this type of equivalence relation to great effect in proof assistants...\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"3032","username":"byorgey","url":"https://mathstodon.xyz/@byorgey","acct":"byorgey"},{"id":"108235819379958852","username":"JacquesC2","url":"https://types.pl/@JacquesC2","acct":"JacquesC2@types.pl"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116386894706255013","created_at":"2026-04-11T15:57:55.961Z","in_reply_to_id":null,"in_reply_to_account_id":null,"sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116386894706255013","url":"https://mathstodon.xyz/@olynch/116386894706255013","replies_count":2,"reblogs_count":0,"favourites_count":7,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003eThe observation that I can get trapped by almost any site with an algorithmic feed (YouTube, Twitter, Reddit, hell even Facebook), no matter how asinine the content it gives me, is very humbling to any pretensions of taste that I have...\u003c/p\u003e\u003cp\u003eTo escape these, the solution has never been to block the relevant domain in ublock, because I inevitably end up wanting to look at some link that someone has sent, and then I unblock it, and then it\u0026#39;s off to the races. The solution is also not self control. Maybe that works for some people. The solution is to figure out how to make the site dumber. For Twitter, it was locking my account. For YouTube it was disabling having a YouTube history, so that my home page was blank of recommendations. Facebook is dumb enough that I mostly manage to stay off it organically, thankfully. And for Reddit, I switched to Old Reddit and unsubscribed to all subreddits so my homepage is blank.\u003c/p\u003e\u003cp\u003eI still have the muscle memory for all of these things, even though I\u0026#39;ve been off Twitter for over a year, my fingers will still sometimes type twitter.com into a freshly opened tab.\u003c/p\u003e\u003cp\u003eI really think the algorithmic feed is one of the worst intentions of the 21st century. I don\u0026#39;t think it\u0026#39;s a good idea to ban it, but I think that there should always be a way (like I\u0026#39;ve found with YouTube and Reddit) of disabling the feed while keeping access to other material on the site.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116381746060363415","created_at":"2026-04-10T18:08:33.860Z","in_reply_to_id":"116381708600117812","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116381746060363415","url":"https://mathstodon.xyz/@olynch/116381746060363415","replies_count":0,"reblogs_count":0,"favourites_count":1,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Ah gotcha :)\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116381701064822138","created_at":"2026-04-10T17:57:07.283Z","in_reply_to_id":"116381340369490097","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116381701064822138","url":"https://mathstodon.xyz/@olynch/116381701064822138","replies_count":1,"reblogs_count":0,"favourites_count":0,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Does this mean inline definitions in telescopes used for dependent records? Or just let bindings? I\u0026#39;ve never had trouble with let bindings, so I\u0026#39;m curious about what the difficulty is.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116376756011618910","created_at":"2026-04-09T20:59:31.759Z","in_reply_to_id":"116376748103360065","in_reply_to_account_id":"111496425044625396","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116376756011618910","url":"https://mathstodon.xyz/@olynch/116376756011618910","replies_count":0,"reblogs_count":0,"favourites_count":3,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@SamToth\" class=\"u-url mention\"\u003e@\u003cspan\u003eSamToth\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Ah, should have guessed that! OK, fortunately now I work in the same office as Mitchell so I\u0026#39;ll ask him about it.\u003c/p\u003e","reblog":null,"application":{"name":"Web","website":null},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"111496425044625396","username":"SamToth","url":"https://mathstodon.xyz/@SamToth","acct":"SamToth"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116376655041773253","created_at":"2026-04-09T20:33:51.081Z","in_reply_to_id":null,"in_reply_to_account_id":null,"sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116376655041773253","url":"https://mathstodon.xyz/@olynch/116376655041773253","replies_count":3,"reblogs_count":0,"favourites_count":2,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003eModal type theory people:\u003c/p\u003e\u003cp\u003eGiven a judgmental proposition P (that is, not necessarily a type, a meta-level proposition), there is an open modality associated to it which looks like (P -\u0026gt; A), this is right adjoint to adding a proof of P to the context. So far, so good.\u003c/p\u003e\u003cp\u003eI want to now instead have a context formation operator which acts like (P -\u0026gt; Γ). My intuition here is that (P -\u0026gt; Γ) \u0026quot;locks\u0026quot; the context Γ, and Γ,P \u0026quot;unlocks\u0026quot; the context. This seems to make sense because (P -\u0026gt; Γ,P) = (P -\u0026gt; Γ), (locking something unlocked is the same as locking the original thing) and (P -\u0026gt; Γ),P = Γ,P (unlocking something that has been locked is the same as unlocking the original thing).\u003c/p\u003e\u003cp\u003eNow, I don\u0026#39;t expect (P -\u0026gt; Γ) to have a further right adjoint (I\u0026#39;m using it for a different purpose). But is this a kind of context operation that people have looked at?\u003c/p\u003e","reblog":null,"application":{"name":"Web","website":null},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116362716700255819","created_at":"2026-04-07T09:29:08.868Z","in_reply_to_id":null,"in_reply_to_account_id":null,"sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116362716700255819","url":"https://mathstodon.xyz/@olynch/116362716700255819","replies_count":0,"reblogs_count":0,"favourites_count":4,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003eWhenever I do something fancy with normalization by evaluation I have an urge to shout \u0026quot;Yes closures! Dance for me! Dance! Dance!\u0026quot;\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116352794797233999","created_at":"2026-04-05T15:25:52.644Z","in_reply_to_id":"116352606927003328","in_reply_to_account_id":"113283570352770474","sensitive":false,"spoiler_text":"","visibility":"unlisted","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116352794797233999","url":"https://mathstodon.xyz/@olynch/116352794797233999","replies_count":0,"reblogs_count":0,"favourites_count":3,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@carloangiuli\" class=\"u-url mention\"\u003e@\u003cspan\u003ecarloangiuli\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@ToucanIan\" class=\"u-url mention\"\u003e@\u003cspan\u003eToucanIan\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@sophiehuiberts\" class=\"u-url mention\"\u003e@\u003cspan\u003esophiehuiberts\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e I\u0026#39;m very happy to know this, but at the same time the phrase \u0026quot;they have played us for absolute fools\u0026quot; is ringing strongly in my head 🤣\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"113283570352770474","username":"carloangiuli","url":"https://mathstodon.xyz/@carloangiuli","acct":"carloangiuli"},{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"},{"id":"109313803364116583","username":"ToucanIan","url":"https://mathstodon.xyz/@ToucanIan","acct":"ToucanIan"},{"id":"109293519073784427","username":"sophiehuiberts","url":"https://mathstodon.xyz/@sophiehuiberts","acct":"sophiehuiberts"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116352785010163952","created_at":"2026-04-05T15:23:23.304Z","in_reply_to_id":"116352574938389981","in_reply_to_account_id":"108207575298675025","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116352785010163952","url":"https://mathstodon.xyz/@olynch/116352785010163952","replies_count":1,"reblogs_count":1,"favourites_count":2,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://types.pl/@brendan\" class=\"u-url mention\"\u003e@\u003cspan\u003ebrendan\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Eta expansion is canonicalization!\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"108207575298675025","username":"brendan","url":"https://types.pl/@brendan","acct":"brendan@types.pl"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116346854792187911","created_at":"2026-04-04T14:15:15.360Z","in_reply_to_id":"116346832308946587","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116346854792187911","url":"https://mathstodon.xyz/@olynch/116346854792187911","replies_count":0,"reblogs_count":0,"favourites_count":1,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mementomori.social/@tml\" class=\"u-url mention\"\u003e@\u003cspan\u003etml\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@albertcardona\" class=\"u-url mention\"\u003e@\u003cspan\u003ealbertcardona\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://neuromatch.social/@elduvelle\" class=\"u-url mention\"\u003e@\u003cspan\u003eelduvelle\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Alright, I\u0026#39;ll back off from this conversation.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"},{"id":"114794619671062813","username":"tml","url":"https://mementomori.social/@tml","acct":"tml@mementomori.social"},{"id":"109404767338318455","username":"albertcardona","url":"https://mathstodon.xyz/@albertcardona","acct":"albertcardona"},{"id":"109560680367918792","username":"elduvelle","url":"https://neuromatch.social/@elduvelle","acct":"elduvelle@neuromatch.social"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116346838739037810","created_at":"2026-04-04T14:11:10.408Z","in_reply_to_id":"116346786149834561","in_reply_to_account_id":"114794619671062813","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116346838739037810","url":"https://mathstodon.xyz/@olynch/116346838739037810","replies_count":2,"reblogs_count":0,"favourites_count":0,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mementomori.social/@tml\" class=\"u-url mention\"\u003e@\u003cspan\u003etml\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@albertcardona\" class=\"u-url mention\"\u003e@\u003cspan\u003ealbertcardona\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://neuromatch.social/@elduvelle\" class=\"u-url mention\"\u003e@\u003cspan\u003eelduvelle\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e Presumably the claim is something like \u0026quot;transit was 10x more competently and sensibly prioritized and organized relative to the technological capabilities of the time\u0026quot; not \u0026quot;transit was 10x faster.\u0026quot;\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"114794619671062813","username":"tml","url":"https://mementomori.social/@tml","acct":"tml@mementomori.social"},{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"},{"id":"109404767338318455","username":"albertcardona","url":"https://mathstodon.xyz/@albertcardona","acct":"albertcardona"},{"id":"109560680367918792","username":"elduvelle","url":"https://neuromatch.social/@elduvelle","acct":"elduvelle@neuromatch.social"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116346827111686284","created_at":"2026-04-04T14:08:12.988Z","in_reply_to_id":"116346737869814264","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116346827111686284","url":"https://mathstodon.xyz/@olynch/116346827111686284","replies_count":1,"reblogs_count":0,"favourites_count":6,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mementomori.social/@tml\" class=\"u-url mention\"\u003e@\u003cspan\u003etml\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@albertcardona\" class=\"u-url mention\"\u003e@\u003cspan\u003ealbertcardona\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://neuromatch.social/@elduvelle\" class=\"u-url mention\"\u003e@\u003cspan\u003eelduvelle\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e I\u0026#39;m all for improving the train system, but I worry that this is unnecessary FUD (fear, uncertainty, doubt) w.r.t. people making transit decisions. I\u0026#39;ve traveled between Southern England and Scotland probably four or five times now (and other long distances in the UK) and sometimes it takes longer than advertised, but the magic of a train ticket being \u0026quot;any permitted route\u0026quot; means that Google maps can just route me around missed trains. And Oxford\u0026lt;-\u0026gt;Cambridge is annoying but certainly doable for a day trip with an early morning start.\u003c/p\u003e\u003cp\u003ePerhaps I\u0026#39;m less optimized for reliably getting places on time than you, but I think there\u0026#39;s a strong case to be made for not refusing to use infrastructure until it\u0026#39;s perfect.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"},{"id":"114794619671062813","username":"tml","url":"https://mementomori.social/@tml","acct":"tml@mementomori.social"},{"id":"109404767338318455","username":"albertcardona","url":"https://mathstodon.xyz/@albertcardona","acct":"albertcardona"},{"id":"109560680367918792","username":"elduvelle","url":"https://neuromatch.social/@elduvelle","acct":"elduvelle@neuromatch.social"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116346759862032502","created_at":"2026-04-04T13:51:06.839Z","in_reply_to_id":"116346641226292523","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116346759862032502","url":"https://mathstodon.xyz/@olynch/116346759862032502","replies_count":2,"reblogs_count":0,"favourites_count":1,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e I think that perhaps those people could be meaning that dependent records are *positive* types, e.g. they have a mapping out universal property. Which is not to say that they should be *defined* in this way, but it is a useful fact sometimes. (That is, it is a useful fact that they are both positive and negative... Though this reminds me of certain people raging about how a subset of a topological space can be closed and open).\u003c/p\u003e\u003cp\u003eAnd I didn\u0026#39;t know that eta rules for recursive types were undecidable... I will have to think about why this is the case.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116346222033230133","created_at":"2026-04-04T11:34:20.222Z","in_reply_to_id":"116345545240360644","in_reply_to_account_id":"286766","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116346222033230133","url":"https://mathstodon.xyz/@olynch/116346222033230133","replies_count":2,"reblogs_count":0,"favourites_count":3,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003eHmmm, I\u0026#39;m wondering if this is actually the intuition for why inductive types sometimes don\u0026#39;t have uniqueness rules (eta rules). The whole point of an inductive type is that *it suffices to assume* that an element is produced by one of a couple introductions. So we don\u0026#39;t need to say that this is *actually* the case, and sometimes it\u0026#39;s useful (for instance, for gen 1 HoTT) to stick some weird elements inside of an inductive type.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116345865910474866","created_at":"2026-04-04T10:03:46.221Z","in_reply_to_id":"116345838287390080","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116345865910474866","url":"https://mathstodon.xyz/@olynch/116345865910474866","replies_count":0,"reblogs_count":0,"favourites_count":6,"quotes_count":0,"edited_at":"2026-04-04T10:03:58.367Z","content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@albertcardona\" class=\"u-url mention\"\u003e@\u003cspan\u003ealbertcardona\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://neuromatch.social/@elduvelle\" class=\"u-url mention\"\u003e@\u003cspan\u003eelduvelle\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e OK, this I can get behind! We must feed our magnificent beasts well :)\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"},{"id":"109404767338318455","username":"albertcardona","url":"https://mathstodon.xyz/@albertcardona","acct":"albertcardona"},{"id":"109560680367918792","username":"elduvelle","url":"https://neuromatch.social/@elduvelle","acct":"elduvelle@neuromatch.social"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}},{"id":"116345640465437095","created_at":"2026-04-04T09:06:26.203Z","in_reply_to_id":"116345604941508998","in_reply_to_account_id":"109252829448079076","sensitive":false,"spoiler_text":"","visibility":"public","language":"en","uri":"https://mathstodon.xyz/users/olynch/statuses/116345640465437095","url":"https://mathstodon.xyz/@olynch/116345640465437095","replies_count":2,"reblogs_count":2,"favourites_count":18,"quotes_count":0,"edited_at":null,"content":"\u003cp\u003e\u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@jonmsterling\" class=\"u-url mention\"\u003e@\u003cspan\u003ejonmsterling\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://mathstodon.xyz/@albertcardona\" class=\"u-url mention\"\u003e@\u003cspan\u003ealbertcardona\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e \u003cspan class=\"h-card\" translate=\"no\"\u003e\u003ca href=\"https://neuromatch.social/@elduvelle\" class=\"u-url mention\"\u003e@\u003cspan\u003eelduvelle\u003c/span\u003e\u003c/a\u003e\u003c/span\u003e I kind of enjoy the vibe of public transit where it\u0026#39;s like these are migrating beasts and by careful divination and ritual offering you can harness their primal energy to speed you in a particular direction, like a raptor riding thermals. Of course there isn\u0026#39;t going to be a migration going precisely from A to B, but with a bit of cleverness you can stitch together something.\u003c/p\u003e\u003cp\u003eIt\u0026#39;s pretty magical and unprecedented in human history that I can cross so many different countries by land safely and relatively quickly. Sure, OK, it could be faster. But like, thank you migrating beasts you are wonderful creatures.\u003c/p\u003e","reblog":null,"application":{"name":"Tusky","website":"https://tusky.app"},"account":{"id":"286766","username":"olynch","acct":"olynch","display_name":"Owen Lynch","locked":false,"bot":false,"discoverable":true,"indexable":false,"group":false,"created_at":"2022-04-25T00:00:00.000Z","note":"\u003cp\u003eGrad student at Oxford, Research Software Engineer at the Topos Institute.\u003c/p\u003e\u003cp\u003eCurrently working on the programming language side of systems theory.\u003c/p\u003e\u003cp\u003eTrump is a fascist, fascists are bad.\u003c/p\u003e","url":"https://mathstodon.xyz/@olynch","uri":"https://mathstodon.xyz/users/olynch","avatar":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","avatar_static":"https://media.mathstodon.xyz/accounts/avatars/000/286/766/original/4b06ab333858358e.png","header":"https://mathstodon.xyz/headers/original/missing.png","header_static":"https://mathstodon.xyz/headers/original/missing.png","followers_count":248,"following_count":104,"statuses_count":666,"last_status_at":"2026-04-18","hide_collections":null,"noindex":false,"emojis":[],"roles":[],"fields":[{"name":"Website","value":"\u003ca href=\"https://owenlynch.org\" target=\"_blank\" rel=\"nofollow noopener me\" translate=\"no\"\u003e\u003cspan class=\"invisible\"\u003ehttps://\u003c/span\u003e\u003cspan class=\"\"\u003eowenlynch.org\u003c/span\u003e\u003cspan class=\"invisible\"\u003e\u003c/span\u003e\u003c/a\u003e","verified_at":null}]},"media_attachments":[],"mentions":[{"id":"109252829448079076","username":"jonmsterling","url":"https://mathstodon.xyz/@jonmsterling","acct":"jonmsterling"},{"id":"109404767338318455","username":"albertcardona","url":"https://mathstodon.xyz/@albertcardona","acct":"albertcardona"},{"id":"109560680367918792","username":"elduvelle","url":"https://neuromatch.social/@elduvelle","acct":"elduvelle@neuromatch.social"}],"tags":[],"emojis":[],"quote":null,"card":null,"poll":null,"quote_approval":{"automatic":["public"],"manual":[],"current_user":"denied"}}]