Yes, my understanding is that quotients should be much more convenient to use than setoids. Univalance means you can more or less ignore equality in the quotien

Yes, my understanding is that quotients should be much more convenient to use than setoids. Univalance means you can more or less ignore equality in the quotient after you define it---proofs should just be transportable.