module Tree where
open import Coinduction
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)
data Tree (A : Set) : Set where
leaf : Tree A
node : (l : ∞ (Tree A)) (x : A) (r : ∞ (Tree A)) → Tree A
map : ∀ {A B} → (A → B) → Tree A → Tree B
map f leaf = leaf
map f (node l x r) = node (♯ map f (♭ l)) (f x) (♯ map f (♭ r))
data _≈_ {A : Set} : (t₁ t₂ : Tree A) → Set where
leaf : leaf ≈ leaf
node : ∀ {l₁ l₂ x₁ x₂ r₁ r₂}
(l≈ : ∞ (♭ l₁ ≈ ♭ l₂)) (x≡ : x₁ ≡ x₂) (r≈ : ∞ (♭ r₁ ≈ ♭ r₂)) →
node l₁ x₁ r₁ ≈ node l₂ x₂ r₂
refl : ∀ {A} (t : Tree A) → t ≈ t
refl leaf = leaf
refl (node l x r) = node (♯ refl (♭ l)) PropEq.refl (♯ refl (♭ r))
trans : ∀ {A} {t₁ t₂ t₃ : Tree A} →
t₁ ≈ t₂ → t₂ ≈ t₃ → t₁ ≈ t₃
trans leaf leaf = leaf
trans (node l≈ x≡ r≈) (node l≈′ x≡′ r≈′) =
node (♯ trans (♭ l≈) (♭ l≈′)) (PropEq.trans x≡ x≡′)
(♯ trans (♭ r≈) (♭ r≈′))
map-cong : ∀ {A B} (f : A → B) {t₁ t₂ : Tree A} →
t₁ ≈ t₂ → map f t₁ ≈ map f t₂
map-cong f leaf = leaf
map-cong f (node l≈ x≡ r≈) =
node (♯ map-cong f (♭ l≈)) (PropEq.cong f x≡) (♯ map-cong f (♭ r≈))