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
.