representing math structures

Stream: general

[Minghao Liu]

hello, has the Lean team considered using the "dependent record type with with construction" described in this paper "Dependently typed records for representing mathematical structure" to represent mathematical structures? The Agda technical report p85 mentioned this, but Agda decided to not use this

[Andrew Ashworth]

No?