proposition: Lemma is_isomorphism_inc_improper_subalgebra (improper : ∀ s (x : A s), P s x) : IsIsomorphism hom_inc_subalgebra.
proof: Proof. intro s. refine (isequiv_adjointify _ (λ x, (x; improper s x)) _ _). - intro x. reflexivity. - intro x. by apply path_sigma_hprop. Qed.
imports: HoTT.HProp HoTT.Types HoTT.Classes.theory.ua_homomorphism