Oh, I have a war story. I have many war stories. Strap in.

Last month I was formalizing a result about free commutative monoids in Agda (standard library setoids). The underlying type was List A quotiented by bag equality. "How hard can it be," I said. "It's just lists," I said.

-- What I thought I was doing:
BagEq : {A : Set} → List A → List A → Set
BagEq xs ys = ∀ a → count a xs ≡ count a ys

-- What I ended up doing for three days:
module BagSetoid where
  -- Prove reflexivity. Fine.
  -- Prove symmetry. Annoying but OK.
  -- Prove transitivity. My paws hurt.
  -- Prove append is Proper. OK.
  -- Prove map is Proper. Wait, the function also needs to be a setoid morphism?
  -- Prove map is Proper for setoid morphisms. Blood pressure rising.
  -- Prove concatMap is Proper. I need to lie down.
  -- Prove foldr is Proper. Please send help.

Three days. Three days to get a halfway-usable interface for "lists, but unordered." In HoTT with HITs this would be like, 15 lines. The FMSet HIT from the HoTT book just gives you commutativity as a path constructor and you're done.

The real killer is when you want to rewrite under a binder. Suddenly nothing works and you have to construct the entire transport manually and—

Coping strategy #1 that I've actually found useful: setoid rewriting via Setoid.rewrite / setoid_rewrite tactic in Coq, combined with pre-registering Proper instances. It doesn't fix the root problem but it makes the day-to-day pain much more bearable.

(* Register once, rewrite forever (sort of) *)
Add Parametric Morphism : my_fun
  with signature my_eq ==> my_eq ==> my_eq
  as my_fun_morphism.
Proof. (* ... *) Qed.

(* Now setoid_rewrite actually works! Sometimes! *)
Goal forall x y, my_eq x y → my_eq (my_fun x x) (my_fun y y).
Proof.
  intros x y H. setoid_rewrite H. reflexivity.
Qed.

The catch is that setoid_rewrite fails silently in weird ways if the Proper instances don't perfectly match the syntactic form of your goal. See my dedicated thread about setoid_rewrite mystery failures for a catalog of suffering.

Coping strategy #2: use refinement types via { x : T | P x } when you can get away with it. Avoids the full setoid machinery if your equivalence is just "same normal form." Doesn't compose well but hey.

Re: QITs — they're essentially HITs truncated to be sets (h-sets). The difference from plain quotient types is that you can have infinitely many constructors specified simultaneously with their equality conditions. This is super useful for defining things like:

• Cauchy reals (as a QIT, not a setoid — no more carrying ℕ → ℚ everywhere)
• Type-theoretic syntax / intrinsically-typed terms with substitution laws built in
• Free algebraic structures with their equations

-- QIT example: integers as a quotient of (ℕ × ℕ, diff-eq)
-- Instead of setoid: (ℕ × ℕ, λ (a,b) (c,d) → a+d = b+c)

data ℤ-QIT : Set where
  diff   : ℕ → ℕ → ℤ-QIT           -- n - m
  cancel : ∀ n m k →
    diff (n + k) (m + k) ≡ diff n m  -- (n+k)-(m+k) = n-m
  isSet  : isSet ℤ-QIT

-- The cancel constructor IS the setoid relation, baked into the type.
-- No external ≈ to carry. No Proper instances. Beauty.

The isSet constructor (from the HoTT book Ch. 6) truncates the HIT to a set so you don't have to worry about higher paths. This is what distinguishes QITs from general HITs.

See the Altenkirch-Kaposi QIIT paper for the general theory. It's a bit dense but worth it. We have a reading group thread here too.

Hot take: the true villain of setoid hell isn't the setoids themselves. It's the lack of a quotient type eliminator that the compiler verifies. With setoids, the invariant "all functions must respect ≈" is a social contract enforced by shame, not a type-level guarantee.

I once spent 6 hours debugging a proof that should have been true before realizing I had defined a function that didn't actually respect my equivalence relation. The type checker was fine with it! Because of course it was — from the type checker's perspective, I just defined a function carrier → carrier that happened to use the wrong element of an equivalence class.

This is also why the Lean 4 approach of Quot.lift + Quot.sound as primitives is so much nicer. You literally cannot define a function on a quotient without proving it well-defined at definition site. No forgetting, no 2am bugs. Discuss: is this worth the other limitations of Lean's quotient axiom approach?

See also: Lean 4 Quotient Primitives — a love letter

@QuotientQueen what you've discovered is the category of setoids, which is actually a perfectly fine and well-studied mathematical object! Setoids and setoid morphisms form a category (technically a locally small one). The name for what you're in is:

✨ Setoid Hell, Layer ω ✨

More precisely: you're building the internal category of setoids within type theory, which requires exactly this tower of morphism-setoids. This is actually the mathematical foundation of Bishop-style constructive mathematics. It's not a bug, it's the intended experience.

The "is there a better way" answer is: yes, and it's called an exact completion. You can formally "complete" a category with the setoid construction to get a category with quotients. But doing this inside a proof assistant without native quotients is left as an exercise to the suffering reader.

See: Bishop-style constructivism in proof assistants and exact completions in type theory.