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

[Lars Lindqvist]

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
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151025/5e755c0b/attachment.html