Nuprl Definition : quotient

The quotient type allows us to change the equality for members of a type A
to a given equivalence relation B(x,y).
It is a special case of the more general pertype.

When B(x,y) is the trival equivalence relation True, then we display
the quotient x,y:A//B as ⌜⇃(A)⌝. We call this the "half squash" of A
since it retains the members of A but "squashes" the equality in A.⋅

x,y:A//B[x; y] == pertype(λx,y. ((x ∈ A) ∧ (y ∈ A) ∧ B[x; y]))

Definitions occuring in Statement : pertype: pertype(R), and: P ∧ Q, member: t ∈ T, lambda: λx.A[x]
Definitions occuring in definition : pertype: pertype(R), lambda: λx.A[x], and: P ∧ Q, member: t ∈ T
Rules referencing : StrongContinuity2

Latex:
x,y:A//B[x; y] == pertype(\mlambda{}x,y. ((x \mmember{} A) \mwedge{} (y \mmember{} A) \mwedge{} B[x; y])) Date html generated: 2017_09_29-PM-05_47_56 Last ObjectModification: 2015_12_22-PM-04_13_22 Theory : per!type!1 Home Index