Ratwa Research Ability Training with Agda in Sun Yat-sen University. Plan & Progress Insertion Decidable conversion from/to List.Any Permutation Setoid Decidable Sorting QuickSort Permutation Monotone