Benedikt Ahrens and RΓ©gis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index
Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.RelativeComonad.
Require Import Theory.Comodule.

Generalizable All Variables.

Category of Comodules

Category definition

Section Definitions.

  Context `{F : Functor π’ž π’Ÿ} (T : RelativeComonad F) (β„° : Category).

  Implicit Types (A B C D : Comodule T β„°).

  Import Comodule.Morphism.

  Infix "β‡’" ≔ Hom.
  Infix "∘" ≔ compose.

  Lemma left_id A B(f : A β‡’ B) : id ∘ f β‰ˆ f.
  Show proof.
    intro x; simpl. rewrite left_id. reflexivity.

  Lemma right_id A B (f : A β‡’ B) : f ∘ id β‰ˆ f.
  Show proof.
    intro x; simpl. now rewrite right_id.

  Lemma compose_assoc A B C D (f : A β‡’ B) (g : B β‡’ C) (h : C β‡’ D) : h ∘ g ∘ f β‰ˆ h ∘ (g ∘ f).
  Show proof.
    intro x; simpl. now rewrite compose_assoc.

  Canonical Structure 𝑹π‘ͺπ’π’Žπ’π’… : Category ≔
    mkCategory left_id right_id compose_assoc.

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