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

[Thorsten Altenkirch]

On 14/05/2015 10:54, "Andrew Pitts" <Andrew.Pitts at cl.cam.ac.uk> wrote:

>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...

A QIT is a higher inductive type which has only level-1 constructors and
which is forced to be an hSet (this is actually a level 2 constructor).

>
>> 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?

The simplest example is to consider infinitely branching trees

data T0 : Set where
	leaf : T0
	node : (Nat -> T0) -> T0

Which we want to quotient up to permutations

data _~_ : T0-> T0 -> Set where
	leaf : leaf ~ leaf
 	perm : (g : Nat -> T0)(f : Nat -> Nat) -> isIso f -> node g ~ node (g o
f)

Hence we define


T : Set
T = T0 / _~_


But now we want to lift node to T

nodeT : (ℕ -> T) -> T

That is it should satisfy that nodeT ([_] o f) = [ node f ] where f : Nat
-> T0 and [_] : T0 -> T is the class constructor.

At this point it is instructive to do it for binary trees and observe that
to lift node you have to sequence the eliminator for quotients. However,
this is not possible for T.

However, this is no problem for QITs:

data T' : Set where
  	leaf : T'
	node : (Nat -> T') -> T'
	perm : (g : Nat -> T')(f : ℕ -> ℕ) -> isIso f -> node g == node (g ∘ f)


Note that I am not claiming that T’ is T, but that T’ is what we want.
Also to avoid complications _~_ should be propositional, and I am
implicitly adding is-h-set T’ as a constructor.

One way to fix this problem is to assume countable choice. The nice thing
about QITs is that you don’t need countable choice.

In the HoTT ook QITs are used to define Cauchy reals so that they are
Cauchy complete. If you just use quotients you need countable choice for
this. This is also used when defining the constructible Hierarchy, that is
Aczels encoding of sets as trees in type theory, We want to quotient by
extensionality but we also want to be able to lift comprehension to the
quotiented trees. Again this needs choice (not just countable) but can be
done with QITs easily.

Thorsten










	




>
>Best wishes,
>
>Andy





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.