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.Isomorphism
.
Require
Import
Theory.Functor
.
Require
Import
Theory.Product
.
Generalizable
All
Variables
.
Cartesian strong monoidal functor
Definition
Section
StrongMonoidal
.
Context
`{
BinaryProduct
π} `{
BinaryProduct
π} (
F
:
Functor
π
π
).
Definition
Ο
(
A
B
:
π
) :
F
(
A
Γ
B
)
β
F
A
Γ
F
B
β
β¨
F
β
Ο
β
,
F
β
Ο
β
β©
.
Class
CartesianStrongMonoidal
β
mkCartesianStrongMonoidal
{
Ο
_inv
:
β
{
A
B
}
,
F
A
Γ
F
B
β
F
(
A
Γ
B
)
;
Ο
_is_inverse
:>
β
{
A
B
}
,
IsInverse
(
Ο
A
B
)
Ο
_inv
}.
End
StrongMonoidal
.
Arguments
mkCartesianStrongMonoidal
{
_
_
_
_
_
_
}
_
.
Arguments
Ο
{
_
_
_
_
_
_
_
}.
Notation
"
'CartesianStrongMonoidal.make' β¦ 'Ο' β Ο β¦" β
(@
mkCartesianStrongMonoidal
_
_
_
_
_
Ο
_
) (
only
parsing
).
Equations
Context
`{
BinaryProduct
π} `{
BinaryProduct
π} {
F
:
Functor
π
π
} `{!
CartesianStrongMonoidal
F
}.
Lemma
F
Ο
β_
Ο
_inv
:
β
{
A
B
}
,
F
β
Ο
β
β
Ο
β»ΒΉ
β
Ο
β
[
F
A
,
F
B
]
.
Show proof.
intros
A
B
.
etransitivity
;
[
apply
Ξ β.cong
; [
instantiate
(1 β
Ο
β
β
Ο
);
unfold
Ο
;
now
rewrite
Ο
β_compose
|
reflexivity
] |].
now
rewrite
compose_assoc
,
iso_left
,
right_id
.
Lemma
F
Ο
β_
Ο
_inv
:
β
{
A
B
}
,
F
β
Ο
β
β
Ο
β»ΒΉ
β
Ο
β
[
F
A
,
F
B
]
.
Show proof.
intros
A
B
.
etransitivity
;
[
apply
Ξ β.cong
; [
instantiate
(1 β
Ο
β
β
Ο
);
unfold
Ο
;
now
rewrite
Ο
β_compose
|
reflexivity
] |].
now
rewrite
compose_assoc
,
iso_left
,
right_id
.
Benedikt Ahrens and RΓ©gis Spadotti—
Terminal semantics for codata types in intensional Martin-LoΜf type theory
Table of contents
Index