```------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for Conats
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --sized-types #-}

module Codata.Sized.Conat.Bisimilarity where

open import Level using (0ℓ)
open import Size
open import Codata.Sized.Thunk
open import Codata.Sized.Conat
open import Relation.Binary

infix 1 _⊢_≈_
data _⊢_≈_ i : (m n : Conat ∞) → Set where
zero : i ⊢ zero ≈ zero
suc  : ∀ {m n} → Thunk^R _⊢_≈_ i m n → i ⊢ suc m ≈ suc n

refl : ∀ {i m} → i ⊢ m ≈ m
refl {m = zero}  = zero
refl {m = suc m} = suc λ where .force → refl

sym : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ n ≈ m
sym zero     = zero
sym (suc eq) = suc λ where .force → sym (eq .force)

trans : ∀ {i m n p} → i ⊢ m ≈ n → i ⊢ n ≈ p → i ⊢ m ≈ p
trans zero      zero      = zero
trans (suc eq₁) (suc eq₂) = suc λ where .force → trans (eq₁ .force) (eq₂ .force)

isEquivalence : ∀ {i} → IsEquivalence (i ⊢_≈_)
isEquivalence = record
{ refl  = refl
; sym   = sym
; trans = trans
}

setoid : Size → Setoid 0ℓ 0ℓ
setoid i = record
{ isEquivalence = isEquivalence {i = i}
}

module ≈-Reasoning {i} where

open import Relation.Binary.Reasoning.Setoid (setoid i) public

infix 1 _⊢_≲_
data _⊢_≲_ i : (m n : Conat ∞) → Set where
z≲n : ∀ {n} → i ⊢ zero ≲ n
s≲s : ∀ {m n} → Thunk^R _⊢_≲_ i m n → i ⊢ suc m ≲ suc n

≈⇒≲ : ∀ {i m n} → i ⊢ m ≈ n → i ⊢ m ≲ n
≈⇒≲ zero     = z≲n
≈⇒≲ (suc eq) = s≲s λ where .force → ≈⇒≲ (eq .force)

≲-refl : ∀ {i m} → i ⊢ m ≲ m
≲-refl = ≈⇒≲ refl

≲-antisym : ∀ {i m n} → i ⊢ m ≲ n → i ⊢ n ≲ m → i ⊢ m ≈ n
≲-antisym z≲n      z≲n      = zero
≲-antisym (s≲s le) (s≲s ge) = suc λ where .force → ≲-antisym (le .force) (ge .force)

≲-trans : ∀ {i m n p} → i ⊢ m ≲ n → i ⊢ n ≲ p → i ⊢ m ≲ p
≲-trans z≲n       _         = z≲n
≲-trans (s≲s le₁) (s≲s le₂) = s≲s λ where .force → ≲-trans (le₁ .force) (le₂ .force)
```