Synthetic theories such as homotopy type theory axiomatize classical mathematical objects such as spaces up to homotopy. Although theorems in synthetic theories translate to theorems about the axiomatized structures on paper, this fact has not yet been exploited in proof assistants. This makes it challenging to formalize results in classical mathematics using synthetic methods. For example, Cubical Agda supports reasoning about cubical types, but cubical proofs have not been translated to proofs about cubical set models, let alone their topological realizations.
In this talk we will present SynthLean: a proof assistant that fills this gap by combining reasoning using synthetic theories with reasoning about their models.
SynthLean is part of the HoTTLean project, presented by Steve Awodey in this seminar series a week prior (on February 12th).
=== Online talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8H...
Meeting ID: 898 5609 1954 Passcode: ITPtalk