Lemma ishom_nat_to_z2: @ishom _ nat_algebra z2_algebra (nat_to_z2). Proof. unfold ishom. intros. induction nm as [n proofn]. inductive_reflexivity n proofn. 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.