ET.agda?

ex.agda

module ex where

open import Level using (Level) renaming (suc to lsuc)
open import Data.Bool using (Bool; true; false)
open import Data.Nat
open import Data.Maybe using (Maybe; just; nothing)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_)
open import Relation.Nullary using (Dec; yes; no)
open import Data.Unit using (⊤; tt)

typeOf : {ℓ : Level} {A : Set ℓ}(x : A) → Set ℓ
typeOf {ℓ} {A} x = A

data T (A : Set) : Set where
  unT : (x : A) → T A

data ET {A : Set} : Set where
  unET : (T A) → ET

data Equal {A : Set} : (B : Set) → Set₁ where
  eq : (B : Set) → A ≡ B → Equal A
  ne : (B : Set) → A ≢ B → Equal A

typeEq : (a b : Set) → a ≡ b → Equal {a} b
typeEq ta .ta refl = eq ta refl

foo : {a : Set} → T a → T a → Bool
foo x y = true

bar : {A B : Set} → ET {A} → ET {B} → Maybe Bool
bar (unET (unT x)) (unET (unT y)) with typeEq (typeOf x) (typeOf y) {!!}
bar (unET (unT x)) (unET (unT y)) | eq B A≡B = just (foo (unT x) (unT y))
bar (unET (unT x)) (unET (unT y)) | ne B A≢B = nothing