Generic Eq for term algebras in Agda

GEq.agda

open import Relation.Binary.PropositionalEquality
  renaming (cong to ap; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; subst to tr)
open import Data.Empty
open import Function hiding (_$_)
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)

infixr 3 _⇒_
infix 3 sort⇒_
infixl 2 _▶_
infixl 2 _$_ _$'_

data SigTy : Set
data Sig   : Set

data SigTy where
  sort   : SigTy
  sort⇒_ : SigTy → SigTy
  _⇒_    : Sig → SigTy → SigTy

data Sig where
  ∙   : Sig
  _▶_ : Sig → SigTy → Sig

data Var : Sig → SigTy → Set where
  vz : ∀ {Γ A} → Var (Γ ▶ A) A
  vs : ∀ {Γ A B} → Var Γ A → Var (Γ ▶ B) A

data Tm (Γ : Sig) : SigTy → Set where
  var  : ∀ {A} → Var Γ A → Tm Γ A
  _$_  : ∀ {A} → Tm Γ (sort⇒ A) → Tm Γ sort → Tm Γ A
  _$'_ : ∀ {Δ A} → Tm Γ (Δ ⇒ A) → Tm Δ sort → Tm Γ A

--------------------------------------------------------------------------------

El : Sig → Set
El Γ = Tm Γ sort

NatSig : Sig
NatSig = ∙ ▶ sort ▶ sort⇒ sort

ListSig : Sig → Sig
ListSig A = ∙ ▶ sort ▶ A ⇒ sort⇒ sort

zero : El NatSig
zero = var (vs vz)

suc : El NatSig → El NatSig
suc n = var vz $ n

nil : ∀ {A} → El (ListSig A)
nil = var (vs vz)

cons : ∀ {A} → El A → El (ListSig A) → El (ListSig A)
cons a as = var vz $' a $ as

--------------------------------------------------------------------------------

data Dec (A : Set) : Set where
  yes : A → Dec A
  no  : (A → ⊥) → Dec A

eqVar? : ∀ {Γ A B}(x : Var Γ A)(y : Var Γ B) → Dec (Σ (A ≡ B) λ p → tr (Var Γ) p x ≡ y)
eqVar? vz vz = yes (refl , refl)
eqVar? (vs x) (vs y) with eqVar? x y
... | yes (refl , refl) = yes (refl , refl)
... | no p              = no (λ {(refl , refl) → p (refl , refl)})
eqVar? vz (vs y) = no (λ {(refl , ())})
eqVar? (vs x) vz = no (λ {(refl , ())})

eq? : ∀ {Γ A B}(t : Tm Γ A)(u : Tm Γ B) → Dec (Σ (A ≡ B) λ p → tr (Tm Γ) p t ≡ u)
eq? (var x) (var x₁) with eqVar? x x₁
... | yes (refl , refl) = yes (refl , refl)
... | no  p = no λ {(refl , refl) → p (refl , refl)}
eq? (t $ t₁) (u $ u₁) with eq? t u
... | no p = no (λ {(refl , refl) → p (refl , refl)})
... | yes (refl , refl) with eq? t₁ u₁
... | no p = no λ {(refl , refl) → p (refl , refl)}
... | yes (refl , refl) = yes (refl , refl)
eq? (t $' t₁) (u $' u₁)with eq? t u
... | no p = no (λ {(refl , refl) → p (refl , refl)})
... | yes (refl , refl) with eq? t₁ u₁
... | no p = no λ {(refl , refl) → p (refl , refl)}
... | yes (refl , refl) = yes (refl , refl)
eq? (var x) (u $ u₁)    = no (λ {(refl , ())})
eq? (var x) (u $' u₁)   = no (λ {(refl , ())})
eq? (t $ t₁) (var x)    = no (λ {(refl , ())})
eq? (t $ t₁) (u $' u₁)  = no (λ {(refl , ())})
eq? (t $' t₁) (var x)   = no (λ {(refl , ())})
eq? (t $' t₁) (u $ u₁)  = no (λ {(refl , ())})

gEq : ∀ {A} → (x y : El A) → Dec (x ≡ y)
gEq x y with eq? x y
... | yes (refl , p) = yes p
... | no p           = no (λ q → p (refl , q))