Terminal semantics for codata types in intensional Martin-Löf type theory

Require Import Category.RComod.
Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.Isomorphism.
Require Import Theory.RelativeComonad.
Require Import Theory.RelativeComonadWithCut.
Require Import Theory.Comodule.
Require Import Theory.Product.
Require Import Theory.CartesianStrongMonoidal.

Generalizable All Variables.

          {E : 𝒞} `{!CartesianStrongMonoidal F} {T : RelativeComonadWithCut F E}
          {ℰ : Category} (M : Comodule T ℰ).

  Program Definition precomposition_with_product : Comodule T ℰ ≔

Comodule.make	⦃ M	≔ λ C ∙ M (E × C)
	; mcobind	≔ λ A B ∙ λ f ↦ M ⋅mcobind (T ⋅extend(f)) ⦄.

intros f g eq_fg. now rewrite eq_fg.

rewrite cut_counit. rewrite <- ∘-×. rewrite <- compose_assoc. rewrite iso_right.
rewrite left_id. rewrite mcobind_counit. reflexivity.

    rewrite mcobind_mcobind. apply Π.cong. repeat rewrite compose_assoc.
    rewrite ∘-×. rewrite cut_cobind. unfold Extend. simpl.
    repeat rewrite compose_assoc. rewrite counit_cobind.
    repeat rewrite <- compose_assoc. rewrite F π ₁_φ _inv. rewrite π ₁_compose. reflexivity.

End PrecompositionWithProduct.

Arguments precomposition_with_product {_ _ _ _ _} _ {_ _ _} _.

Notation "M [ E '×─' ] " ≔ (precomposition_with_product E M) (at level 0).

Section Morphisms.

now rewrite α_commutes.

End Morphisms.

Arguments precomposition_with_product_mor {_ _ _ _ _} _ {_ _ _ _ _} _.

Notation "α ［ E '×─' ］" ≔ (precomposition_with_product_mor E α) (at level 0).

Precomposition with product