module stlc.catComb.betaeta where

open import stlc.catComb.eval
open import stlc.monad

open CatCombValue

infix 3 _=βη_

data _=βη_ : ∀ {A B} → CatComb A B → CatComb A B → Set where
  refl : ∀ {A B} {f : CatComb A B} → f =βη f
  sym : ∀ {A B} {f g : CatComb A B} → f =βη g → g =βη f
  trans : ∀ {A B} {f g h : CatComb A B} → f =βη g → g =βη h → f =βη h
--- CATEGORICAL ---
  assoc : ∀ {A B C D} {f : CatComb C D} {g : CatComb B C} {h : CatComb A B} → (f ∘ g) ∘ h =βη f ∘ (g ∘ h)
  id-r : ∀ {A B} {f : CatComb A B} → f ∘ id =βη f
  id-l : ∀ {A B} {f : CatComb A B} → id ∘ f =βη f
--- TERMINAL ---
  term : ∀ {A} {f : CatComb A unit} → f =βη !
--- PRODUCT ---
  first : ∀ {A B C} {f : CatComb C A} {g : CatComb C B} → p₁ ∘ ⟨ f , g ⟩ =βη f
  second : ∀ {A B C} {f : CatComb C A} {g : CatComb C B} → p₂ ∘ ⟨ f , g ⟩ =βη g
  ×-dist : ∀ {A B C D} {f : CatComb B C} {g : CatComb B D} {h : CatComb A B} → ⟨ f , g ⟩ ∘ h =βη ⟨ f ∘ h , g ∘ h ⟩
  pair-η : ∀ {A B} → ⟨ p₁ {A} {B} , p₂ {A} {B} ⟩ =βη id
--- EXPONENTIAL ---
  eval : ∀ {A B C} {f : CatComb (A × B) C} {g : CatComb A B} → app ∘ ⟨ cur f , g ⟩ =βη f ∘ ⟨ id , g ⟩
  cur-comp : ∀ {A B C D} {f : CatComb (A × B) C} {g : CatComb D A} → cur f ∘ g =βη cur (f ∘ ⟨ g ∘ p₁ , p₂ ⟩)
  cur-η : ∀ {A B} → cur {A ⇒ B} app =βη id {A ⇒ B}
  cur-cong : ∀ {A B C} {f g : CatComb (A × B) C} → f =βη g → cur f =βη cur g
--- COPRODUCT ---
  inl : ∀ {A B C D} {f : CatComb (A × B) D} {g : CatComb (A × C) D} → [ f , g ] ∘ ⟨ p₁ , i1 ∘ p₂ ⟩ =βη f
  inr : ∀ {A B C D} {f : CatComb (A × B) D} {g : CatComb (A × C) D} → [ f , g ] ∘ ⟨ p₁ , i2 ∘ p₂ ⟩ =βη g
  +-dist : ∀ {A B C D E} {f : CatComb (A × B) D} {g : CatComb (A × C) D} {h : CatComb D E} → h ∘ [ f , g ] =βη [ h ∘ f , h ∘ g ]
  copair-η : ∀ {A B C} → [ ⟨ p₁ {A} {B} , i1 ∘ p₂ ⟩ , ⟨ p₁ {A} {C} , i2 ∘ p₂ ⟩ ] =βη id
--- LIST OBJECT ---
  it-nil : ∀ {A X P x r} → it {A} {X} {P} x r ∘ ⟨ id , nil ∘ ! ⟩ =βη x
  it-rec : ∀ {A X P x r} → it {A} {X} {P} x r ∘ ⟨ id ∘ p₁ , cons ∘ p₂ ⟩ =βη r ∘ ⟨ p₁ , ⟨ p₁ ∘ p₂ , it {A} {X} {P} x r ∘ ⟨ p₁ , p₂ ∘ p₂ ⟩ ⟩ ⟩
--- MONAD ---
  monad-id-l : ∀ {Γ A B TA TB f} {a : CatComb Γ A} {ma : Monad {A} TA} {mb : Monad {B} TB} {s : SameMonad ma mb} → bind {s = s} ∘ ⟨ ret {m = ma} ∘ a , f ⟩ =βη app ∘ ⟨ f , a ⟩
  monad-id-r : ∀ {Γ A TA} {m : CatComb Γ TA} {ma : Monad {A} TA} {s : SameMonad ma ma} → bind {s = s} ∘ ⟨ m , cur (ret {m = ma} ∘ p₂) ⟩ =βη m
  monad-assoc : ∀ {Γ A B C TA TB TC g h} {m : CatComb Γ TA} {ma : Monad {A} TA} {mb : Monad {B} TB} {mc : Monad {C} TC} {sab : SameMonad ma mb} {sbc : SameMonad mb mc} → bind {s = sbc} ∘ ⟨ bind {s = sab} ∘ ⟨ m , g ⟩ , h ⟩ =βη bind {s = sameMonadTrans sab sbc} ∘ ⟨ m , cur (bind {s = sbc} ∘ ⟨ app ∘ ⟨ g ∘ p₁ , p₂ ⟩ , h ∘ p₁ ⟩) ⟩