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?