Notation for quotient types.

Stream: general

[Miguel Marco]

Very quick question: Given a Type X : Type and R : Setoid X, is there a notation to represent Quotient R as X / R (or something similar)?

[Oliver Nash]

Yes but you need to use a funny unicode slash ⧸ which is not the same as /. See for example the source of docs#QuotientGroup.Quotient.group