proposition: Theorem is_isomorphism_second_isomorphism : IsIsomorphism hom_second_isomorphism.
proof: Proof. intro s. apply isequiv_surj_emb; exact _. Qed.
imports: HSet Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra