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.Types.
Require Import Category.Setoids.
Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.Product.
Require Import Theory.Isomorphism.
Require Import Theory.CartesianStrongMonoidal.

Functor 𝑬𝑸 : π‘»π’šπ’‘π’† β†’ π‘Ίπ’†π’•π’π’Šπ’…

Definition

Program Definition F : π‘»π’šπ’‘π’† β†’ π‘Ίπ’†π’•π’π’Šπ’… ≔ Ξ» T βˆ™ Setoids.make⦃ Carrier≔ T
; Equiv≔ eq ⦄.

Program Definition map {A B} : [ A β‡’ B ⟢ F A β‡’ F B ] ≔
  Ξ» f ↦ Setoids.Morphism.make f.
f-cong
Show proof.
  intros f g eq_fg x y eq_xy; simpl.
  now rewrite eq_xy.

Lemma id A : id[ F A ] β‰ˆ map id[ A ].
Show proof.
  intros x y eq_xy; now rewrite eq_xy.

Lemma map_compose A B C (f : A β‡’ B) (g : B β‡’ C) : map (g ∘ f) β‰ˆ (map g) ∘ (map f).
Show proof.
  intros x y eq_xy. now rewrite eq_xy.

Definition 𝑬𝑸 : Functor π‘»π’šπ’‘π’† π‘Ίπ’†π’•π’π’Šπ’… ≔ mkFunctor id map_compose.

𝑬𝑸 is strong monoidal

Program Instance 𝑬𝑸_SM : CartesianStrongMonoidal 𝑬𝑸 ≔
  CartesianStrongMonoidal.make ⦃ Ο† ≔ Ξ» A B βˆ™ Setoids.Morphism.make (Ξ» x βˆ™ x) ⦄.
Ο†-cong
Show proof.
  now f_equal.
Ο†-inverse
Show proof.
  constructor.
  -
    intros f g eq_fg. exact eq_fg.
  -
    intros f g eq_fg. simpl in Γ—. destruct f. auto.

Functor 𝑬𝑸-Γ— : π‘»π’šπ’‘π’† Γ— π‘»π’šπ’‘π’† β†’ π‘Ίπ’†π’•π’π’Šπ’…

Definition

Program Definition 𝑬𝑸_prod : Functor (π‘»π’šπ’‘π’† π˜… π‘»π’šπ’‘π’†) π‘Ίπ’†π’•π’π’Šπ’… ≔
  Functor.make ⦃ F≔ Ξ» A βˆ™ Setoids.make ⦃ Carrier ≔ fst A βŸ¨Γ—βŸ© snd A
                                          ; Equiv ≔ eq ⦄
               ; map ≔ Ξ» A B βˆ™ Ξ» f ↦ Setoids.Morphism.make (Ξ» x βˆ™ (fst f (fst x) , snd f (snd x))) ⦄.
equivalence
Show proof.
  eauto with typeclass_instances.
map-proper
Show proof.
  intros [? ?] [? ?] [? ?] [? ?] [? ?] eq. injection eq; intros.
  simpl in *; f_equal; congruence.

Notation "𝑬𝑸-π˜…" ≔ 𝑬𝑸_prod.
Benedikt Ahrens and RΓ©gis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index