quotients-and-lifts

Use Quot.lift with a representative function f : A → B and a respect proof hf showing that f preserves the equivalence relation. Quot.lift constructs a well-defined function from the quotient by ensuring equal representatives map to equal values.

A respect proof hf : ∀ a b, r a b → f a = f b verifies that your function f respects the quotient relation r. Without it, Quot.lift cannot guarantee the function is well-defined on equivalence classes.

Quot.ind enables induction on quotient types by letting you prove properties hold for all quotient elements via their representatives. You prove the property for a representative and show it respects the underlying relation.

Use Quot.sound when you need to prove two quotient elements are equal by showing their representatives are related by the quotient relation r. Quot.sound converts proofs of r a b into proofs that ⟦a⟧ = ⟦b⟧.

Yes, nested Quot.lift patterns are supported in ComputationalPaths code. When lifting through multiple quotient layers, ensure each inner lift respects its relation and compose the respect proofs correctly, paying attention to relation direction and symmetry.

Standard obligations include constructing respect proofs for Quot.lift, discharging equivalence properties to apply Quot.sound, and handling nested lift patterns in computational paths. ComputationalPaths encodings like LoopQuot and circle require symmetry awareness for correct relation direction.