Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.RelativeComonadWithCut.
Require Import Theory.Product.
Require Import Theory.CartesianStrongMonoidal.

Generalizable All Variables.

Section Definitions.

  Context `{BinaryProduct 𝒞} `{BinaryProduct 𝒟}
          (F : Functor 𝒞 𝒟) (E : 𝒞) `{!CartesianStrongMonoidal F}.

  Implicit Types (A B C D : RelativeComonadWithCut F E).

  Import RelativeComonadWithCut.Morphism.

  Infix "⇒" ≔ Hom.
  Infix "∘" ≔ compose.

Lemma left_id A B

(f : A ⇒ B) : id ∘ f ≈ f.

  Show proof.

  Lemma right_id A B (f : A ⇒ B) : f ∘ id ≈ f.
  Show proof.

  Lemma compose_assoc A B C D (f : A ⇒ B) (g : B ⇒ C) (h : C ⇒ D) : h ∘ g ∘ f ≈ h ∘ (g ∘ f).
  Show proof.

  Canonical Structure 𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅𝑾𝒊𝒕𝒉𝑪𝒖𝒕 : Category ≔
    mkCategory left_id right_id compose_assoc.

End Definitions.