[Agda] Quotient types in Agda, if you Trust Me

[Andrew Pitts]

On 14 May 2015 at 10:33, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> Just a general remark: if we just want to have hsets we know how to
> implement this so that canonicity holds based on our work on Observational
> Type Theory. Conor and his team went some way to do when working on
> Epigram 2, which alas never was finished.
>
> At some point we discussed adding this to Agda at an AIM. One problem is
> that you can¹t just allow pattern matching on inductive families which
> implicitly use equality, i.e. which repeat variables (such as
> propositional equality itself).
>
> Maybe we should revisit this.

quotient.agda is of course a quick-and-dirty hack intended to allow
use of quotients in Agda right now. But I am really a slow-and-clean
person myself (really), so I certainly second your comment.

> However, it would be good to do this in a
> way which is compatible with future extensions to capture HoTT properly.
>
> Also we should¹t just have quotient types but 1st order HITs (I call the
> quotient-inductive types or QITs).

Can you say what the specification of QITs is? And...

> There are a number of applications
> where QITs are essential and they generalise quotient types. E.g. This is
> used to formalise the Reals in the book

[the book = the Homotopy Type Theory book (needs saying since this is
a thread on the Agda mailing list, not the HoTT mailing list)]

> and Ambrus and I are working on Type Theory in Type Theory based on this.

...is there a small example to illustrate the limitation of quotients types?

Best wishes,

Andy