Mathematics behind 'structure'

Stream: general

[Bart Michels]

I wonder what structures in Lean correspond to in type theory. My hypothesis is that they're not really a mathematical thing but an abstraction to avoid code repetition, and which Lean is able to translate into actual mathematics. A bit like abstract classes in Java, with the theorems about structures being non-abstract methods?

[Johan Commelin]

I think it's just syntactic sugar around an inductive type with one constructor... but I might be wrong.