Transport is key

[sassa_nf]

transport : forall {A : Set} {B : A -> Set} {x y : A} -> x == y -> B x -> B y
transport refl bx = bx

can be used to prove congruence and commutativity.

cong : forall {A B : Set} {x y : A} -> (f : A -> B) -> (x == y) -> (f x) == (f y)
cong {x = x} f xy = transport {B = (\y -> (f x) == (f y))} -- just making explicit that B is a type (f x) == (f _)
                              xy refl -- this refl is of type (f x) == (f x), which gets transported along x == y to (f x) == (f y)

-- commutativity of _==_
comm : forall {A : Set} {x y : A} -> x == y -> y == x
comm {x = x} xy = transport {B = (_== x)} xy refl  -- this refl is of type x == x, which gets transported along x == y to y == x

(The whole thing about proving the properties of adding odds and evens: https://stackoverflow.com/a/56512565/1935631)