Structure associated to every Desarguesian projective plane

Stream: general

[Quinn Culver]

En route to formalizing the fundamental theorem of projective geometry, I want to declare a structure associated to every Desarguesian projective plane. (The fundamental theorem says that structure is a division ring that coordinatizes the plane.) TPIL gives the following syntax

structure <name> <parameters> <parent-structures> : Sort u :=
  <constructor> :: <fields>

Should the projective plane be one of the parameters? Do I need to use inheritance?

[Reid Barton]

Probably it should be a parameter but hard to guess without more information.