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

[Lars Lindqvist]

Hi,
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.
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)).
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.
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.
So the sum in the coinductive introduction rule correspond to the product in the inductive elimination rule.
/LL

 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151026/13ea0e44/attachment.html