People, I observe in Relation.Unary.agda : -- The singleton set. {_} : A → Pred A a Is this strange symbol intended for the name? Also type-checking my project sometimes breaks by segmentation fault, and it improves after restarting Linux. (I suspect that something is corrupted in the emacs mode or in files, or in the hardware). Thanks, ------ Sergei