Algebra σ := BuildAlgebra carriers_subalgebra ops_subalgebra. Global Instance trunc_subalgebra {n : trunc_index} `{!IsTruncAlgebra n.+1 A} : IsTruncAlgebra n.+1 . Proof. pose proof (hprop_subalgebra_predicate A P). intro s. apply @istrunc_sigma. - exact _. - intro. induction n; exact _. Qed.
Require Import Import algebra_notations ne_list.notations. Import subalgebra_notations.