This repository contains a translation of Matita's arithmetic library in Agda, made using the tool Predicativize and the logical framework Dedukti. We refer to the paper Sharing proofs with predicative theories through universe polymorphic elaboration for an introduction to the tool and details about the translation.
Matita's arithmetic library had first been translated to Dedukti by Ali Assaf, using the tool Krajono. Details about the translation from Matita to Dedukti can be found in Ali's PhD thesis.