fact: Record Isomorphic {σ : Signature} (A B : Algebra σ) := BuildIsomorphic { def_isomorphic : ∀ s, A s → B s ; is_homomorphism_isomorphic : IsHomomorphism def_isomorphic ; is_isomorphism_isomorphic : IsIsomorphism def_isomorphic }.
imports: HoTT.Classes.theory.ua_homomorphism HoTT.Types HoTT.Tactics