Library UniMath.Algebra.Universal.Examples.Nat

Example on natural numbers

Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021

This file contains the definition of the signature of natural numbers with zero and addition, the algebras of natural numbers and booleans and the morphism between them.

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.

Local Open Scope stn.
Local Open Scope hom.

Definition nat_signature := make_signature_simple_single_sorted [ 0 ; 1 ].

Definition nat_sort: sorts nat_signature := tt.

Definition nat_zero_op: names nat_signature := ●0.
Definition nat_succ_op: names nat_signature := ●1.

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.

Goal ops' nat_algebra nat_succ_op 1 = 2.
Proof. apply idpath. Defined.

Definition z2_algebra := make_algebra_simple_single_sorted' nat_signature boolset [( false ; negb )].

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.

Goal nat_to_z2 nat_sort 1 = true.
Proof. apply idpath. Defined.

Goal nat_to_z2 nat_sort 2 = false.
Proof. apply idpath. Defined.

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.

Definition natz2 : nat_algebra ↷ z2_algebra := make_hom ishom_nat_to_z2.

Definition nat_zero := build_gterm' nat_zero_op.
Definition nat_succ := build_gterm' nat_succ_op.

Definition nat2term (n: nat): gterm nat_signature nat_sort
  := nat_rect
       (λ _, gterm nat_signature nat_sort)
       nat_zero
       (λ (n: nat) (tn: gterm nat_signature nat_sort ), nat_succ tn)
       n.