idris-ct

idris-ct copied to clipboard

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

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

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

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.