Abstract

Recent developments in the foundations of mathematics have led to a surge of interest in intensional theories of types and their applications in verified programming & formalised mathematics. Due to their constructive nature, these theories generally cannot benefit from classical proof automation techniques, but concurrently require a great deal of ‘bookkeeping’ to work with their proof-relevant notions of identity. In this talk, I’ll discuss a family of constructions know as ‘free extensions’ and how they can help alleviate some of this burden. Ultimately, I’ll describe an extensible tactic that I’ve developed for the Agda proof assistant, capable of synthesising proofs of algebraic identities. This tactic is formally verified as sound and complete, does not rely on postulates or extensionality, and is compatible with a broad variety of Agda configurations.