45 citations · 56 across the 9 of their papers we have counts for
Showing 2023Show all
2 papers · 1 filter
cs.LO2023
A First Order Theory of Diagram Chasing
Assia Mahboubi, Matthieu Piquerez
This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chas…
cs.LO2023★ 2 cited
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance, Assia Mahboubi
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most…