<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;">
<div>Hi Lars,</div>
<div><br>
</div>
<div>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. </div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>Thorsten</div>
<div><br>
</div>
<span id="OLK_SRC_BODY_SECTION">
<div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt">
<span style="font-weight:bold">From: </span>Lars Lindqvist <<a href="mailto:l_lindqvist@hotmail.com">l_lindqvist@hotmail.com</a>><br>
<span style="font-weight:bold">Date: </span>Sunday, 25 October 2015 15:35<br>
<span style="font-weight:bold">To: </span>"<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>
<span style="font-weight:bold">Subject: </span>[Agda] Coinductive types and 'duals' to dependent lambda calculus?<br>
</div>
<div><br>
</div>
<div><style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:Calibri
}
--></style>
<div 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>
</div>
</div>
</span>
<PRE>
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.
</PRE></body>
</html>