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?

Improve this question
$\endgroup$
5
  • $\begingroup$ You almost sound like a student of mine who's currently formalizing this stuff as a class project. $\endgroup$
    – Andrej Bauer
    Commented May 31, 2023 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
    Commented May 31, 2023 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$
    – Andrej Bauer
    Commented May 31, 2023 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
    Commented May 31, 2023 at 15:52
  • $\begingroup$ @DanDoel Thanks! That works. $\endgroup$
    – Russoul
    Commented Jun 1, 2023 at 17:22

1 Answer 1

Reset to default
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 ~> _≑_.

Improve this answer
$\endgroup$

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