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

Generalizable All Variables.

Section Definitions.

  Context `{F : Functor 𝒞 𝒟} (T : RelativeComonad F) (ℰ : Category).

  Implicit Types (A B C D : Comodule T ℰ).

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