<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:Calibri
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><div>Hi,</div><div><br></div><div>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.</div><div><br></div><div>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).</div><div><br></div><div>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.</div><div><br></div><div>My question:</div><div>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?</div><div><br></div><div>Locally cartesian closed categories provide models for extensional type theory. What about opposites of lccc's?</div><div><br></div><div>/LL</div><div><br></div> </div></body>
</html>