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.

Generalizable All Variables.

Relative comonad

Definition

Structure RelativeComonad `(F : Functor π’ž π’Ÿ) : Type ≔ mkRelativeComonad
{ T:>π’ž β†’ π’Ÿ
; counit:βˆ€ {X}, T X β‡’ F X
; cobind:βˆ€ {X Y}, [ T X β‡’ F Y ⟢ T X β‡’ T Y ]
; cobind_counit:βˆ€ {X}, cobind counit β‰ˆ id[ T X ]
; counit_cobind:βˆ€ {X Y} {f : T X β‡’ F Y}, counit ∘ cobind(f) β‰ˆ f
; cobind_cobind:βˆ€ {X Y Z} {f : T X β‡’ F Y} {g : T Y β‡’ F Z}, cobind(g) ∘ cobind(f) β‰ˆ cobind(g ∘ cobind(f)) }.

Arguments mkRelativeComonad{_ _ _ _ _ _} _ _ _.
Arguments counit{_ _ _} _ {_}.
Arguments cobind{_ _ _} _ {_ _}.
Arguments cobind_counit{_ _ _} _ {_}.
Arguments counit_cobind{_ _ _} _ {_ _ _}.
Arguments cobind_cobind{_ _ _} _ {_ _ _ _ _}.

Notation "'counit[' X ]"≔ (counit _ (X ≔ X)) (only parsing).
Notation "T 'β‹…counit'"≔ (counit T) (at level 0, only parsing).
Notation "T 'β‹…counit[' X ]"≔ (counit T (X ≔ X)) (at level 0, only parsing).
Notation "T 'β‹…cobind'"≔ (cobind T) (at level 0, only parsing).

Notation "'RelativeComonad.make' ⦃ 'T' ≔ T ; 'counit' ≔ counit ; 'cobind' ≔ cobind ⦄" ≔
  (@mkRelativeComonad _ _ _ T counit cobind _ _ _) (only parsing).

Functoriality of relative comonads

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

  Program Definition lift {A B} : [ A β‡’ B ⟢ T A β‡’ T B ] ≔
    Ξ» f ↦ Tβ‹…cobind (Fβ‹…f ∘ Tβ‹…counit).
  Show proof.
    intros f g eq_fg. now rewrite eq_fg.

  Lemma lift_id : βˆ€ A, id[ T A ] β‰ˆ lift id[ A ].
  Show proof.
    intros A; simpl; unfold lift.
    rewrite <- identity, left_id, cobind_counit.
    reflexivity.

  Lemma lift_compose : βˆ€ A B C (f : A β‡’ B) (g : B β‡’ C), lift (g ∘ f) β‰ˆ (lift g) ∘ (lift f).
  Show proof.
    intros A B C g f; simpl; unfold lift.
    rewrite cobind_cobind,
            compose_assoc,
            counit_cobind,
            <- compose_assoc,
            <- map_compose.
    reflexivity.

  Definition Lift : Functor π’ž π’Ÿ ≔ mkFunctor lift_id lift_compose.

Morphism of relative comonads

Structure Morphism `{F : Functor π’ž π’Ÿ} (T S : RelativeComonad F) : Type ≔ mkMorphism
{ Ο„:>βˆ€ C, T C β‡’ S C
; Ο„_counit:βˆ€ {C}, Tβ‹…counit[ C ] β‰ˆ Sβ‹…counit[ C ] ∘ Ο„(C)
; Ο„_commutes:βˆ€ {C D} {f : S C β‡’ F D}, Ο„(D) ∘ Tβ‹…cobind (f ∘ Ο„(C)) β‰ˆ Sβ‹…cobind f ∘ Ο„(C) }.

Arguments mkMorphism{_ _ _ _ _ _} _ _.
Arguments Ο„{_ _ _ _ _ _} _.
Arguments Ο„_counit{_ _ _ _ _} _ {_}.
Arguments Ο„_commutes{_ _ _ _ _} _ {_ _ _}.

Notation "'RelativeComonad.make' ⦃ 'Ο„' ≔ Ο„ ⦄" ≔ (@mkMorphism _ _ _ _ _ Ο„ _ _) (only parsing).

Module Morphism.

  Section id_composition.

    Context `{F : Functor π’ž π’Ÿ}.

    Implicit Types (T S U : RelativeComonad F).

    Program Definition Hom T S : Setoid ≔
      Setoid.make ⦃ Carrier ≔ Morphism T S ; Equiv ≔ Ξ» f g βˆ™ βˆ€ x, f x β‰ˆ g x ⦄.
    Show proof.
      constructor.
      - intros f x; reflexivity.
      - intros f g eq_fg x. symmetry. apply eq_fg.
      - intros f g h eq_fg eq_gh; etransitivity; eauto.

    Local Infix "β‡’" ≔ Hom.

    Program Definition id {S} : S β‡’ S ≔
      RelativeComonad.make ⦃ Ο„ ≔ Ξ» C βˆ™ id[ S C ] ⦄.
    Show proof.
      now rewrite right_id.
    Show proof.
      rewrite left_id; now do 2 rewrite right_id.

    Program Definition compose {S T U} : [ T β‡’ U ⟢ S β‡’ T ⟢ S β‡’ U ] ≔
      Ξ» g f ↦₂ RelativeComonad.make ⦃ Ο„ ≔ Ξ» C βˆ™ g(C) ∘ f(C) ⦄.
    Show proof.
      rewrite <- compose_assoc; now do 2 rewrite <- Ο„_counit.
    Show proof.
      setoid_rewrite <- compose_assoc at 2.
      rewrite <- Ο„_commutes. rewrite compose_assoc.
      setoid_rewrite <- compose_assoc at 2. rewrite Ο„_commutes.
      rewrite <- compose_assoc. reflexivity.
    Show proof.
      intros f₁ fβ‚‚ eq_f₁fβ‚‚ g₁ gβ‚‚ eq_g₁gβ‚‚ x. simpl.
      apply Ξ β‚‚.cong; [ apply eq_f₁fβ‚‚ | apply eq_g₁gβ‚‚ ].

  End id_composition.

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