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
.
Require
Import
Theory.Functor
.
Natural transformation definition
Structure
NaturalTransformation
{π π :
Category
} (
F
G
:
Functor
π
π
) β
mkNaturalTransformation
{
Ξ·
:
β
A
,
F
A
β
G
A
;
Ξ·_commutes
:
β
{
A
B
} {
f
:
A
β
B
},
Ξ·
(
B
)
β
F
β
f
β
G
β
f
β
Ξ·
(
A
) }.
Arguments
mkNaturalTransformation
{
_
_
_
_
_
}
_
.
Arguments
Ξ·
{
_
_
_
_
}
_
_
.
Arguments
Ξ·_commutes
{
_
_
_
_
}
_
{
_
_
_
}.
Notation
"
'NaturalTransformation.make' β¦ 'Ξ·' β Ξ· β¦" β
(@
mkNaturalTransformation
_
_
_
_
Ξ·
_
) (
only
parsing
).
Benedikt Ahrens and RΓ©gis Spadotti—
Terminal semantics for codata types in intensional Martin-LoΜf type theory
Table of contents
Index