Add an alternative definition of Kuratowski-finiteness using listed

[ayberkt]

In module MLTT.List, there is a notion called listed.

TypeTopology/source/MLTT/List.lagda

Lines 101 to 102 in d8e2220

	listed : Type → Type
	listed X = Σ xs ꞉ List X , ((x : X) → member x xs)

The propositional truncation of this should be equivalent to Kuratowski-finiteness. Proving this might be a fun exercise, but will involve some bureaucracy regarding the Fin type.