module Q where

open import Data.Nat
open import Data.Sum

data U : Set where
  NAT   : U 
  PLUS  : U → U → U

⟦_⟧ : U → Set
⟦ NAT ⟧         = ℕ
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧

record U• : Set where
  constructor •[_,_]
  field
    ∣_∣ : U
    • : ⟦ ∣_∣ ⟧

open U•

data _⟷_ : U• → U• → Set where
  swap1₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₁ (• t₁) ] ⟷ 
                           •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₂ (• t₁) ]
  swap2₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₂ (• t₂) ] ⟷ 
                           •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₁ (• t₂) ]

simplify : {t₁ t₂ : U•} → (c₁ : t₁ ⟷ t₂) → (t₂ ⟷ t₁)
simplify {•[ ._ , ._ ]} {•[ ._ , ._ ]} swap1₊ = {!!}
simplify {•[ ._ , ._ ]} {•[ ._ , ._ ]} swap2₊ = {!!} 

--simplify swap1₊ = swap2₊
--simplify swap2₊ = swap1₊