Trail equality

TrailEquality.agda

module TrailEquality where
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality

data Maybe (A : Set) : Set where
  just : (x : A) → Maybe A
  nothing : Maybe A

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

data Trail : ℕ → Set where
  beginning : Trail zero
  route : ∀{n} (f : ℕ → ℕ) (t : Trail n) → Trail (f n)

caseTrail : (P : ∀{n} → Trail n → Set)
  → P beginning
  → ({n : ℕ} (f : ℕ → ℕ) (t : Trail n) → P t → P (route f t))
  → ∀{n} (t : Trail n) → P t
caseTrail P pb pr beginning = pb
caseTrail P pb pr (route f t) = pr f t (caseTrail P pb pr t)

compare : ∀ {n} (x y : Trail n) → Maybe (x ≡ y)
compare beginning y = {!!}
compare (route f x) y = {!!}

-- compare : ∀ {m n} (x : Trail m) (y : Trail n) → m ≡ n → Maybe (x ≅ y)
-- compare beginning beginning refl = just refl
-- compare (route f x) (route g y) p = {!!}
-- compare _ _ _ = nothing

-- compare : ∀ {m n} (x : Trail m) (y : Trail n) → Maybe (x ≅ y)
-- compare beginning beginning = just refl
-- compare (route f x) (route g y) with compare x y
-- compare (route f x) (route g y) | just p = {!!}
-- compare (route f x) (route g y) | nothing = nothing
-- compare _ _ = nothing