Hi list, Most CT books have lots of elementary exercises whose solutions consist of defining morphisms, functors, natural transformations, etc, and doing calculations with them and proving things. Is there a "canonical language" for solving those exercises? Here's why I am asking. I am giving a course without any formal prerequisites that is mostly an introduction to lambda-calculus, intuitionistic propositional logic, and CT, and the students - most of them have very little mathematical background - have a lot of difficulty when they have to write down answers of exercises... the way that I found to keep them from spending far too much time on trying different ways of writing was to convince them to use untyped lambda-calculus to define things whenever possible, but that feels a bit like cheating... So, here are some question for the people who have taught very basic courses on CT: how did you teach your students to write? And what resources did you use? Cheers and thank in advance =), Eduardo Ochs [For admin and other information see: http://www.mta.ca/~cat-dist/ ]