Copy type checking function as a preparation for bidirectional type checking.
Something like this?
Push/pull through position information.
Actually call the bidirectional type checker.
Stuck in push rule for applications.
WIP
Typechecking now actually fails for (some?) terms that do not type check.
It fails, pretty. Ha! :-)

Abstraction case of push checking.
Fix push typechecking of lambda abstractions.
Merge reorganisation stuff.
TypecheckPull Int and IntOp.
TypecheckPull if0.
TypecheckPull Pi. TypecheckPull should be finished now.
TypecheckPush application.

I wonder why Pierce does this:

f pull A -> B     x push A
--------------------------
        f x push B

instead of this:

x pull A     f push A -> B
--------------------------
        f x push B

Anyway, I implemented Pierce's.
TypecheckPush IntOp.

Also a question about IfZero. I'm totally confused about dependent types it seems...
Finish bidirectional type checking. On to debugging it.
Fix push application. Also use proper debug logging function for push checking.
A couple of examples that demonstrate simple functions.
Add functions examples to the test suite.
Test (not actually working) a bug in the typechecker. A fix for that is coming up.