You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Andre Knispel (Apr 08 2020 at 16:07):Not sure if this goes in here, but I'll be talking about my type theory powered by metaprogramming over at twitch tomorrow: https://twitter.com/AndreKnispel/status/1247914790598688772?s=20
Some people here have seen my talk about it at the Statebox Summit last year (https://www.youtube.com/watch?v=QW37iWVSN5Y), and there has been a lot of progress since then. It has some cool features that you don't get in other proof assistants, for example the ability to reason in a logic that has been formalized within the system, without syntactic overhead (which should be fun if you want to write programs in topoi).
I'm planning to give a talk and demo on my work on Meta-Cedille (https://github.com/WhatisRT/meta-cedille) tomorrow (the 9th) at 18:00 (GMT+2) over at https://www.twitch.tv/whatisrt_
- Andre Knispel (@AndreKnispel)