Benedikt Ahrens and RΓ©gis Spadotti—
Terminal semantics for codata types in intensional Martin-LoΜf type theory
Table of contents
Index
Require
Import
Category.RComonad
.
Require
Import
Category.RComonadWithCut
.
Require
Import
Theory.Category
.
Require
Import
Theory.Isomorphism
.
Require
Import
Theory.Functor
.
Require
Import
Theory.RelativeComonad
.
Require
Import
Theory.RelativeComonadWithCut
.
Require
Import
Theory.Product
.
Require
Import
Theory.CartesianStrongMonoidal
.
Generalizable
All
Variables
.
Canonical cut
Definition
Section
Defs
.
Context
`{
BinaryProduct
π} `{
BinaryProduct
π} (
F
:
Functor
π
π
) (
E
:
π
) `{!
CartesianStrongMonoidal
F
}.
Program Definition
πͺππ
:
Functor
(
πΉπͺππππππ
F
) (
πΉπͺππππππ πΎππππͺππ
F
E
) β
Functor.make
β¦
F
β
Ξ»
T
β
RelativeComonadWithCut.make
β¦
RelativeComonad
β
T
;
cut
β
Ξ»
A
β
Lift
(
T
)
β
Ο
β
β¦
;
map
β
Ξ»
T
S
β
Ξ»
Ο
β¦
RelativeComonadWithCut.make
β¦
RelativeComonad
-Ο
β
Ο
β¦
β¦
.
cut-counit
Show proof.
now
rewrite
counit_cobind
.
cobind-cobind
Show proof.
do
2
rewrite
cobind_cobind
.
apply
Ξ .cong
.
now
rewrite
compose_assoc
,
counit_cobind
,
<-
compose_assoc
,
F
Ο
β_
Ο
_inv
,
Ο
β_compose
.
cut-cobind
Show proof.
now
rewrite
(
RelativeComonad
.Ο
_counit
Ο), <-
compose_assoc
,
RelativeComonad
.Ο
_commutes
.
map-cong
Show proof.
intros
f
g
eq_fg
x
.
auto
.
map-id
Show proof.
reflexivity
.
map-compose
Show proof.
reflexivity
.
Program Definition
πΌ
:
Functor
(
πΉπͺππππππ πΎππππͺππ
F
E
) (
πΉπͺππππππ
F
) β
Functor.make
β¦
F
β
Ξ»
T
β
T
;
map
β
Ξ»
A
B
β
Ξ»
Ο
β¦
Ο
β¦
.
map-cong
Show proof.
repeat
intro
;
auto
.
map-id
Show proof.
reflexivity
.
map-compose
Show proof.
reflexivity
.
End
Defs
.
Benedikt Ahrens and RΓ©gis Spadotti—
Terminal semantics for codata types in intensional Martin-LoΜf type theory
Table of contents
Index