Formalizing Constructive Projective Geometry in Agda

We present a formalization of Projective Geometry in the proof assistant and programming language Agda. We formalize a recent development in constructive Projective Geometry which has been shown appropriate to cover most traditional topics in the area applying only constructively valid methods. The equivalence with other well-known constructive axiomatic systems for projective geometry is proved and formalized. The implementation covers a basic fragment of intuitionistic synthetic Projective Plane Geometry including the axioms, principle of duality, Fano and Desargues properties and harmonic conjugates. We focus in an illustrative example of implementation of a complex and large proof which appears partially and vaguely described in the literature; namely the uniqueness of the harmonic conjugate. The most important details of our implementation are described and we show how to take advantage of several interesting properties of Agda such as modules, dependent record types, implicit arguments and instances which result very helpful to reduce the typical verbosity of formal proofs.