(f : ∀ (i:I) s, C s → A i s) : ∀ (s : Sort σ) , C s → ProdAlgebra I A s := λ (s : Sort σ) (x : C s) (i : I), f i s x.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.