After a long discussion on the Lean Zulip, Mario Carneiro has shown that the Calculus of Inductive Constructions (in its full version w/ large elimination of Acc) + Excluded Middle proves that ZF is consistent: https://arxiv.org/abs/2609.23143 It is fairly simple to show that Aczel’s type of sets as well-founded trees is a model of ZF without Replacement, and even a bit further, that the iterative hierarchy V_alpha exists for all ordinals alpha, but Replacement seems very analogous to Unique Choice, and there is (as far as I am aware) no syntactic construction that can show the relative consistency of UC (or LEM) over CiC w/ large elimination of Acc. Instead, the proof of consistency roughly proceeds by dichotomy on whether the image of a set by a functional relation is sufficiently bounded. If it is, the set can be constructed, thus establishing the Axiom of Replacement and the consistency of ZF; otherwise the ranks of the sets show that V_alpha for their limit alpha is already a model of ZF. This is an amusing trick in that it answers the question in presence of LEM, but doesn’t shed any light on the relationship between Unique Choice and Replacement (or stronger type-theoretic choice principles and Collection).