"For any" is universal quantification, which translates into dependent function types. As an example, let's take the following theorem: For any natural number n greater than zero, there exists a natural number m, such that S(m) = n.
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality
theorem : (n : ℕ) → 0 < n → Σ[ m ∈ ℕ ] (suc m ≡ n)
theorem zero ()
theorem (suc n) _ = n , refl
We can rewrite your theorem using the same pattern:
theorem : {A B : Set} (f : A → B) {m n : ℕ} →
A has-size m → B has-size n → n < m →
Σ[ a ∈ A ] Σ[ a′ ∈ A ] (a ≢ a′ → f a ≡ f a′)
This is a bit more involved: for any sets A
and B
, any function f
from A
to B
and any natural numbers m
and n
such that A
has m
and B
has n
elements and m
is greater than n
, there exist elements a
and a′
in A
such that even if a
is different from a′
, f a
is equal to f a′
. Note that I cut the b
element; it's still the same theorem but a bit easier to write down.
_has-size_
remains to be defined. I suggest defining A has-size m
to be the statement that A
is isomorphic to Fin m
(Fin
can be found in Data.Fin
). If your assumptions are that A
is isomorphic to Fin m
and B
to Fin n
, you can do the proof on numbers (which is far easier) and then transform those numbers back to elements of A
or B
.
As for your second question:
C-c C-n reverse (1 ∷ 2 ∷ 3 ∷ [])
gives back
3 ∷ 2 ∷ 1 ∷ []
You might have tried to write the list as [1, 2, 3]
as you would in Haskell, but this shortcut is not present in Agda. With clever use of operators, you could probably make it sort of work, though it would certainly require more whitespace (such as [ 1 , 2 , 3 ]
), but I don't think it's worth the effort.