diff --git a/Chain.agda b/Chain.agda
new file mode 100644
index 0000000..b1cef95
--- /dev/null
+++ b/Chain.agda
@@ -0,0 +1,24 @@
+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)