Definition nat_to_z2 : nat_algebra s→ z2_algebra := λ s: sorts nat_signature, nat_rect (λ _, bool) false (λ n HP, negb HP). Goal nat_to_z2 nat_sort 0 = false. 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.