module stlc.monad.properities.monadIdL where

open import stlc.monad.properities.common

open import stlc.value.properities

monadIdL : ∀ {Γ A B TA TB s₁ s₂ s₃ s₄ s₅ t t'} {ma : Monad {A} TA} {mb : Monad {B} TB} {sab : SameMonad ma mb} {f : CatComb (Γ × A) TB} → ⟨ f ∣ s₁ , s₄ ⟩= t' → ⟨ getReturnImpl ma ∣ s₃ ⟩= s₅ → ⟨ getBindImpl sab ∣ s₅ , s₂ ⟩= t → s₃ ≣ s₄ → s₂ ≣ cur f s₁ → t ≣ t'
monadIdL {sab = exception} x ev-i1 (ev-comp ev-swap (ev-copair1 (ev-app z))) e₁ (cur x₁) = x₁ (_⇔_.to ≣⇔≣' e₁) z x
monadIdL {t' = cur g t} {sab = state} x₁ ev-cur ev-cur e₁ (cur e₂) = cur (λ { x (ev-bind-state (ev-app ev-swap) (ev-app x₂) x₄) x₃ → ≣injective x₄ (ev-app x₃) (pair (e₂ (_⇔_.to ≣⇔≣' e₁) x₂ x₁) (_⇔_.from ≣⇔≣' x))})
monadIdL {sab = nondeterminism} x (ev-comp (ev-pair ev-id (ev-comp ev-unit ev-nil)) ev-cons) (ev-comp ev-swap (ev-comp (ev-it-cons (ev-it-nil (ev-comp ev-unit ev-nil)) (ev-comp (ev-pair (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 ev-p1)) (ev-app z₄)) (ev-comp ev-p2 ev-p2)) ev-cons)) (ev-comp (ev-pair ev-unit ev-id) (ev-it-cons (ev-it-nil ev-nil) (ev-comp ev-p2 (ev-comp ev-swap z)))))) e₁ (cur e₂) rewrite uniqueness ev-it-id z = e₂ (_⇔_.to ≣⇔≣' e₁) z₄ x
monadIdL {t' = cur g t} {sab = continuation} x ev-cur ev-cur e₁ (cur e₂) = cur (λ { x₁ (ev-comp (ev-pair (ev-comp ev-p1 ev-p1) ev-cur) (ev-app (ev-comp ev-swap (ev-app (ev-comp (ev-pair (ev-comp (ev-pair (ev-comp ev-p1 (ev-comp ev-p1 ev-p2)) ev-p2) (ev-app x₂)) (ev-comp ev-p1 ev-p2)) x₄))))) x₃ → ≣injective x₄ (ev-app x₃) (pair (e₂ (_⇔_.to ≣⇔≣' e₁) x₂ x) (_⇔_.from ≣⇔≣' x₁))})