The Coq mailing list

[Neelakantan Krishnaswami <n.krishnaswami AT cs.bham.ac.uk>]

On 25/09/15 13:35, Ilmārs Cīrulis wrote:
> I often have to use Equivalence and Proper (while tinkering around),
> therefore a question appeared:
>
> What about Coq (or any other proof assistant / type theory) where
> setoids and morphisms are first class citizens (built in, replacing
> standard Type and function that becomes something like lower level of
> language). In such case there would be no need of special libraries for
> Equivalence, Setoid and related libraries for, e.g., lists or other data
> structures that respects equivalence.
>
> What are cons of such idea?

This is essentially the idea behind Observational Type Theory; you
should look at:

* Extensional Equality in Intensional Type Theory. T. Altenkirch
  LICS 1999
* Observational equality, now! T. Altenkirch, C. McBride, W. Swierstra,
  PLPV 2007

The core idea (every type is a setoid and every definable term is a
equality-respecting morphism) is very simple, but making all the syntax
line up to make it work is tricky and intricate.

Best,
Neel