2
$\begingroup$

Suppose we work inside MLTT with equality reflection (extensional MLTT). Assume I postulate existence of Streams as final co-algebra for the suitable functor.

Is that enough to prove the bisimulation principle:


R : Stream A β†’ Stream A β†’ π•Œ
R-head : (xs ys : Stream A) β†’ R xs ys β†’ xs.head ≑ ys.head
R-tail : (xs ys : Stream A) β†’ R xs ys β†’ R xs.tail ys.tail 
---------------------------------------------------------
bisim : (xs ys : Stream A) β†’ R xs ys β†’ xs ≑ ys

If not, what extra must be assumed to prove it? Do I need to assume a co-induction principle for (xs ≑ ys)? As in assume that (_ ≑(Stream A) _) is the final indexed co-algebra or something?

$\endgroup$
5
  • $\begingroup$ You almost sound like a student of mine who's currently formalizing this stuff as a class project. $\endgroup$ May 31 at 7:12
  • $\begingroup$ Unfortunately, I am not them. You can tell me the answer, I won’t disclose it to them, I promise πŸ˜‚ $\endgroup$
    – Russoul
    May 31 at 7:44
  • 1
    $\begingroup$ The other day the students asked how to derive equality from bisimilarity. The answer given by Danel Ahman was: "You will need a postulate for that." (This was Agda.) $\endgroup$ May 31 at 12:17
  • 1
    $\begingroup$ I believe the standard approach is to consider $Ξ£_{xs,ys : \mathsf{Stream}_A} R\ xs\ ys$. This can be given a 'simultaneous step' coalgebra structure due to the premises on $R$. Then both projections ($xs$ and $ys$) are coalgebra homomorphisms to $\mathsf{Stream}_A$, so must be equal (by finality). So, did you try that? $\endgroup$
    – Dan Doel
    May 31 at 15:52
  • $\begingroup$ @DanDoel Thanks! That works. $\endgroup$
    – Russoul
    Jun 1 at 17:22

1 Answer 1

3
$\begingroup$

The universal property of final coalgebras can be formalized as

unique-ana : βˆ€ (f : A β†’ B Γ— A) (g : A β†’ Stream B) β†’
  unfold ∘ g ≑ mapβ‚‚ g ∘ f β†’ g ≑ ana f

where

unfold : Stream B β†’ B Γ— Stream B   -- Final coalgebra
ana : (A β†’ B Γ— A) β†’ A β†’ Stream B   -- Anamorphism of a coalgebra
mapβ‚‚ : (A β†’ S) β†’ B Γ— A β†’ B Γ— S     -- The functor (B Γ—_)

Assuming functional extensionality (which you have in ExtMLTT), unique-ana is indeed equivalent to the bisimulation principle, aka. stream extensionality:

stream-ext : s β‰ˆ t β†’ s ≑ t

where

_β‰ˆ_ : {A : Set} β†’ Stream A β†’ Stream A β†’ Type₁  -- Bisimilarity
s β‰ˆ t = Ξ£[ R ∈ (Stream _ β†’ Stream _ β†’ Type) ]
  R s t Γ— (βˆ€ {u v} β†’ R u v β†’ (u .hd ≑ v .hd) Γ— R (u .tl) (v .tl)))

The trick is to view a stream s : Stream A as a coalgebra index s : β„• β†’ A Γ— β„•, which given an index i returns the i-th element of s and the incremented index i+1. Define drop i s as the stream after dropping the first i elements of s. The universal property unique-ana tells you that drop i s = ana (index s) i. Then s β‰ˆ t β†’ s ≑ t can be proved as follows:

s
≑ drop 0 s         -- by definition
≑ ana (index s) 0  -- by unique-ana
≑ ana (index t) 0  -- by fun-ext and s β‰ˆ t
≑ drop 0 t         -- by unique-ana
≑ t                -- by definition

Note that the bisimulation principle is a coinduction principle for the identity type on streams: in your formulation, the premises above the bar is a coalgebra (an object R and a morphism R ~> F R for a certain endofunctor F) and the conclusion is the anamorphism R ~> _≑_.

$\endgroup$

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.