module Chain where

open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_)
open import Data.Product using (_×_; Σ; _,_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)

module _ {a} {A : Set a} (_R_ : A → A → Set a) where

    data Chain : A → A → ℕ → Set a where
        done : ∀ {a : A} → Chain a a 0
        step : ∀ {a₁ a₂ a₃ : A} {n : ℕ} → a₁ R a₂ → Chain a₂ a₃ n → Chain a₁ a₃ (suc n)

    concat : ∀ {a₁ a₂ a₃ : A} {n₁ n₂ : ℕ} → Chain a₁ a₂ n₁ → Chain a₂ a₃ n₂ → Chain a₁ a₃ (n₁ + n₂)
    concat done a₂a₃ = a₂a₃
    concat (step a₁Ra aa₂) a₂a₃ = step a₁Ra (concat aa₂ a₂a₃)

    empty-≡ : ∀ {a₁ a₂ : A} → Chain a₁ a₂ 0 → a₁ ≡ a₂
    empty-≡ done = refl

    Bounded : ℕ → Set a
    Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound

    Height : ℕ → Set a
    Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)