Nuprl Definition : quotient

The quotient type allows us to change the equality for members of type A
to given equivalence relation B(x,y). 
It is 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 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

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