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.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-Löf type theory
Table of contents
Index