Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory