tag:blogger.com,1999:blog-3679812208800765969.post6510788170721867089..comments2012-05-25T17:36:44.028-07:00Comments on monoidal: Descending the level ladderghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-3679812208800765969.post-68381641006396956172012-04-19T16:50:12.045-07:002012-04-19T16:50:12.045-07:00I agree, I think it is not possible. At the very l...I agree, I think it is not possible. At the very least, * should be changed to a kind for natural numbers.ghttps://www.blogger.com/profile/04686862403622560424noreply@blogger.comtag:blogger.com,1999:blog-3679812208800765969.post-23926516979029684952012-04-19T07:10:06.801-07:002012-04-19T07:10:06.801-07:00It is possible to write the term
com :: forall (m...It is possible to write the term<br /><br />com :: forall (m :: *) (n :: *). Equal (Add m n) (Add n m)<br /><br />?<br /><br />I don't see how to use induction in your scenario.Andrés Sicard-Ramírezhttps://www.blogger.com/profile/10605871537627808332noreply@blogger.com