proposition: Lemma precategory_algebra `{Funext} (σ : Signature) : PreCategory.
proof: Proof. apply (@Build_PreCategory (SetAlgebra σ) Homomorphism hom_id (@hom_compose σ)); [intros; by apply path_hset_homomorphism .. | exact _]. Defined.
imports: HoTT.Types HoTT.Categories.Category.Core HoTT.Categories.Category.Univalent HoTT.Classes.theory.ua_isomorphic