(b:Bool) : Algebra σ := if b then B else A. Global Instance trunc_bin_prod_algebras {n : trunc_index} `{!IsTruncAlgebra n A} `{!IsTruncAlgebra n B} : ∀ (b:Bool), IsTruncAlgebra n ( b). Proof. intros []; exact _. Qed.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.