#### Exercise `Any-∃` Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`. Не говоря уже о том, что ∃[ x ∈ xs ] P x даже не допустимого синтаксиса - допустимым может быть только Σ[ x ∈ xs ] P x , ни одна из сигнатур типа, которые я...

postulate extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) ----------------------- → f ≡ g Я знаю, что приведенное выше определение является последовательным, но что, если его немного изменить?...