[Agda] Question about coinductive types

[Pierre Hyvernat]

Hello...

My question is more about the semantics of MLTT than just about Agda, 
but since that's where it originated, I guess this list is a good place 
to ask...

I've been writing some Agda code involving coinductive types and was 
wondering about the following:

  are functions definable in type theory* congruence wrt bisimilarity?

  *: say, MLTT with weakly terminal coalgebras for indexed containers

Am I right in expecting that to be true if we only consider functions 
between datatypes, ie exclude inductive families like intensional 
equality, which does not respect bisimilarity. (Equality is still needed 
to define bisimilarity though...)


Any pointer, suggestions?


The reason I ask is that writing out explicit bisimilarity proofs for 
general indexed containers in Agda is **very** painful. The more I can 
keep in some "meta" theory, the better...


Pierre
-- 
For every complex problem, there is a solution that is
simple, neat, and wrong.
    -- H. L. Mencken