# Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

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-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?

• You almost sound like a student of mine who's currently formalizing this stuff as a class project. Commented May 31, 2023 at 7:12
• Unfortunately, I am not them. You can tell me the answer, I wonβt disclose it to them, I promise π Commented May 31, 2023 at 7:44
• 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.) Commented May 31, 2023 at 12:17
• 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? Commented May 31, 2023 at 15:52
• @DanDoel Thanks! That works. Commented Jun 1, 2023 at 17:22

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 ~> _β‘_.