We discussed some questions related to inverses and composition, e.g. if f composed with g is the identity, does it follow that f is bijective ? Or that g is an inverse of f if f was already bijective ? What if we consider g composed with f instead ? Proofs for these facts can sometimes be found by "following the types", i.e. there is only one step one can take, and the result just follows automatically.
We saw very small counter-examples (e.g functions with domains and codomains having one or two elements), which are usually easier to deal with than more complicated functions, like functions on the integers or the reals.
The question of whether these kind of proofs should usually go by contradiction was raised. Arguments by contradiction are very often not necessary (sometimes you really need them though)! I think they should be avoided when possible, as they tend to "add negations everywhere", and hence make the proof more complex. Of course, it is never logically wrong to work by contradiction, but it makes it easier to make a mistake...
Whenever you write a proof by contradiction, try to read your proof again and think about whether it was really necessary to use contradiction.