Terminal semantics for codata types in intensional Martin-Löf type theory

This table of contents give pointers in the Coq formalisation following the sectioning of the paper

Preliminaries

• Category definition
• Category of Types
• Category of Setoids
• Functor 𝑬𝑸 : Type -> Setoid
• Cartesian strong monoidal functors
  • Functor 𝑬𝑸 is strong monoidal

Codata types in intensional Martin-Löf type theory

• Streams
• Cosubstitution for streams
• Infinite triangular matrices
• Redecoration for infinite triangular matrices

Relative Comonads and their morphisms

• Relative comonad definition
• Functoriality of relative comonads
• Morphism of relative comonads
• Category of relative comonads

Comodules over relative comonads

• Comodule over a relative comonad definition
• Functoriality of comodules
• Morphism of comodules
• Category of comodules
• Tautological comodule
• Pushforward comodule
• Morphism of comonads induces morphism of comodules

Terminality for streams and infinite triangular matrices

• Relative comonad with cut definition
• Morphism of relative comonads with cut
• Category of relative comonads with cut
• Canonical cut operation
• Precomposition with product
• Pushforward commutes with precomposition with product
• Category of streams
• Terminal object in Stream
• Category TriMat of infinite triangular matrices
• Terminal object in TriMat