------------------------------------------------------------------------
-- 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.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)

infix  _⊢_≈_
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  _⊢_≲_
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)