Is there a choice-free proof that a Euclidean domain is a UFD?

There are two parts to showing a Euclidean domain or a PID are UFDs: (i) existence of an irreducible factorization for every nonzero nonunit and (ii) essential uniqueness of the irreducible factorization (any two use the same number of irreducible factors and the irreducibles that occur in both factorizations can be matched termwise up to multiplication by a unit).

To prove (ii), the key point is that every irreducible element is a prime element, and to prove that you need to be able to write $px + ay = 1$ for any irreducible $p$ and element $a$ where $p \nmid a$; the nondivisibility implies (since $p$ is irreducible) that the only common factors of $p$ and $a$ are units, so Euclid's algorithm in a Euclidean domain lets you algorithmically solve $px + ay = 1$ for some $x$ and $y$. In a PID you'd instead observe that the ideal $(p,a)$ has to be $(1)$.

To prove (i) is a major distinction between Euclidean domains and PIDs. You can do this for Euclidean domains in a much more concrete way than for PIDs. I compare approaches for each as Theorems 4.2 and 4.3 at http://www.math.uconn.edu/~kconrad/blurbs/ringtheory/euclideanrk.pdf. You need to read Sections 2 and 3 first to see why I mean about being able to assume the "$d$-inequality" holds: a Euclidean domain does not have to have its "norm" function $d$ be totally multiplicative or satisfy $d(a) \leq d(ab)$, but you can always adjust the "norm" function to fit that inequality all the time if it doesn't at the start. (Some books make this inequality part of the definition of a Euclidean domain and some do not.) Of course in $\mathbf Z$ and $F[x]$ that inequality is true, so you save some time when proving those rings are UFDs compared to a general Euclidean domain.

The bottom line is that you definitely do not need to introduce the machinery of PIDs in order to prove rings like $\mathbf Z$ or $F[x]$ have unique factorization. After all, unique factorization in those types of rings as well as in $\mathbf Z[i]$ was known (say, to Gauss) long before there was a concept of PID. I remember being surprised when I first saw how PIDs are proved to be UFDs, since I knew the case of Euclidean domains already and the proof of part (i) for PIDs was rather more abstract than I expected.

Given a non-unit $r \in R$, let $p$ be a non-unit divisor of $r$ that has minimal norm. Then $p$ must be irreducible. By induction on the norm, we know that $r/p$ is a product of primes (or a unit), so $r = p \cdot (r/p)$ is a product of primes. I don't think the usual proof of the uniqueness of the decomposition uses the axiom of choice (the key is just to prove that if $p \mid ab$, then either $p \mid a$ or $p \mid b$), so it seems to me that we are done.