    ------------------------------------------------------------------------
    -- 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 using (Size; ∞)
    open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
    open import Codata.Sized.Conat using (Conat; zero; suc)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures using (IsEquivalence)

    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)