proposition: Theorem is_isomorphism_third_isomorphism : IsIsomorphism hom_third_isomorphism.
proof: Proof. unfold hom_third_isomorphism. destruct path_quotient_algebras_third_surjection. exact _. Qed.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism