← Feed

Posts

• Post #2093355

  I’m having a GAT summer… (Slides credit to @jacobneu)

• Post #2093352

  The bittersweet feeling of getting rid of hundreds of lines of a fiddly proof in Agda to replace it with a nice, short, conceptual proof that’s about 17 lines long (and requires one fewer axiom). Details will follow (when I merge the code), but the main take away has been that the closure properties of orthogonal maps are very powerful (https://samtoth.github.io/agda-synthetic-categories/stt-00BZ/index.xml)

• Post #2093349

  Happy to have made my first contribution to Agda :) We now have a sharp modality (from https://arxiv.org/abs/1509.07584) which is a right adjoint to the flat modality which Agda already has. Sharp is an idempotent monad, so unlike flat it can be postulated in type theory… but I think having it as a builtin provides a lot of convenience for not a lot of extra complication to the theory. By defining it as a record, we have definitional eta-laws and I think it’s pretty cool being able to use Sharp...

• Post #2093348

  Is there an award somewhere for most cursed Agda snippet??

• Post #2093347

  I'm quite fond of the proof that π : U• → U is an object classifier - i.e. that is terminal in the category with objects (small) maps and morphisms cartesian squares. We show that a cartesian square from f to π is equivalent to the proposition that f is a small map (a concept which - amongst many other things - @FredrikBakke has recently formalised for agda-synthetic-categories). First we can straighten a cartesian map of arrows into a cartesian map of families. Explicitly this is a m...