Elektrine lite

← Feed

Fredrik Bakke

FredrikBakke@mathstodon.xyz

<p>PhD student from Norway formalizing lots of stuff in univalent type theory using Agda</p>

Posts

  • Post #3005540

    Where does one even file for moral bankruptcy? Do student loans carry over?

  • Post #3005539

    Here&amp;#39;s a fun past time. What&amp;#39;s the shortest Agda program you can write that proves false? Constraints: 1. It must typecheck with `agda --safe` + any other flags you like 2. It must construct a term that inhabits an obviously empty type

  • Post #2093351

    I just made my first contribution to @SamToth&amp;#39;s `agda-synthetic-categories` today. This is a really cool library which builds on the recent Triangulated Type Theory of Gratzer and friends. Definitely worth checking out! https://samtoth.github.io/agda-synthetic-categories/