Tootfinder

In the paper "Agda-ventures with PolyP" Jeremy Gibbons (@…) and I revisit PolyP in a literate Agda setting — combining executable code, theory, and reflection on three decades of generic programming. It is part of a Festschrift gifted to Johan Jeuring at the academic celebration of his 60th birthday.
📖 Blog post:

Which version of the rendered maths in the Agda manual looks better on your screen?
PNG
SVG
about the same

Substitution Without Copy and Paste
Thorsten Altenkirch (University of Nottingham), Nathaniel Burke (Imperial College London), Philip Wadler (University of Edinburgh)
https://arxiv.org/abs/2510.12304

Substitution Without Copy and Paste
Defining substitution for a language with binders like the simply typed $λ$-calculus requires repetition, defining substitution and renaming separately. To verify the categorical properties of this calculus, we must repeat the same argument many times. We present a lightweight method that avoids repetition and that gives rise to a simply typed category with families (CwF) isomorphic to the initial simply typed CwF. Our paper is a literate Agda script.

Final ICFP keynote on Proof-Carrying Neuro-Symbolic Code by Ekaterina Komendantskaya
#icfpsplash25
https://share.google/G4C1iRyA0qE5m5Mi2

On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
Sebasti\'an Urciuoli (Universidad ORT Uruguay)
https://arxiv.org/abs/2510.12300

On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
We develop formal theories of conversion for Church-style lambda-terms with Pi-types in first-order syntax using one-sorted variables names and Stoughton's multiple substitutions. We then formalize the Pure Type Systems along some fundamental metatheoretic properties: weakening, syntactic validity, closure under alpha-conversion and substitution. Finally, we compare our formalization with others related. The whole development has been machine-checked using the Agda system. Our work demonstrate…

whenever i open the github actions log in my browser and it's typechecking some agda my fans start spinning about as fast as if i were running agda myself. i love the modern web

Thinking about structure preservation. Given a nice enough (say, GAT) signature like (pseudo-Agda)
we can automatically derive the appropriate notion of homomorphism:
But what if I want to talk about preserving derived structure, like terminal objects? I might try to extend the signature (C : Cat) with (c : Ob C) (_ : is-terminal c), but then a morphism between those is just a pointed functor, so this doesn't help. Rather than extend Cat with a terminal object, it seems like I need to extend it with the notion of terminality itself:
This extends the notion of homomorphism like so:
Now every Cat extends to a CatWithTerminality by setting IsTerminal := is-terminal, and we can say that a Functor preserves terminal objects if it extends to a FunctorWithTerminality.
Has anyone thought about this in similar terms?