Proof of the laws of the flow functor

Question

I am writing something similar to Stream. I can prove every law of a functor, but I can’t figure out how to prove it:

module Stream import Classes.Verified %default total codata MyStream a = MkStream a (MyStream a) mapStream : (a -> b) -> MyStream a -> MyStream b mapStream f (MkStream as) = MkStream (fa) (mapStream fs) streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (fx)) s = mapStream g (mapStream fs) streamFunctorComposition (MkStream xy) fg = let inductiveHypothesis = streamFunctorComposition yfg in ?streamFunctorCompositionStepCase ---------- Proofs ---------- streamFunctorCompositionStepCase = proof intros rewrite inductiveHypothesis trivial 

gives:

 *Stream> :total streamFunctorComposition Stream.streamFunctorComposition is possibly not total due to recursive path: Stream.streamFunctorComposition, Stream.streamFunctorComposition 

Is there a trick to prove functor laws over codata that also passes an integrity check?

Answer 1

I managed to get a little help in the IRC from Daniel Peebles (copumpkin) , who explained that the ability to use propositional equality over codates is usually not something normal allowed. He pointed out that one can define one's own equivalence relation, for example, as Agda defines for Data.Stream :

 data _≈_ {A} : Stream A → Stream A → Set where _∷_ : ∀ {xy xs ys} (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys 

I was able to directly translate this definition into Idris:

 module MyStream %default total codata MyStream a = MkStream a (MyStream a) infixl 9 =#= data (=#=) : MyStream a -> MyStream a -> Type where (::) : a = b -> Inf (as =#= bs) -> MkStream a as =#= MkStream b bs mapStream : (a -> b) -> MyStream a -> MyStream b mapStream f (MkStream as) = MkStream (fa) (mapStream fs) streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (fx)) s =#= mapStream g (mapStream fs) streamFunctorComposition (MkStream xy) fg = Refl :: streamFunctorComposition yfg 

And this easily passed the integrity check, because now we just make a simple coin.

This fact is a bit disappointing, as it seems to mean that we cannot define a VerifiedFunctor for our stream type.

Daniel also pointed out that observational-type theory allows propositional equality over codata, something that needs to be studied.