fact: Record Homomorphism {σ} {A B : Algebra σ} : Type := BuildHomomorphism { def_hom : ∀ (s : Sort σ), A s → B s ; is_homomorphism_hom : IsHomomorphism def_hom }.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics