[Agda] separate definition of constructors?

[Roman]

> I think I saw Conor McBride do something like this a long time ago (in a
> talk in which he mentioned some building that was constructed by
> building one floor at a time on the ground and then hoisting it up,
> finishing with the ground floor, or something like that)

Here is a reference:
https://pigworker.wordpress.com/2015/01/09/universe-hierarchies/

A quote:

> What would I do? I’d think about the Central Bank of Ireland, a magnificent work of performance
> architecture by the late Sam Stephenson. The building was constructed around a pair of
> reinforced concrete lift shafts. Working at ground level, they built one floor of the building, and
> then they winched it up to the top of the lift shafts and pinned it into place. The building
> appeared to be growing downward from the Dublin sky. At each step, they did the construction
> at the lowest level possible, then shifted it to where they needed it.