interfaces.naturals

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

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

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).