Add code for generating and working with quotients

[WhatisRT]

This adds some generic code for dealing with (extensional) quotients

[clayrat]

I'm not sure where are you using Singleton, but there's an interface for such things in contrib: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Interfaces/Proposition.idr

[WhatisRT]

Oh, Singleton is a leftover from a previous try. Good to know that Proposition is a thing!

[fredrikNordvallForsberg]

One thing that could be nice would be to do the right %access incantations in UnsafeQuotient so that the commuting triangle in exists would commute pointwise.

It might also be worth it to split up the dependent pair in exists into two fields in the record, since this is the way to define functions out of the quotient.

[fredrikNordvallForsberg]

Should this module use %access public export?

[WhatisRT]

Good point, forgot that.

[fredrikNordvallForsberg]

Suggested change

	(\y, f, g, h, a => trans (cong $ wrapUnwrapId a) (sym $ h $ unwrap a))
	(\y, f, g, h, (InternalWrap a) => sym $ h a)

[WhatisRT]

I find these things very weird. In the previous line where I use unwrap, I cannot pattern match in the lambda, while in this line I can. The only reason why unwrap exists is because it didn't work there for me. Do you or @clayrat have any insight as to what might be the issue there?

[fredrikNordvallForsberg]

As for the dependent pair, do you mean that it would be nicer if we didn't have to write fst $ exists ...? In that case, I'd just define another function.

Concretely, I suggest to replace the exists field with the following two fields (possibly with better chosen names):

  extension : (y : Type) -> (f : RespectingMap x y eq)
           -> carrier -> y
  commutes : (y : Type) -> (f : RespectingMap x y eq)
          -> extEq (fst f) (extension y f . (fst proj))

Why?

1. Most of the time, the function extension y f is probably what you want easy access to (what I tried to say above).
2. Should make it easier to build things stepwise using holes, because Idris doesn't need to juggle sigma types and first projections etc.
3. Might make it easier to talk about the code, e.g. 'the commuting triangle in exists' above is the commutes field.

I'm not sure what you mean by 'the commuting triangle in exists would commute pointwise'.

What I meant was that in the Quotients.Unsafe module, the proof of commutes y f a is Refl for every a, which is nice, but outside this module, nothing reduces anymore.

[fredrikNordvallForsberg]

Probably best not to export unwrap, as it corresponds to a form of global axiom of choice?

[WhatisRT]

Oh, completely missed that.

[WhatisRT]

I'm not sure what you mean by 'the commuting triangle in exists would commute pointwise'.

As for the dependent pair, do you mean that it would be nicer if we didn't have to write fst $ exists ...? In that case, I'd just define another function.