The question is about declarative versus computational formalization.
In the declarative style we characterize a “thing” by stating conditions,
quite often universal properties, that determine it up to a unique isomorphism. Any “thing” satisfying the stated conditions is acceptable.
In the computational style we just construct the “thing” concretely, and use features provided by the proof assistant to compute with it directly.
A typical example is the structure of natural numbers. In the declarative style we define “pointed successor algebra” and say that $\mathbb{N}$ is an initial pointed successor algebra. In the computational style we define $\mathbb{N}$ as an inductive type.
Each approach has benefits and drawbacks:
The declarative style is more flexible, but doing everything in this style complicates formalization. For example, one can never refer to “the natural numbers $\mathbb{N}$” but must always say “and given an initial pointed successor algebra $N$ ..." Now imagine you had to do this every time you wanted to mention a cartesian product, a function space, a unit type, etc.
The computational style allows us to compute more easily (although the declarative one does as well with some extra work), but it locks in specific design choices. You defined natural numbers in unary, but now you'd like to compute in binary? Tough luck, you'll have to get the proof assistant developers to hack the system and provide some magic.
People tend to use the computational style, but there are situations which demand a different approach because the “unique up to unique isomorphism“ cannot be realized as an exact equality. For example, suppose we want to define “the $n$-th power of $A$” as a type? That's easily done:
open import Data.Nat
open import Data.Product
open import Data.Unit
module Cow where
power : Set → ℕ → Set
power A zero = ⊤
power A (suc n) = A × power A n
But what if we want $A^{n + m} = A^n \times A^m$ to hold as an equality? This might be doable, but is at the very least going to require a lot of trickery and fragile design. And then someone is going to walk in and ask about $A^0 = 1$, and everything will crumble.
The Lean library defines is_localization for a similar reason. Because the “equality” $R[1/f][1/g] = R[1/f g]$ (or some such) cannot be achieved using any reasonable concrete construction of $R[1/f]$, we switch to declarative style as we have to deal with isomorphisms anyhow.
In my opinion, we are not facing just a formalization engineering problem, but rather a genuinely mathematical one. Many branches of mathematics sweep the problem under the rug by saying things like “we identify $A^{n + m}$ with $A^n \times A^m$“ – but homotopy theorists and higher-category theorists thrive on it. It remains to be seen how their insights can be transformed into formalization techniques. A very good attempt is homotopy type theory and univalent mathematics, which however requires one to pay a high price – a new way of thinking – and is therefore not very popular.
