[Agda] Coinductive types and 'duals' to dependent lambda calculus?

[Thorsten Altenkirch]

Hi Lars,

Dependent recursion generalizes induction, which says that any subset of the inductive set which is closed under constructors is already the whole set. Dually coinduction says that any equivalence relation which is closed under destructors is the equality. Equivalence relation are dual to subsets in the sense that subsets classify monos into the type while equivalence relations classify epis going out of the type.

Usually equivalence relations are proof-irrelevant but in the light of Homotopy Type Theory they don’t need to be. Maybe this would be a good start towards a more symmetric account of the induction/coinduction duality.

Thorsten

From: Lars Lindqvist <l_lindqvist at hotmail.com<mailto:l_lindqvist at hotmail.com>>
Date: Sunday, 25 October 2015 15:35
To: "agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>>
Subject: [Agda] Coinductive types and 'duals' to dependent lambda calculus?

Hi,

This question is not really related to agda directly but since there is a lot of knowledge about coinductive data types in this forum I hope it is ok anyway. I am just an interested hobbist by the way so there is a lot of hand-waving in the question below.

In dependent type theory you can form dependent types like (a:A)B(a) and an object of this type can be interpreted as a proof that every object of type A have property B. When A is an inductive type you use the elimination rule of A to construct an object of type (a:A)B(a).

For a coinductive type C one would(?) expect to use the introduction rule of C to construct a term of type D(c)(c:C). A term of this type would be a proof that property D (an invariant) always gives rise to a process of type C. Or in other words: All behaviours of D can be covered by behaviours of C in a productive way.

My question:
Are my expectations for the coinductive case above just nonsense? I have been looking for papers about 'duals' to dependent type theory but have not found much. Is there some fundamental flaw in the above thinking?

Locally cartesian closed categories provide models for extensional type theory. What about opposites of lccc's?

/LL





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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151028/8ff78f70/attachment.html