Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.RelativeComonad.

Generalizable All Variables.

Section Definitions.

  Context `(F : Functor 𝒞 𝒟).

  Implicit Types (A B C D : RelativeComonad F).

  Import RelativeComonad.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.