<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>I am very far from any theory. My question just derives from basic observations of initial T-algebras and final T-coalgebras. Dependent type theory seems to fit initiality well and dual dependent type teory (whatever that is) seems to fit finality well. I do not have much knowledge about homotopy type theory I am afraid.</div><div><br></div><div>To construct a term of type (a:A)B(a) where A is inductive you use the elimination rule of A. Then you use the introduction rules of B to fill in the cases in the elimination rule. When A=N the cases are B(zero) and (b:B(n))B(succ(n)).</div><div><br></div><div>To construct a term of type D(c)(c:C) where C is coinductive you use the introduction rule of C to cover the eliminators of D. By cover here I mean the dual of filling in the cases in the inductive elimination rule above.</div><div><br></div><div>For example consider T(X)=1+X. As initial T-algebra you get N and as final T-coalbegra you get P, possibly terminating processes with eliminators stop and next:P(P). The introduction rule for P would then be some kind of sum of Q:Set(P), casestop:Q(stop), casenext:Q(next(p))(Q(p)) and these might be used to cover the eliminators of Q. So if the only behaviour of R:Set(P) is R(next(p))(R(p)) this nonterminating behaviour can be covered by casenext with Q=R.</div><div><br></div><div>So the sum in the coinductive introduction rule correspond to the product in the inductive elimination rule.</div><div><br></div><div>/LL</div><div><br></div><div><br></div> </div></body>
</html>