(improper : ∀ s (x : A s), P s x) : IsIsomorphism hom_inc_subalgebra. Proof. intro s. refine (isequiv_adjointify _ (λ x, (x; improper s x)) _ _). - intro x. reflexivity. - intro x. by apply path_sigma_hprop. Qed.
Require Import Import algebra_notations ne_list.notations. Import subalgebra_notations.