# 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. May 31 at 7:12
• Unfortunately, I am not them. You can tell me the answer, I won’t disclose it to them, I promise 😂 May 31 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.) May 31 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? May 31 at 15:52
• @DanDoel Thanks! That works. Jun 1 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 ~> _≡_.