Require Import Category.Types.
Require Import Category.Setoids.
Require Import Category.Types_Setoids.
Require Import Category.RComonad.
Require Import Category.RComod.
Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.RelativeComonad.
Require Import Theory.PushforwardComodule.
Require Import Theory.Comodule.

Generalizable All Variables.

Module Stream.

  Structure Obj : Type ≔ mkObj

{ T	:>	𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅 𝑬𝑸
; tail	:> [T] ⇒ [T] }.

Arguments mkObj	{_ } _.
Arguments T	_.
Arguments tail	_.

  Notation "'Stream.make' ⦃ 'T' ≔ T ; 'tail' ≔ tail ⦄" ≔
           (@mkObj T tail) (only parsing).

  Structure Morphism (T S : Obj) : Type ≔ mkMorphism

{ τ	:> T ⇒ S
; τ_commutes	: ⟨τ⟩ ∘ τ⁎⋅T ≈ S ∘ ⟨τ⟩ }.

Arguments mkMorphism	{_ _ _} _.
Arguments τ	{_ _} _.
Arguments τ_commutes	{_ _} _ {_ _ _ _}.

  Notation "'Stream.make' ⦃ 'τ' ≔ τ ⦄" ≔ (@mkMorphism _ _ τ _) (only parsing).

  Program Definition Hom (T S : Obj) : Setoid ≔

Setoid.make	⦃ Carrier	≔ Morphism T S
	; Equiv	≔ (λ g f ∙ g ≈ f) ⦄.

  Show proof.

End Stream.

Export Stream.

Section Defs.

  Implicit Types (T S R U : Obj).

  Infix "⇒" ≔ Hom.

  Program Definition id {T} : T ⇒ T ≔
    Stream.make ⦃ τ ≔ id[T] ⦄.

  Show proof.

  Obligation Tactic ≔ idtac.
  Program Definition compose {T S R} : [ S ⇒ R ⟶ T ⇒ S ⟶ T ⇒ R ] ≔
    λ g f ↦₂ Stream.make ⦃ τ ≔ g ∘ f ⦄.

  Show proof.

  Show proof.

  Infix "∘" ≔ compose.

  Lemma left_id : ∀ T S (f : T ⇒ S), id ∘ f ≈ f.
  Show proof.

  Lemma right_id : ∀ T S (f : T ⇒ S), f ∘ id ≈ f.
  Show proof.

  Lemma compose_assoc T R S U (f : T ⇒ R) (g : R ⇒ S) (h : S ⇒ U) : h ∘ g ∘ f ≈ h ∘ (g ∘ f).
  Show proof.

  Canonical Structure 𝑺𝒕𝒓𝒆𝒂𝒎 : Category ≔
    mkCategory left_id right_id compose_assoc.

End Defs.