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?

  • $\begingroup$ You almost sound like a student of mine who's currently formalizing this stuff as a class project. $\endgroup$ 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$ 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


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


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


_β‰ˆ_ : {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:

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


Your Answer

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

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