On 09/03/13 09:03, Andreas Abel wrote: > One the way, one would probably identify the fragment of Agda which is > justifiable in MLTT. Yes, this is what I think would be useful. Also, simply "justifiable" (omitting MLTT) would be good too. Best, Martin