Type theory via exact categories