[Agda] coinductively defined families

[Thorsten Altenkirch]

I would assume this as the default by now. Intensional equality for infinite objects is just wrong.

Ok, the implementation is a bit behind but we don’t take every bug as a principle, do we?

Thorsten

On 08/03/2018, 11:09, "Agda on behalf of Henning Basold" <agda-bounces at lists.chalmers.se on behalf of henning at basold.eu> wrote:

    Instead, one needs a
    type theory, in which bisimilarity would be included in the
    propositional equality (observational type theory any one?).




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 contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.