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.Isomorphism.
Require Import Theory.Functor.
Require Import Theory.Product.

Generalizable All Variables.

Cartesian strong monoidal functor

Definition

Section StrongMonoidal.

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

  Definition Ο† (A B : π’ž) : F (A Γ— B) β‡’ F A Γ— F B ≔ ⟨ F β‹… π₁ , F β‹… Ο€β‚‚ ⟩.

  Class CartesianStrongMonoidal ≔ mkCartesianStrongMonoidal
  { Ο†_inv: βˆ€ {A B}, F A Γ— F B β‡’ F (A Γ— B)
  ; Ο†_is_inverse :> βˆ€ {A B}, IsInverse (Ο† A B) Ο†_inv }.

End StrongMonoidal.

Arguments mkCartesianStrongMonoidal {_ _ _ _ _ _} _.
Arguments Ο† {_ _ _ _ _ _ _}.

Notation "'CartesianStrongMonoidal.make' ⦃ 'Ο†' ≔ Ο† ⦄" ≔
  (@mkCartesianStrongMonoidal _ _ _ _ _ Ο† _) (only parsing).

Equations

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

  Lemma Fπ₁_Ο†_inv : βˆ€ {A B}, F β‹… π₁ ∘ φ⁻¹ β‰ˆ π₁[F A, F B].
  Show proof.
    intros A B.
    etransitivity;
      [ apply Ξ β‚‚.cong; [ instantiate (1 ≔ π₁ ∘ Ο†); unfold Ο†; now rewrite π₁_compose
                       | reflexivity ] |].
    now rewrite compose_assoc, iso_left, right_id.

  Lemma FΟ€β‚‚_Ο†_inv : βˆ€ {A B}, F β‹… Ο€β‚‚ ∘ φ⁻¹ β‰ˆ Ο€β‚‚[F A, F B].
  Show proof.
    intros A B.
    etransitivity;
      [ apply Ξ β‚‚.cong; [ instantiate (1 ≔ Ο€β‚‚ ∘ Ο†); unfold Ο†; now rewrite Ο€β‚‚_compose
                       | reflexivity ] |].
    now rewrite compose_assoc, iso_left, right_id.

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