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

[Andreas Abel]

Hello Lars,

On 25.10.2015 15:35, Lars Lindqvist wrote:
> 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.

If the output c:C is constructed from the input D(c), then somehow one 
would rather expect the usual dependency (d:D) -> C(d).  However, at 
least in coinductive logic programming, one could imagine a predicate on 
(c:C)xD(c) which could maybe be interpreted in an algorithmic way such 
that d is the input and c the output.

Do you have an example that can illustrate your point?  (Examples are 
usually a tremendous help to clarify the theory.)

Cheers,
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/