Is it possible to encode QIITs using only inductive types and quotients

PhD meeting 20251002 (Thorsten): There appears to be an argument against this, implying that quotients are not a conservative extension in this context.

See Universal QIIT.