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

Generalizable All Variables.

Structure Comodule `{F : Functor 𝒞 𝒟} (T : RelativeComonad F) (ℰ : Category) : Type ≔ mkComodule

{ M	:>	𝒞 → ℰ
; mcobind	:	∀ {C D}, [ T C ⇒ F D ⟶ M C ⇒ M D ]
; mcobind_counit	:	∀ {C}, mcobind counit[ C ] ≈ id[ M C ]
; mcobind_mcobind	:	∀ {C D E} {f : T C ⇒ F D} {g : T D ⇒ F E},

                         mcobind(g) ∘ mcobind(f) ≈ mcobind(g ∘ T⋅cobind(f)) }.

Arguments mkComodule	{_ _ _ _ _ _ _} _ _.
Arguments M	{_ _ _ _ _} _ _.
Arguments mcobind	{_ _ _ _ _} _ {_ _}.
Arguments mcobind_counit	{_ _ _ _ _} _ {_}.
Arguments mcobind_mcobind	{_ _ _ _ _} _ {_ _ _ _ _}.

Notation "M '⋅mcobind'" ≔ (mcobind M) (at level 0).

Notation "'Comodule.make' ⦃ 'M' ≔ M ; 'mcobind' ≔ mcobind ⦄" ≔
  (@mkComodule _ _ _ _ _ M mcobind _ _) (only parsing).

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

  Program Definition mlift {A B} : [ A ⇒ B ⟶ M A ⇒ M B ] ≔
    λ f ↦ M⋅mcobind (F⋅f ∘ counit[ A ]).
  Show proof.

  Lemma mlift_id A : id[ M A ] ≈ mlift id[ A ].
  Show proof.

  Lemma mlift_compose A B C (f : A ⇒ B) (g : B ⇒ C) : mlift (g ∘ f) ≈ (mlift g) ∘ (mlift f).
  Show proof.

  Definition MLift : Functor 𝒞 ℰ ≔ mkFunctor mlift_id mlift_compose.

Structure Morphism `{F : Functor 𝒞 𝒟} {T : RelativeComonad F} {ℰ} (M N : Comodule T ℰ) : Type ≔ mkMorphism

{ α	:> ∀ C, M C ⇒ N C
; α_commutes	: ∀ {C D} {f : T C ⇒ F D}, α(D) ∘ M⋅mcobind f ≈ N⋅mcobind f ∘ α(C) }.

Arguments mkMorphism	{_ _ _ _ _ _ _ _} _.
Arguments α	{_ _ _ _ _ _ _} _ _.
Arguments α_commutes	{_ _ _ _ _ _ _} _ {_ _ _}.

Notation "'Comodule.make' ⦃ 'α' ≔ α ⦄" ≔
         (@mkMorphism _ _ _ _ _ _ _ α _) (only parsing).

Module Morphism.

  Section id_composition.

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

    Program Definition Hom (M N : Comodule T ℰ) : Setoid ≔
      Setoid.make ⦃ Carrier ≔ Morphism M N

; Equiv

≔ λ f g ∙ ∀ x, f x ≈ g x ⦄.

    Show proof.

    Local Infix "⇒" ≔ Hom.

    Program Definition id {M : Comodule T ℰ} : M ⇒ M ≔
      Comodule.make ⦃ α ≔ λ C ∙ id[ M C ] ⦄.
    Show proof.

    Program Definition compose {M N P : Comodule T ℰ} : [ N ⇒ P ⟶ M ⇒ N ⟶ M ⇒ P ] ≔
      λ g f ↦₂ Comodule.make ⦃ α ≔ λ C ∙ g(C) ∘ f(C) ⦄.
    Show proof.
    Show proof.

  End id_composition.

End Morphism.