Revision as of 01:24, 30 March 2017 edit 24.85.232.10 (talk) No edit summary ← Previous edit		Revision as of 10:09, 10 February 2018 edit undo 14.155.90.195 (talk) No edit summary Next edit →
Line 68: [http://www.cse.chalmers.se/~peterd/papers/inductive.html A list of Peter Dybjer's publications on induction and induction-recursion] [http://www.cs.swan.ac.uk/~csetzer/slides/dybjer60thBirthdayGothenburgJune2013/dybjer60thBirthdayGothenburgJune2013.pdf Slides covering Induction-Recursion and its derivatives] * 1337777.OOO : ''limit objects depend on morphisms , BUT THIS DEPENDENCE NEED-NOT BE GRAMMATICAL !'' , https://github.com/1337777/cartier/blob/master/cartierSolution3.v [[Category:Type theory]]

Induction-recursion: Difference between revisions