A setoid is a type with a distinguished equivalence relation, denoted ≈. This is mainly used as input to the Quotient type constructor.

Instance Constructor

Setoid.mk.{u}

Methods

r : α → α → Prop

iseqv : Equivalence Setoid.r

Equivalence according to some canonical equivalence relation for a type is written using ≈, which is overloaded using the type class HasEquiv.

term ::= ...
    | `x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `≈` in identifiers is `equiv`.term ≈ term

HasEquiv α is the typeclass which supports the notation x ≈ y where x y : α.

Instance Constructor

HasEquiv.mk.{u, v}

Methods

Equiv : α → α → Sort v

An equivalence relation ~ : α → α → Prop is a relation that is:

• reflexive: x ~ x

• symmetric: x ~ y implies y ~ x

• transitive: x ~ y and y ~ z implies x ~ z

Equality is an equivalence relation, and equivalence relations share many of the properties of equality. In particular, Quot α r is most well behaved when r is an equivalence relation, and in this case we use Quotient instead.

Constructor

Equivalence.mk.{u}

Fields

refl : ∀ (x : α), r x x

symm : ∀ {x y : α}, r x y → r y x

trans : ∀ {x y z : α}, r x y → r y z → r x z

Let α be any type, and let r be an equivalence relation on α. It is mathematically common to form the "quotient" α / r, that is, the type of elements of α "modulo" r. Set theoretically, one can view α / r as the set of equivalence classes of α modulo r. If f : α → β is any function that respects the equivalence relation in the sense that for every x y : α, r x y implies f x = f y, then f "lifts" to a function f' : α / r → β defined on each equivalence class ⟦x⟧ by f' ⟦x⟧ = f x. Lean extends the Calculus of Constructions with additional constants that perform exactly these constructions, and installs this last equation as a definitional reduction rule.

Given a type α and any binary relation r on α, Quot r is a type. Note that r is not required to be an equivalence relation. Quot is the basic building block used to construct later the type Quotient.

Given a type α and any binary relation r on α, Quot.mk maps α to Quot r. So that if r : α → α → Prop and a : α, then Quot.mk r a is an element of Quot r.

See Quot.

Given a type α, any binary relation r on α, a function f : α → β, and a proof h that f respects the relation r, then Quot.lift f h is the corresponding function on Quot r.

The idea is that for each element a in α, the function Quot.lift f h maps Quot.mk r a (the r-class containing a) to f a, wherein h shows that this function is well defined. In fact, the computation principle is declared as a reduction rule.

Given a type α and any binary relation r on α, Quot.ind says that every element of Quot r is of the form Quot.mk r a.

See Quot and Quot.lift.

The quotient axiom, or at least the nontrivial part of the quotient axiomatization. Quotient types are introduced by the init_quot command in Init.Prelude which introduces the axioms:

opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u

opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r

opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
  (∀ a b : α, r a b → f a = f b) → Quot r → β

opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
  (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q

All of these axioms are true if we assume Quot α r = α and Quot.mk and Quot.lift are identity functions, so they do not add much. However this axiom cannot be explained in that way (it is false for that interpretation), so the real power of quotient types come from this axiom.

It says that the quotient by r maps elements which are related by r to equal values in the quotient. Together with Quot.lift which says that functions which respect r can be lifted to functions on the quotient, we can deduce that Quot α r exactly consists of the equivalence classes with respect to r.

It is important to note that r need not be an equivalence relation in this axiom. When r is not an equivalence relation, we are actually taking a quotient with respect to the equivalence relation generated by r.

Quot.liftOn q f h is the same as Quot.lift f h q. It just reorders the argument q : Quot r to be first.

Dependent induction principle for a quotient, when the target type is a Subsingleton. In this case the quotient's side condition is trivial so any function can be lifted.

Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

• Quot.lift, for nondependent functions

• Quot.ind, for theorems / proofs of propositions about quotients

• Quot.recOnSubsingleton, when the target type is a Subsingleton

• Quot.hrecOn, which uses HEq (f a) (f b) instead of a sound p ▸ f a = f b assummption

Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

• Quot.lift, for nondependent functions

• Quot.ind, for theorems / proofs of propositions about quotients

• Quot.recOnSubsingleton, when the target type is a Subsingleton

• Quot.hrecOn, which uses HEq (f a) (f b) instead of a sound p ▸ f a = f b assummption

Heterogeneous dependent recursion principle for a quotient. This may be easier to work with since it uses HEq instead of an Eq.ndrec in the hypothesis.

Squash α is the quotient of α by the always true relation. It is empty if α is empty, otherwise it is a singleton. (Thus it is unconditionally a Subsingleton.) It is the "universal Subsingleton" mapped from α.

It is similar to Nonempty α, which has the same properties, but unlike Nonempty this is a Type u, that is, it is "data", and the compiler represents an element of Squash α the same as α itself (as compared to Nonempty α, whose elements are represented by a dummy value).

Squash.lift will extract a value in any subsingleton β from a function on α, while Nonempty.rec can only do the same when β is a proposition.

The canonical quotient map into Squash α.

If β is a subsingleton, then a function α → β lifts to Squash α → β.