# interfaces.naturals

Require Import
Relation_Definitions Morphisms
abstract_algebra theory.categories
varieties.semirings categories.varieties.

Class Naturals (A: semirings.Object) `{!InitialArrow A}: Prop :=
{ naturals_initial:> Initial A }.

Section initial_maps.
Variable A: Type.

Class NaturalsToSemiRing :=
naturals_to_semiring: B `{RingMult B} `{RingPlus B} `{RingOne B} `{RingZero B}, A B.

Context `{NaturalsToSemiRing} `{SemiRing A} `{ `{SemiRing B}, SemiRing_Morphism (naturals_to_semiring B)}.

Program Definition natural_initial_arrow: InitialArrow (semirings.object A) :=
λ y u, match u return A y u with tt => naturals_to_semiring (y tt) end.

Global
Lemma natural_initial (same_morphism : `{SemiRing B} {h : A B} `{!SemiRing_Morphism h}, naturals_to_semiring B = h) :
Initial (semirings.object A).
End initial_maps.

Instance: Params (@naturals_to_semiring) 7.

Class Naturals A {e plus mult zero one} `{U: NaturalsToSemiRing A} :=
{ naturals_ring:> @SemiRing A e plus mult zero one
; naturals_to_semiring_mor:> `{SemiRing B}, SemiRing_Morphism (naturals_to_semiring A B)
; naturals_initial:> Initial (semirings.object A) }.

Class NatDistance N `{Equiv N} `{RingPlus N}
:= nat_distance_sig : (x y: N), { z: N | x + z = y y + z = x }.
Definition nat_distance `{NatDistance N} : N N N := λ x y, proj1_sig (nat_distance_sig x y).