open import Data.Product
open import Data.Product.Properties
open import Data.Unit
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Axiom.UniquenessOfIdentityProofs

module decEq (U : Set)(T : U → Set)
             (dec : (A : U) → (x y : T A) → Dec (x ≡ y)) where

-- universe containing unit type only
T⊤ : ⊤ → Set
T⊤ _ = ⊤

-- Because of uniqueness for ⊤ and functions, we can prove funext for
-- functions out of ⊤
funext⊤ : {A : Set} → {f g : ⊤ → A} → f tt ≡ g tt → f ≡ g
funext⊤ {A} {f} {g} = lem {A} {f tt} {g tt}
  where
   lem : {A : Set} → {ftt gtt : A} → ftt ≡ gtt → (λ (x : ⊤) → ftt) ≡ (λ x → gtt)
   lem refl = refl

open import SP U T ⊤ T⊤

mutual

  eq : (s : SP) → (x y : D s) → Dec (x ≡ y)
  eq s (inn x) (inn y) with eqArg s x y
  ... | yes p = yes (cong inn p)
  ... | no ¬p = no (λ innx≡inny → ¬p (inn-inj innx≡inny))

  eqArg : {s' : SP}(s : SP) → (x y : Arg s (D s')) → Dec (x ≡ y)
  eqArg done x y = yes refl
  eqArg (non-ind A s) (a , x) (a' , y) with dec A a a'
  eqArg (non-ind A s) (a , x) (a , y) | yes refl with eqArg (s a) x y
  eqArg (non-ind A s) (a , x) (a , y) | yes refl | yes x≡y =
    yes (cong (a ,_) x≡y)
  eqArg (non-ind A s) (a , x) (a , y) | yes refl | no ¬x≡y =
    no λ r → ¬x≡y (,-injectiveʳ-≡ (Decidable⇒UIP.≡-irrelevant (dec A)) r refl)
  eqArg (non-ind A s) (a , x) (a' , y)| no ¬p =
    no λ ax≡a'y → ¬p (cong proj₁ ax≡a'y)
  eqArg {s'} (ind A s) (f , x) (g , y) with eq s' (f _) (g _) | eqArg s x y
  ... | yes p | yes q = yes (cong₂ _,_ (funext⊤ p) q)
  ... | yes p | no q = no λ r → q (cong proj₂ r)
  ... | no p | q = no λ r → p (cong (λ h → h tt) (cong proj₁ r))