Benedikt Ahrens and Régis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index
Require Import Category.RComod.
Require Import Category.Stream.Category.
Require Import Category.Stream.Model.
Require Import Category.TriMat.Axioms.
Require Import Category.TriMat.Model.
Require Import Theory.Category.
Require Import Theory.RelativeComonad.
Require Import Theory.RelativeComonadWithCut.

Module Diag (Import TE : Typ).

  Module Import TriTriMat.Model.Terminality TE.
  Module StrStream.Model.Terminality.

  Definition 𝒅𝒊𝒂𝒈Str Stream.make T 𝑻𝒓𝒊 ; tail 𝑪𝒖𝒕 𝑹𝒆𝒔𝒕 .

End Diag.
Benedikt Ahrens and Régis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index