Is there a "model-independent reason" why a levelwise-invertible natural transformation of $\infty$-functors is invertible? In the quasicategory model, this follows from the fact that the inclusion from $\Delta[1]$ to the walking iso is an anodyne extension, but this feels unenlightening to me...

I suppose you need to couple that with the fact that the inclusion of the maximal Kan subcomplex of a quasicategory is full on 2-cells and higher.

@TimCampion I don't know something precise, but morally, I think this holds because inverses are unique up to a contractible space of choices.

@PhilTosteson Sure, and basically that idea is straightforward to turn into an actual proof in the 1-categorical case. But in the $\infty$-categorical case it's not so clear to me...

Actually the reasoning I gave above doesn't work. So I'm back to not even knowing a proof at all.

I'm having trouble finding this in HTT, although 2.2.3.6 shows something similar for categories of left fibrations.

as opposed to functor categories