Library Coq.Numbers.Natural.Abstract.NIso



Require Import NBase.

Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).

Module NBasePropMod2 := NBasePropFunct NAxiomsMod2.

Notation Local N1 := NAxiomsMod1.N.
Notation Local N2 := NAxiomsMod2.N.
Notation Local Eq1 := NAxiomsMod1.Neq.
Notation Local Eq2 := NAxiomsMod2.Neq.
Notation Local O1 := NAxiomsMod1.N0.
Notation Local O2 := NAxiomsMod2.N0.
Notation Local S1 := NAxiomsMod1.S.
Notation Local S2 := NAxiomsMod2.S.
Notation Local "n == m" := (Eq2 n m) (at level 70, no associativity).

Definition homomorphism (f : N1 -> N2) : Prop :=
  f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n).

Definition natural_isomorphism : N1 -> N2 :=
  NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p).

Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd.


Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2.

Theorem natural_isomorphism_succ :
  forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).


Theorem hom_nat_iso : homomorphism natural_isomorphism.

End Homomorphism.

Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).

Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1.

Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.

Notation Local N1 := NAxiomsMod1.N.
Notation Local N2 := NAxiomsMod2.N.
Notation Local h12 := Hom12.natural_isomorphism.
Notation Local h21 := Hom21.natural_isomorphism.

Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity).

Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n.

End Inverse.

Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).

Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.

Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2.
Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1.

Notation Local N1 := NAxiomsMod1.N.
Notation Local N2 := NAxiomsMod2.N.
Notation Local Eq1 := NAxiomsMod1.Neq.
Notation Local Eq2 := NAxiomsMod2.Neq.
Notation Local h12 := Hom12.natural_isomorphism.
Notation Local h21 := Hom21.natural_isomorphism.

Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop :=
  Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\
  forall n : N1, Eq1 (f2 (f1 n)) n /\
  forall n : N2, Eq2 (f1 (f2 n)) n.

Theorem iso_nat_iso : isomorphism h12 h21.




End Isomorphism.