Surjective quotients lead to classical logic
	deleted:    Paradox.agda
	new file:   SurjectiveQuotients.agda