{σ : Signature} {A B : Algebra σ} (f : ∀ s, A s → B s) `{IsIsomorphism σ A B f} : ∀ (s : Sort σ), A s <~> B s. Proof. intro s. rapply (Build_Equiv _ _ (f s)). Defined.
Require Import Import algebra_notations ne_list.notations.