Definition nat_algebra := make_algebra_simple_single_sorted' nat_signature natset [( 0 ; S )]. Goal ops' nat_algebra nat_zero_op = 0. Proof. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.MoreLists. Require Import UniMath.Algebra.Universal.Algebras. Require Import UniMath.Algebra.Universal.Terms.