interfaces.integers

A model of the the integers, ZZ.

Section initial_maps.
  Variable Int: Type.

  Class IntegersToRing :=
    integers_to_ring: R `{RingMult R} `{RingPlus R} `{RingOne R} `{RingZero R} `{GroupInv R}, Int R.

  Context `{IntegersToRing} `{Ring Int} `{ `{Ring B}, SemiRing_Morphism (integers_to_ring B)}.

  Global Instance integer_initial_arrow: InitialArrow (rings.object Int).
  Defined.
  Lemma integer_initial (same_morphism : `{Ring B} {h : Int B} `{!SemiRing_Morphism h}, integers_to_ring B = h) :
    Initial (rings.object Int).
End initial_maps.

Instance: Params (@integers_to_ring) 8.

Class Integers A {e plus mult zero one opp} `{U : IntegersToRing A} :=
  { integers_ring:> @Ring A e plus mult zero one opp
  ; integers_to_ring_mor:> `{Ring B}, SemiRing_Morphism (integers_to_ring A B)
  ; integers_initial:> Initial (rings.object A) }.

Section specializable.
  Context (Int N: Type) `{Equiv Int} `{RingMult Int} `{RingPlus Int} `{RingOne Int}
    `{GroupInv Int} `{RingZero Int} `{NaturalsToSemiRing N}.

  Class IntAsNat := int_as_nat: i: Int,
    { n: N | i = naturals_to_semiring N Int n } + { n: N | i = - naturals_to_semiring N Int n }.

  Class IntAbs := int_abs_sig : i: Int,
    { n: N | naturals_to_semiring N Int n = i - naturals_to_semiring N Int n = i }.
  Definition int_abs `{IntAbs}: Int N := λ x, proj1_sig (int_abs_sig x).
End specializable.

Instance: Params (@int_abs) 10.