Benedikt Ahrens and RΓ©gis Spadotti—
Terminal semantics for codata types in intensional Martin-LoΜf type theory
Table of contents
Index
Require
Import
Theory.Category
.
Functor definition
Structure
Functor
(π π :
Category
) :
Type
β
mkFunctor
{
F
:>
π
β
π
;
map
:
β
{
A
B
}
,
[
A
β
B
βΆ
F
A
β
F
B
]
;
identity
:
β
{
A
}
,
id
[
F
A
]
β
map
id
[
A
]
;
map_compose
:
β
{
A
B
C
} {
f
:
A
β
B
} {
g
:
B
β
C
},
map
(
g
β
f
)
β
(
map
g
)
β
(
map
f
)
}.
Arguments
mkFunctor
{
_
_
} {
_
_
}
_
_
.
Arguments
map
{
_
_
}
_
{
_
_
}.
Notation
"
F β f" β (
map
F
f
) (
at
level
35,
no
associativity
).
Notation
"
'Functor.make' β¦ 'F' β F ; 'map' β map β¦" β
(@
mkFunctor
_
_
F
map
_
_
) (
only
parsing
).
Benedikt Ahrens and RΓ©gis Spadotti—
Terminal semantics for codata types in intensional Martin-LoΜf type theory
Table of contents
Index