Small updates

Completed antipode proof in TK-duality, added proof of compatibility
counit and antipode