module stlc.catComb.properities.propC where

open import stlc.catComb.betaeta

open import stlc.catComb.properities.common
open import stlc.catComb.properities.propA
open import stlc.catComb.properities.propB

open import stlc.monad.properities

open import stlc.value.properities

propC : ∀ {A B s s' t t'} {f g : CatComb A B} → ⟨ f ∣ s ⟩= t → ⟨ g ∣ s' ⟩= t' → f =βη g → s ≣ s' → t ≣ t'
propC x x₁ refl x₃ = ≣injective x x₁ x₃
propC x x₁ (sym x₂) x₃ = ≣sym (propC x₁ x x₂ (≣sym x₃))
propC {s = s} x x₁ (trans {g = g} x₂ x₄) x₃ with ⦅ t , ⦅ fst , snd ⦆ ⦆ ← propA g (propB s) with e₁ ← propC x fst x₂ ≣refl with e₂ ← propC fst x₁ x₄ x₃ = ≣trans e₁ e₂
propC (ev-comp x (ev-comp x₂ x₄)) (ev-comp (ev-comp x₁ x₆) x₅) assoc x₃ = propC x₄ x₅ refl (propC x₂ x₆ refl (propC x x₁ refl x₃))
propC (ev-comp ev-id x₂) x₁ id-r x₃ = propC x₂ x₁ refl x₃
propC (ev-comp x ev-id) x₁ id-l x₃ = propC x x₁ refl x₃
propC {t = ⟨⟩} x ev-unit term x₃ = unit
propC (ev-comp (ev-pair x x₄) ev-p1) x₁ first x₃ = propC x x₁ refl x₃
propC (ev-comp (ev-pair x x₄) ev-p2) x₁ second x₃ = propC x₄ x₁ refl x₃
propC (ev-comp x (ev-pair x₂ x₄)) (ev-pair (ev-comp x₁ x₆) (ev-comp x₅ x₇)) ×-dist x₃ = pair (propC x₂ x₆ refl (propC x x₁ refl x₃)) (propC x₄ x₇ refl (propC x x₅ refl x₃))
propC (ev-pair ev-p1 ev-p2) ev-id pair-η x₃ = x₃
propC (ev-comp (ev-pair ev-cur x₅) (ev-app x₁)) (ev-comp (ev-pair ev-id x₄) x₂) eval x₃ = propC x₁ x₂ refl (pair x₃ (propC x₅ x₄ refl x₃))
propC (ev-comp x ev-cur) ev-cur cur-comp x₃ = cur (λ {x₁ x₂ (ev-comp (ev-pair (ev-comp ev-p1 x₅) ev-p2) x₄) → propC x₂ x₄ refl (pair (propC x x₅ refl x₃) (_⇔_.from ≣⇔≣' x₁))})
propC {s = cur h s} {cur h' s'} ev-cur ev-id cur-η (cur x) = cur (λ {x₁ (ev-app x₂) x₃ → x x₁ x₂ x₃})
propC ev-cur ev-cur (cur-cong x₂) x₃ = cur (λ x x₁ x₄ → propC x₁ x₄ x₂ (pair x₃ (_⇔_.from ≣⇔≣' x)))
propC (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 ev-i1)) (ev-copair1 x₂)) x₁ inl x₃ = propC x₂ x₁ refl x₃
propC (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 ev-i2)) (ev-copair2 x₂)) x₁ inr x₃ = propC x₂ x₁ refl x₃
propC (ev-comp (ev-copair1 x) x₂) (ev-copair1 (ev-comp x₁ x₅)) +-dist (pair x₃ (inl x₄)) = propC x₂ x₅ refl (propC x x₁ refl (pair x₃ x₄))
propC (ev-comp (ev-copair2 x) x₂) (ev-copair2 (ev-comp x₁ x₅)) +-dist (pair x₃ (inr x₄)) = propC x₂ x₅ refl (propC x x₁ refl (pair x₃ x₄))
propC (ev-copair1 (ev-pair ev-p1 (ev-comp ev-p2 ev-i1))) ev-id copair-η (pair x₃ (inl x₄)) = pair x₃ (inl x₄)
propC (ev-copair2 (ev-pair ev-p1 (ev-comp ev-p2 ev-i2))) ev-id copair-η (pair x₃ (inr x₄)) = pair x₃ (inr x₄)
propC (ev-comp (ev-pair ev-id (ev-comp ev-unit ev-nil)) (ev-it-nil x₂)) x₁ it-nil x₃ = propC x₂ x₁ refl x₃
propC (ev-comp (ev-pair (ev-comp ev-p1 ev-id) (ev-comp ev-p2 ev-cons)) (ev-it-cons x x₆)) (ev-comp (ev-pair ev-p1 (ev-pair (ev-comp ev-p2 ev-p1) (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 ev-p2)) x₁))) x₂) it-rec (pair x₃ (pair x₄ x₅)) = propC x₆ x₂ refl (pair x₃ (pair x₄ (propC x x₁ refl (pair x₃ x₅))))
propC (ev-comp (ev-pair (ev-comp y (ev-ret y₃)) y₂) (ev-bind y₁)) (ev-comp (ev-pair z z₂) (ev-app z₁)) monad-id-l x₃ with e₁ ← propC y z₂ refl x₃ with e₂ ← propC y₂ z refl x₃ = monadIdL z₁ y₃ y₁ e₁ e₂
propC (ev-comp (ev-pair x ev-cur) (ev-bind x₁)) y monad-id-r x₃ with e ← propC x y refl x₃ = monadIdR x₁ e
propC (ev-comp (ev-pair {s₂ = cur f₁ s₁} (ev-comp (ev-pair {s₂ = cur f₂ s₂} x x₄) (ev-bind x₃)) x₂) (ev-bind x₁)) (ev-comp (ev-pair y ev-cur) (ev-bind y₁)) monad-assoc z with e ← propC x y refl z = monadAssoc y₁ x₁ x₂ x₃ x₄ z e