Library Coq.Numbers.Natural.Abstract.NIso
Require
Import
NBase
.
Module
Homomorphism
(
N1
N2
:
NAxiomsRecSig
).
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
).
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
.
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
.
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
.