`{Funext} (σ : Signature) : PreCategory. Proof. apply (@Build_PreCategory (SetAlgebra σ) Homomorphism hom_id (@hom_compose σ)); [intros; by apply path_hset_homomorphism .. | exact _]. Defined.
Require Import Import Morphisms.CategoryMorphismsNotations isomorphic_notations.