What is a construction (in mathematics)? Related questions: Formally what is a mathematical construction? and What is a Universal Construction in Category Theory?
Backstory: A question arose in a seminar that concluded with the statement that Bernoulli shifts with the same entropy are isomorphic (proven by Ornstein in 1970 paper here): "Did Ornstein construct an explicit isomorphism?" The reply was that Ornstein indeed outlined a procedure. I left wondering about the definition of construction. This leads to my question.
Question: What is a construction (in mathematics)?
The answer I instinctively came up with is that a construction is a set in Gödel's constructible universe
I feel that this cannot be the complete picture.


*

*Category theory has a notion of a "universal property" which wants to describe structures up to isomorphisms. Then the class of all such structures may not be a set. Then maybe a construction is instead a class of objects satisfying a "universal property" i.e. a definable class. This falls in line with What is a Universal Construction in Category Theory?

*Formal logic with a deductive apparatus has a notion of a "proof" which wants to describe "theorems". Then maybe a construction is instead a "proof." i.e. a finite sequence of steps in the construction. This falls in line with Formally what is a mathematical construction?
There are three main ideas (1) existence <Gödel's constructible universe> (2) universal property <What is a Universal Construction in Category Theory?> and (3) finite sequence of steps <Formally what is a mathematical construction?>
Should all three combined be the definition?
 A: Your question sort of mixes syntax, semantics, informal notions of constructions, and Platonism or other philosophical approaches.
Suppose that you work in $\sf ZF+AD$. That means that the reals are not well-orderable. But you can still construct them from $\Bbb Q$. But now $\Bbb R\notin L$, so can you construct it or not? What about the "real reals"? Are they in $L$ or not? Maybe Woodin's Ultimate $L$ instead? But whenever Platonism is involved, questions of choice-of-theory start to rear their ugly head.
The truth is that a construction is an outline, which is accepted by other mathematicians as a correct algorithm for starting from something and ending up with something else.
The exact details of what is a construction are left to vary between one field and another. You might argue that a diagram chasing argument and appealing to a universal property is not "enough" to be called a construction. Others would tell you that a transfinite recursion which heavily relies on the choice of choice function/well-ordering is not a construction. And others would tell you that unless you can explicitly compute each and every object in the "constructed target", then it's not a construction.
Each of these are subject to the conventional jargon of the field of interest. If mathematics is what mathematicians do and other mathematicians agree to be mathematics, then a construction is something that mathematicians construct in their respective fields, and their colleagues agree to be a construction.
So at the end of the day, "construction" is context dependent. It might be one thing for a set theorist, and a whole other thing for a group theorist, and an entirely different thing for someone working in proof theory. I don't think you can fully quantify this into a mathematical definition, just like you can't quite quantify what it means for two proofs to be the same. This is more of a "pornography" thing: you can identify a construction when you see one, but it has no exact definition.
