Require Import Category.Types.
Require Import Category.Setoids.
Require Import Category.Types_Setoids.
Require Import Category.RComod.
Require Import Category.RComonadWithCut.
Require Import Theory.Category.
Require Import Theory.Functor.
Require Import Theory.RelativeComonadWithCut.
Require Import Theory.Comodule.
Require Import Theory.Product.
Require Import Theory.PrecompositionWithProduct.
Require Import Theory.PushforwardComodule.

Generalizable All Variables.

Module TriMat.

  Structure Obj (E : 𝑻𝒚𝒑𝒆) : Type ≔ mkObj

{ T	:>	𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅𝑾𝒊𝒕𝒉𝑪𝒖𝒕 𝑬𝑸 E
; rest	:>	[T] ⇒ [T][E×─]
; rest_cut	:	∀ {A}, rest(A) ∘ T⋅cut ≈ T⋅cut ∘ rest(E × A) }.

Arguments mkObj	{_ _ _} _.
Arguments T	{_} _.
Arguments rest	{_} _.
Arguments rest_cut	{_} _ {_ _ _ _}.

  Notation "'TriMat.make' ⦃ 'T' ≔ T ; 'rest' ≔ rest ⦄" ≔
           (@mkObj _ T rest _) (only parsing).

  Structure Morphism {E} (T S : Obj E) : Type ≔ mkMorphism

{ τ	:> T ⇒ S
; τ_commutes	: ⟨τ⟩［E×─］ ∘ Φ ∘ τ⁎⋅T ≈ S ∘ ⟨τ⟩ }.

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

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

  Program Definition Hom {E} (T S : Obj E) : Setoid ≔

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

  Show proof.

End TriMat.

Export TriMat.

Section Defs.

  Variable (E : 𝑻𝒚𝒑𝒆).

  Implicit Types (T S R U : Obj E).

  Infix "⇒" ≔ Hom.

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

  Show proof.

  Obligation Tactic ≔ idtac.
  Program Definition compose {T S R} : [ S ⇒ R ⟶ T ⇒ S ⟶ T ⇒ R ] ≔
    λ g f ↦₂ TriMat.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.