------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise equality of colists
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --guardedness #-}
module Codata.Musical.Colist.Bisimilarity where
open import Codata.Musical.Colist.Base using (Colist; []; _∷_; map)
open import Codata.Musical.Notation using (♭; ♯_; ∞)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _=[_]⇒_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive)
private
variable
a b : Level
A : Set a
B : Set b
-- xs ≈ ys means that xs and ys are equal.
infix 4 _≈_
data _≈_ {A : Set a} : Rel (Colist A) a where
[] : [] ≈ []
_∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys
infixr 5 _∷_
-- The equality relation forms a setoid.
setoid : Set a → Setoid _ _
setoid A = record
{ Carrier = Colist A
; _≈_ = _≈_
; isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
}
}
where
refl : Reflexive _≈_
refl {[]} = []
refl {x ∷ xs} = x ∷ ♯ refl
sym : Symmetric _≈_
sym [] = []
sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)
trans : Transitive _≈_
trans [] [] = []
trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)
module ≈-Reasoning where
import Relation.Binary.Reasoning.Setoid as EqR
private
open module R {a} {A : Set a} = EqR (setoid A) public
-- map preserves equality.
map-cong : (f : A → B) → _≈_ =[ map f ]⇒ _≈_
map-cong f [] = []
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4