Algebra σ := BuildAlgebra carriers_prod_algebra ops_prod_algebra. Global Instance trunc_prod_algebra {n : trunc_index} `{!∀ i, IsTruncAlgebra n (A i)} : IsTruncAlgebra n . Proof. intro s. exact _. Qed.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.