Library Stdlib.Numbers.Natural.Abstract.NIso
Require Import NBase.
Module Homomorphism (N1 N2 : NAxiomsRecSig).
Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity).
Definition homomorphism (f : N1.t -> N2.t) : Prop :=
f N1.zero == N2.zero /\ forall n, f (N1.succ n) == N2.succ (f n).
Definition natural_isomorphism : N1.t -> N2.t :=
N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.succ p).
#[global]
Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism.
Theorem natural_isomorphism_0 : natural_isomorphism N1.zero == N2.zero.
Theorem natural_isomorphism_succ :
forall n : N1.t, natural_isomorphism (N1.succ n) == N2.succ (natural_isomorphism n).
Theorem hom_nat_iso : homomorphism natural_isomorphism.
End Homomorphism.
Module Inverse (N1 N2 : NAxiomsRecSig).
Module Import NBasePropMod1 := NBaseProp N1.
Module Hom12 := Homomorphism N1 N2.
Module Hom21 := Homomorphism N2 N1.
Local Notation h12 := Hom12.natural_isomorphism.
Local Notation h21 := Hom21.natural_isomorphism.
Local Notation "n == m" := (N1.eq n m) (at level 70, no associativity).
Lemma inverse_nat_iso : forall n : N1.t, h21 (h12 n) == n.
End Inverse.
Module Isomorphism (N1 N2 : NAxiomsRecSig).
Module Hom12 := Homomorphism N1 N2.
Module Hom21 := Homomorphism N2 N1.
Module Inverse12 := Inverse N1 N2.
Module Inverse21 := Inverse N2 N1.
Local Notation h12 := Hom12.natural_isomorphism.
Local Notation h21 := Hom21.natural_isomorphism.
Definition isomorphism (f1 : N1.t -> N2.t) (f2 : N2.t -> N1.t) : Prop :=
Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\
forall n, N1.eq (f2 (f1 n)) n /\
forall n, N2.eq (f1 (f2 n)) n.
Theorem iso_nat_iso : isomorphism h12 h21.
End Isomorphism.