Excuse me that this time I flood the mailing list with questions. I have read "Classical Mathematics for a Constructive World", by Russell O’Connor, http://arxiv.org/pdf/1008.1213 Does someone implemented part of the paper in Agda? Thanks, Peter