Implement observational type theory