I don't understand these things you wrote:

On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote:

Interestingly it seems that QITs are more expressive then quotients (which can be encoded impredicatively).

And as I said above, QITs are an interesting extension which in some instances avoids appealing to the axiom of choice.

Like, in a constructive, predicative system without any choice principles, and where quotients are not expressed as QITs, is there an expressiveness difference? (I'm thinking of Computational Type Theory, for example.)