coinductives

[Vladimir Voevodsky]

Hello,

does anyone have an idea on how the following proof can be completed:

****

CoInductive stream ( T : UU ) := streamconstr : forall ( t : T ) ( s : stream T ) , stream T .

Definition streamfunct { T1 T2 : UU } ( f : T1 -> T2 ) ( s1 : stream T1 ) : stream T2 .
Proof. intros . cofix. destruct s1 as [ s1f s1r ] . exact ( streamconstr T2 ( f s1f ) streamfunct ) . Defined .

Lemma streamfunctid { T : UU } ( s : stream T ) : paths ( streamfunct ( idfun T ) s ) s .
Proof. intros . ???

****

V.

PS "idfun T := fun x : T => x" and "paths" is a notation for identity.

[Peter LeFanu Lumsdaine]

As I understand, one cannot complete this proof in Coq without an extra axiom.

Essentially, just like function types, coinductive types do not automatically have “the right equality type”.  One can define a type which “should be” their equality type — for functions, “pointwise equality”/“homotopy”; for coinduction, “coinductive equality”/“bisimulation”.  But then one cannot prove that this implies actual propositional equality; and, in general, one can hardly ever prove actual propositional equality in function types/coinductive types without adding an extensionality axiom saying that the desired and actual equality coincide (precisely, that the canonical map from propositional equality to the “desired equality type” is always an equivalence).
 
In the case of streams, “coinductive equality” is defined co-inductively, so as to satisfy:

    CoindEq s1 s2 = ((paths (head s1) (head s2)) * (CoindEq (tail s1) (tail s2)))

In your case, it is straightforward to show (without extra axioms)

    Lemma streamfunctid' { T : UU } ( s : stream T ) : CoindEq ( streamfunct ( idfun T ) s ) s .

and then the extensionality axiom, if you assume it, gets you the rest of the way.

–p.

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Michael Shulman]

Dan Licata claimed/conjectured here:
http://homotopytypetheory.org/2014/02/17/another-proof-that-univalence-implies-function-extensionality/
that just as univalence implies function extensionality, it should
also imply "coinductive extensionality". But he said he hadn't
checked the details, and those might depend on the particular choices
in an implementation of coinductive types (which I guess are different
in Coq and Agda, and even between versions of Agda).

The presentation of coinductive types in Coq and Agda is pretty weird,
because they aren't dual to inductive types. Categorically, one would
expect a coinductive definition to be defined by a set of
*destructors* rather than a set of constructors. Arguably, the reason
that equality isn't provably bisimulation is that from match and cofix
you can prove a corecursion principle, but not a "coinduction
principle". But to formulate a "coinduction principle" generally
that's dual to an induction principle, one seems to need some kind of
"codependent types".

Mike

[Andreas Abel]

On 04.06.2014 16:10, Michael Shulman wrote:
> The presentation of coinductive types in Coq and Agda is pretty weird,
> because they aren't dual to inductive types. Categorically, one would
> expect a coinductive definition to be defined by a set of
> *destructors* rather than a set of constructors.

Actually, Agda (development version, soon to be released as 2.4.0) now
has such coinductive types given by destructors.

{-# OPTIONS --copatterns #-}

record Stream A : Set where
coinductive
field head : A
tail : Stream A
open Stream

cons : {A : Set} -> A -> Stream A -> Stream A
head (cons a s) = a
tail (cons a s) = s

map : {A B : Set} -> (A -> B) -> Stream A -> Stream B
head (map f s) = f (head s)
tail (map f s) = map f (tails s)

See also http://www2.tcs.ifi.lmu.de/~abel/Streams2014Leiden.pdf

> Arguably, the reason
> that equality isn't provably bisimulation is that from match and cofix
> you can prove a corecursion principle, but not a "coinduction
> principle". But to formulate a "coinduction principle" generally
> that's dual to an induction principle, one seems to need some kind of
> "codependent types".

Type theory, as it is now, is biased toward induction and values. You
can abstract over values by not over eliminations. To be able to
isolate coinduction principles I guess we need a more symmetric type
theory that has first class eliminations.

Copatterns are a first, small step towards this symmetry.

Cheers,
Andreas

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andrea...@gu.se
http://www2.tcs.ifi.lmu.de/~abel/

[Paolo Capriotti]

On Wed, Jun 4, 2014 at 3:10 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> Dan Licata claimed/conjectured here:
> http://homotopytypetheory.org/2014/02/17/another-proof-that-univalence-implies-function-extensionality/
> that just as univalence implies function extensionality, it should
> also imply "coinductive extensionality". But he said he hadn't
> checked the details, and those might depend on the particular choices
> in an implementation of coinductive types (which I guess are different
> in Coq and Agda, and even between versions of Agda).

I don't see how this can be true, at least for Agda's coinductive
types. In fact, if N* denotes the type of co-natural numbers, then N*
+ 1 with the obvious coalgebra structure (mapping the extra point to
itself) satisfies the same rules for coinductive types as N*. In
particular, it is consistent that there are elements (like the
original infinity of N* and the extra point) that are "bisimilar", but
not equal, regardless of univalence.

I'm not familiar with Coq's coinductive types, but I'd be surprised if
this example were substantially different there.

Paolo

[Andrej Bauer]

> I don't see how this can be true, at least for Agda's coinductive
> types.

Where can we see the rules for coinductive types that Agda believes
in? The rules for N* would probably suffice, so perhaps a kind soul
can just post them for us.

With kind regards,

Andrej

[Altenkirch Thorsten]

Type Theory is not symmetric, indeed coinductive types can be derived from
function-extensionality and inductive types but this doesn't dualize.

We have to be careful not to see too many symmetries. Classical logic is
one example of a system which is too symmetric.

I think that the essential idea behind types like streams etc is the
ability to suspend computations, so that terms can be promoted to values.
This was the idea behind Agdas infty construct. When working on PiSigma we
looked at how to define propositional equality for the type of delayed
computations.

Pattern matching is about labelled sums and copatterns should be about
records not coinductive types. While inductive types usually start with a
coproduct and coinductive types with a product this sin't the case. Also
this identification makes it harder to integrate mixed
induction-coinduction which is more common than most people think.

I feel like the lone preacher in the dessert.. :-)

Thorsten

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

[Paolo Capriotti]

On Wed, Jun 4, 2014 at 4:14 PM, Andrej Bauer <andrej...@andrej.com> wrote:
>> I don't see how this can be true, at least for Agda's coinductive
>> types.
>
> Where can we see the rules for coinductive types that Agda believes
> in? The rules for N* would probably suffice, so perhaps a kind soul
> can just post them for us.

I believe the rules can be summed up by saying that N* is a weakly
terminal coalgebra of X \mapsto 1 + X such that the coalgebra map N*
-> 1 + N* has a section.

Paolo

[Paolo Capriotti]

On Wed, Jun 4, 2014 at 4:18 PM, Altenkirch Thorsten
<psz...@exmail.nottingham.ac.uk> wrote:
> Type Theory is not symmetric, indeed coinductive types can be derived from
> function-extensionality and inductive types but this doesn't dualize.

Why is this true? It's reasonable that you can do it for sets, but can
you really do it in general? For example, how can you define globular
types without coinduction? The presheaf representation runs into the
usual coherence problems.

Paolo

[Vladimir Voevodsky]

Thanks. I basically understand that. I tried to prove that univalence implies that the two concepts of equality coincide. The proof in the case of function extensionality which is in Foundations is very simple.

Given a homotopy h between functions f g : X -> Y we can form a function h : X -> pathspace Y whose composition with evalat0 : pathspace Y -> Y is (definitionally) f and composition with evalat1 is (definitionally) g. Using univalence we obtain that evalat0 = evalat1 and the proof is completed (BTW - no need for any extra universes other than the one to formulate univalence).

Thinking of stream T as an analog of ( nat -> T ) we can try to repeat the argument.

Consider ( stream ( pathsspace T ) ) . An object "e" in "bisimulation s1 s2" where ( s1 s2 : stream T ) easily defines an object "he" in ( stream ( pathsspace T ) )  just as homotopy between functions defines a function to the pathsspace.

Through "functoriality" of streams we have functions " ( stream ( pathsspace T ) -> ( stream T ) " corresponding to evalat0 and evalat1. One can show that univalence implies that these two functions from streams to streams are equal. 

The only problem is that the composition of "he" with the ( stream (evalat0 ) ) can not be proved to be equal to "s1" (and the same for evalat1 and "s2"). 

V.

[Vladimir Voevodsky]

BTW let me add that the reasoning of the previous email shows that

( univalence ) => ( some equality which is supposed to hold *definitionally* ) => ( bisimmulation = equality ) .

so the problem really is in the lack of some definitional equalities.

V.

On Jun 4, 2014, at 2:37 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

[Michael Shulman]

On Wed, Jun 4, 2014 at 8:43 AM, Paolo Capriotti <p.cap...@gmail.com> wrote:
> For example, how can you define globular
> types without coinduction?

tgtype : nat -> Type1
tgtype 0 = Unit
tgtype (S n) = Sum[ A : Type ] ((a b : A) -> tgtype n)

trunc : (n : nat) -> tgtype (S n) -> tgtype n
trunc 0 _ = tt
trunc (S n) (A , hom) = (A , lambda a b -> trunc (hom a b))

gtype : Type1
gtype = Sum[ G : (n : nat) -> tgtype n ] ((n : nat) -> trunc n (G (S n)) == G n)

[Andreas Abel]

At least in the latest development version, your example termination
checks...

On 04.06.2014 17:52, Dan Licata wrote:
> Hi Andreas,
>
> When I tried copatterns (in the development version as of April) and I tried to write
>
> test : ∀ {A} → Stream (A × A) → Stream A
> Stream.head (test s) = fst (Stream.head s)
> Stream.tail (test s) = test (Stream.tail s)
>
> it didn't termination check. Is this a bug? Is my development version too out of date? Am I using it wrong?
>
> -Dan

[Andreas Abel]

If you forget to declare Stream as "coinductive", it does not
termination check.

On 04.06.2014 17:52, Dan Licata wrote:
> Hi Andreas,
>
> When I tried copatterns (in the development version as of April) and I tried to write
>
> test : ∀ {A} → Stream (A × A) → Stream A
> Stream.head (test s) = fst (Stream.head s)
> Stream.tail (test s) = test (Stream.tail s)
>
> it didn't termination check. Is this a bug? Is my development version too out of date? Am I using it wrong?
>
> -Dan
>
> On Jun 4, 2014, at 10:52 AM, Andreas Abel <andrea...@ifi.lmu.de> wrote:
>

[Paolo Capriotti]

Ah, nice! So, can something like this really be done in general?

Paolo

[Vladimir Voevodsky]

> I feel like the lone preacher in the dessert.. :-)

Don't. While I do not understand some of the CS stuff in your post I was happy to read this:

> We have to be careful not to see too many symmetries. Classical logic is
> one example of a system which is too symmetric.

In my opinion closed model structures is is another such example....

Vladimir.

[Michael Shulman]

I don't know. The most general statement I know of is that in a
Pi-pretopos with W-types one can construct M-types. But I don't know
to what extent all coinductive definitions can be reduced to M-types,
even in extensional type theory, let alone intensional type theory.
Maybe someone else does.

[Dan Doel]

On Wed, Jun 4, 2014 at 11:18 AM, Altenkirch Thorsten <psz...@exmail.nottingham.ac.uk> wrote:

I feel like the lone preacher in the dessert.. :-)

​I don't really understand why. :) What you're talking about seems widely implemented (Agda, Coq?, probably Idris). And the only thing I know about that (properly, at least) implements the coinduction you'd get by dualizing induction in category theory is Charity, although I have to take the web site's word for it, because I've never installed Charity, nor met anyone who has.

​Coinduction seems almost unexplored practically relative to the 'put a checker on top of partial recursive domains with delaying' that most things actually implement.

It's also quite common for people to think that inductive and coinductive should be synonymous with eager and delayed, even though in a total language, one can have inductive types with delays (though not eager coinductives in general), and there are certainly uses for those.

-- Dan

[Paolo Capriotti]

On Wed, Jun 4, 2014 at 5:13 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> I don't know. The most general statement I know of is that in a
> Pi-pretopos with W-types one can construct M-types.

So you would need an (infinity,1) version of this, right? Anyway, now
that you've showed me how to construct globular types, I'm starting to
believe that it should be possible to do the same for any M-type.

> But I don't know
> to what extent all coinductive definitions can be reduced to M-types,
> even in extensional type theory, let alone intensional type theory.

What is a "coinductive definition" then? So far I've always taken
"coinductive type" to be a synonym of (indexed) M-type.

Paolo

[Altenkirch Thorsten]

From: Dan Doel <dan....@gmail.com>
Date: Wed, 4 Jun 2014 17:17:57 +0100
To: Thorsten Altenkirch <psz...@exmail.nottingham.ac.uk>
Cc: Andreas Abel <andrea...@ifi.lmu.de>, Michael Shulman <shu...@sandiego.edu>, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>, Vladimir Voevodsky <vlad...@ias.edu>, homotopytypetheory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] coinductives

On Wed, Jun 4, 2014 at 11:18 AM, Altenkirch Thorsten <psz...@exmail.nottingham.ac.uk> wrote:

I feel like the lone preacher in the dessert.. :-)

​I don't really understand why. :)

Maybe I live in a different dessert :-)

What you're talking about seems widely implemented (Agda, Coq?, probably Idris). And the only thing I know about that (properly, at least) implements the coinduction you'd get by dualizing induction in category theory is Charity, although I have to take the web site's word for it, because I've never installed Charity, nor met anyone who has.

​Coinduction seems almost unexplored practically relative to the 'put a checker on top of partial recursive domains with delaying' that most things actually implement.

It's also quite common for people to think that inductive and coinductive should be synonymous with eager and delayed, even though in a total language, one can have inductive types with delays (though not eager coinductives in general), and there are certainly uses for those.

I think the naïve intuition is correct also in a total setting. That is infinite computations are achieved by turning terms into values and evaluate them on demand. 

In a way this is already what lambda does for functions in a different way. We construct infinite objects such as functions and streams by using computations. However, we don't want to identify the objects with the actual description (this is the point of extensionality). 

Also recursive types themselves can be seen as coinductive objects this way, that is in Agda you can actual define an inductive type like natural numbers via a recursively defined object with delay (you need to switch on guarded-type-constructors). 

Obviously I like category theory and I think the symmetry of induction and coinduction is improtant. However, I don't think this is the correct primitive to introduce infinite objects.

Thorsten

-- Dan

[Michael Shulman]

On Wed, Jun 4, 2014 at 9:29 AM, Paolo Capriotti <p.cap...@gmail.com> wrote:
>> I don't know. The most general statement I know of is that in a
>> Pi-pretopos with W-types one can construct M-types.
>
> So you would need an (infinity,1) version of this, right?

Yes, plus whatever strictification is required by the rules of type theory.

> What is a "coinductive definition" then? So far I've always taken
> "coinductive type" to be a synonym of (indexed) M-type.

I meant, whatever is allowed by Coq or Agda (which is obviously a
varying and moving target). For instance, it's not obvious to me how
to write the coinductive definition of globular types as an M-type,
since it uses type dependency.

Mike

[Paolo Capriotti]

On Wed, Jun 4, 2014 at 5:54 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> For instance, it's not obvious to me how
> to write the coinductive definition of globular types as an M-type,
> since it uses type dependency.

I'm not sure what you mean. What is wrong with A = Type, B(X) = X * X ?

Paolo

[Michael Shulman]

Yes, you're right of course. I feel that there was some kind of
coinductive definition that I couldn't see how to write as an M-type,
but right now I'm not thinking of it.

[Paolo Capriotti]

On Wed, Jun 4, 2014 at 7:18 PM, Dan Licata <dli...@wesleyan.edu> wrote:
> Hi Paolo,
>
> Do you have any sense for which of the postulates/holes in
>
> https://github.com/dlicata335/hott-agda/blob/new-without-k/computational-interp/ua-implies-funext/Stream.agda
>
> would break for your counterexample? I don't really see how to reconcile it with my partial proof (or maybe we're just not defining things in the same way?).

I haven't read the whole proof, but I think you'd have a problem
proving map-id already, as Peter argued above.

My intuition is as follows: imagine your Stream A type being realised
as (N -> A) + (N -> A). where the eliminator only takes values in the
first summand, say. Then map-id is false, because `map id` is not the
identity, but the function which collapses both summands into the
first.

One way to make the whole thing go through is to postulate uniqueness
of the eliminator (as Thorsten suggested). Here is my proof of this
fact (slightly obfuscated by the extra generality of indexed M-types):
http://paolocapriotti.com/agda-base/container.m.extensionality.html.

Paolo

[Peter LeFanu Lumsdaine]

It is possible, I think, to define globular types without coinduction (I think Thorsten taught this to me in around 2009, if I remember right?).  This isn’t a fully satisfactory answer to your question, though, since I don’t know how to see this definition as some kind of routine translation of coinductive definitions into terms of functional extensionality + inductive types.

I should apologise, by the way: I will write in a hybrid of Coq and Agda notation, since I am a bit out of practice with both, and I switched OS’s recently and don’t have either running smoothly.

Define n-globular types “FinGlob n” inductively:

FinGlob :: N -> Type

FinGlob 0 = Type

FinGlob (n+1) = { X :: Type & X -> X -> FinGlob n }

Now, define truncation:

trunc :: (n:N) -> (X : FinGlob (n+1)) -> (FinGlob n)

trunc 0 (X0,_) = X0

trunc n (X0,Xrest) = (X0 , \x y -> trunc (Xrest x y))

Now, define un-truncated globular types as the limit of this sequence:

Glob :: Type

Glob = { X :: forall (n:N), FinGlob n

       & forall (n:N), trunc (X (n+1)) == X n }

If I’m not mis-remembering, this provably implements the specification of the coinductive definition of globular sets — there are no coherence issues.

On the other hand, as I said above, it’s indeed not obvious that this approach generalises to arbitrary coinductive types.

–p.

[Peter LeFanu Lumsdaine]

Oops, I apologise — the discussion had moved on while I was away from the internet, and I didn’t see the later replies before sending my last message, so it was a bit obsolete!

–p.

[Paolo Capriotti]

Thanks Peter,
this is indeed the same approach as the one Mike showed.

Maybe I'm being naive, but it seems to me that it should actually be
pretty straightforward to generalise this to arbitrary M-types. This
is what I have so far (non-indexed case only, incomplete proofs):
https://gist.github.com/pcapriotti/3985cc9a07daf3f304fd

Paolo

[Peter LeFanu Lumsdaine]

By the way, I believe that Benedikt Ahrens and Régis Spadotti have been working on these questions recently, and have nailed down fairly nicely what one has to add to Coq-like coinductive types for the result to be equivalent to (homotopy-)terminal coalgebras.  I don’t remember precisely what Benedikt told me their answer was, but I think it was a version of the statement that bisimulation implies equality.

–p.

[Bas Spitters]

You mean this one?
http://www.pps.univ-paris-diderot.fr/types2014/abstract-2.pdf
http://www.pps.univ-paris-diderot.fr/types2014/slides-2.pdf

On Wed, Jun 4, 2014 at 9:36 PM, Peter LeFanu Lumsdaine

[Martin Escardo]

On 04/06/14 12:57, Vladimir Voevodsky wrote:
> does anyone have an idea on how the following proof can be completed:
>
> ****
>
> CoInductive stream ( T : UU ) := streamconstr : forall ( t : T ) ( s : stream T ) , stream T .
>
> Definition streamfunct { T1 T2 : UU } ( f : T1 -> T2 ) ( s1 : stream T1 ) : stream T2 .
> Proof. intros . cofix. destruct s1 as [ s1f s1r ] . exact ( streamconstr T2 ( f s1f ) streamfunct ) . Defined .
>
> Lemma streamfunctid { T : UU } ( s : stream T ) : paths ( streamfunct ( idfun T ) s ) s .
> Proof. intros . ???

With someone on Monday over lunch we thought we had solved a more
general version of the question you ask today, using function
extensionality. As I was writing it down below, I realized it is not a
solution (or doesn't seem to be one). However, let me explain what the
problem is.

You can show that your two streams are bisimilar. This can be
explained with a function

r : stream T -> (N -> T)

defined by recursion on N in the obvious way. Call the elements of the
function type (N -> T) "sequences". Then the streams x and y are
bisimilar iff the sequence r x is pointwise equal to the sequence r y,
and hence r x = r y by funext. We can prove that your two streams of
the lemma are mapped to the same sequence (of course).

Next define another obvious function

s : (N -> T) -> stream T

by corecursion on the stream T. I claim that the composite

r o s : (N -> T) -> (N -> T)

is the identity (use induction on N and funext).

So the type of sequences is a retract of the type of streams.

Moreover, you can show (using induction on N and funext), that the
type of sequences is the final coalgebra of the functor T x (-). So,
morally, it is sequences that should arise (isomorphically) as the
solution of the coinductive definition. If this were the case, you
would also get that the composite

s o r : stream T -> stream T

is the identity. But, as far as I can see, it is only pointwise
bisimilar to the identity, which of course follows from the fact that
r o s = id and so doesn't add anything new. (And this was the mistake
in the lunch time discussion with one of our colleagues here at the
IHP: we thought we had argued that the composite s o r is also the
identity, using funext.)

I had similar problems when trying to define "the one-point
compactification of N" as the final coalgebra of 1+(-) using
coinduction in Agda. In the end, I constructed it explicitly as the
type of decreasing binary sequences as is usual in constructive
mathematics, and I proved that bisimilarity is equivalent to equality
using funext.

Martin

[Benedikt Ahrens]

Peter is referring to [1] where we prove that a set of axioms (see
Module Type MAxioms) is equivalent to the existence of a
(homotopy)-terminal coalgebra (see Module Type MHasTerminal).

More specifically, Peter refers to the axiom

Axiom coind : ∀ (R : M A B → M A B → Prop)
(R_destr : ∀ {s₁ s₂}, R s₁ s₂ → Feq R (destr s₁) (destr s₂)),
∀ {s₁ s₂}, R s₁ s₂ → s₁ = s₂.


To make the connection to IMLTT: there is a similar equivalence proved
between axioms postulating a largest bisimulation relation and existence
of a terminal coalgebra of a polynomial functor on setoids [2].

Finally, in the presence of quotients (not hSet-quotients, but
traditional axiomatic ones, I am not sure if that makes a difference)
and funext, the sets of axioms of [1] and [2] are equivalent, see [3].


[1]
https://bitbucket.org/rs-/coalg-proofs/src/912545757c3ca8602821ede54532787ad26f9366/Category/M_Terminal_Axioms_Type.v

[2]
https://bitbucket.org/rs-/coalg-proofs/src/912545757c3ca8602821ede54532787ad26f9366/Category/M_Terminal_Axioms.v

[3]
https://bitbucket.org/rs-/coalg-proofs/src/912545757c3ca8602821ede54532787ad26f9366/Category/M_Quotient.v

[Vladimir Voevodsky]

Thanks. This is also what I understand to be the case. BTW I have defined bisimulation differently:

CoInductive bisim { T : UU } ( s1 s2 : stream T ) := bisimconstr : forall ( eh : paths ( head s1 ) ( head s2 ) ) ( et : bisim ( tail s1 ) ( tail s2 ) ) , bisim s1 s2 .

V.

[Martin Escardo]

On 04/06/14 21:24, Benedikt Ahrens wrote:
>
> Peter is referring to [1] where we prove that a set of axioms (see
> Module Type MAxioms) is equivalent to the existence of a
> (homotopy)-terminal coalgebra (see Module Type MHasTerminal).
>
> More specifically, Peter refers to the axiom
>
> Axiom coind : ∀ (R : M A B → M A B → Prop)
> (R_destr : ∀ {s₁ s₂}, R s₁ s₂ → Feq R (destr s₁) (destr s₂)),
> ∀ {s₁ s₂}, R s₁ s₂ → s₁ = s₂.

You postulate that bisimilarity implies equality, which, in the
terminology of my message, amounts to saying that s o r is the identity,
and hence sequences and streams form isomorphic types, solving
Vladimir's problem. Right? Then, if I understand you correctly, you are
solving Vladimir's problem by postulating its solution. Or please tell
me if I have misinterpreted what you say.

Martin

>
>
> To make the connection to IMLTT: there is a similar equivalence proved
> between axioms postulating a largest bisimulation relation and existence
> of a terminal coalgebra of a polynomial functor on setoids [2].
>
> Finally, in the presence of quotients (not hSet-quotients, but
> traditional axiomatic ones, I am not sure if that makes a difference)
> and funext, the sets of axioms of [1] and [2] are equivalent, see [3].
>
>
> [1]
> https://bitbucket.org/rs-/coalg-proofs/src/912545757c3ca8602821ede54532787ad26f9366/Category/M_Terminal_Axioms_Type.v
>
> [2]
> https://bitbucket.org/rs-/coalg-proofs/src/912545757c3ca8602821ede54532787ad26f9366/Category/M_Terminal_Axioms.v
>
> [3]
> https://bitbucket.org/rs-/coalg-proofs/src/912545757c3ca8602821ede54532787ad26f9366/Category/M_Quotient.v
>
>
> On 06/04/2014 09:45 PM, Bas Spitters wrote:
>> You mean this one?
>> http://www.pps.univ-paris-diderot.fr/types2014/abstract-2.pdf
>> http://www.pps.univ-paris-diderot.fr/types2014/slides-2.pdf
>>
>> On Wed, Jun 4, 2014 at 9:36 PM, Peter LeFanu Lumsdaine
>> <p.l.lu...@gmail.com> wrote:
>>> By the way, I believe that Benedikt Ahrens and Régis Spadotti have been
>>> working on these questions recently, and have nailed down fairly nicely what
>>> one has to add to Coq-like coinductive types for the result to be equivalent
>>> to (homotopy-)terminal coalgebras. I don’t remember precisely what Benedikt
>>> told me their answer was, but I think it was a version of the statement that
>>> bisimulation implies equality.
>

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Martin Escardo]

On 04/06/14 21:53, Vladimir Voevodsky wrote:
> Thanks. This is also what I understand to be the case. BTW I have defined bisimulation differently:
>
> CoInductive bisim { T : UU } ( s1 s2 : stream T ) := bisimconstr : forall ( eh : paths ( head s1 ) ( head s2 ) ) ( et : bisim ( tail s1 ) ( tail s2 ) ) , bisim s1 s2 .

Yes. I wanted to avoid technicalities in the discussion. The little
unspoken lemma in my message is that x and y are bimisilar in the
(standard) sense you define is equivalent to r x = r y using my
(standard) retraction.

Martin

[Martin Escardo]

Another remark is this:

If you define streams to be sequences,

stream T = (N -> T),

not only can you prove that the type stream T is the final coalgebra
of the functor T x (-) (using funext), as I said in the previous
message, but also you can prove, with your definition of bisimilarity,
that bimisiliarity is equivalent to propositional equality (in Agda,
in the pure MLTT fragment of Agda plus funext, and so in Coq+funext
too).

I say this to emphasize that the (apparent) failure of the coincidence
of bisimilarity with equality is not an intrinsic problem of identity
types versus bisimilarity, but an oddity of the way
coinduction/recursion is (attempted to be) realized in Coq and
Agda. Much more thought is needed to include coinduction in type
theory in a proper way. In any case, most (all?) coinductive types I
can think of are anyway already definable in type theory from first
principles, plus funext.

It is disturbing that the addition of coinduction as a primitive
doesn't behave as it should (even when one does have funext, as in
HoTT) and *can* (by direct construction from what we already have in
our type theory with funext).

Martin

[Benedikt Ahrens]

On 06/04/2014 10:54 PM, Martin Escardo wrote:
>
> On 04/06/14 21:24, Benedikt Ahrens wrote:
>>
>> Peter is referring to [1] where we prove that a set of axioms (see
>> Module Type MAxioms) is equivalent to the existence of a
>> (homotopy)-terminal coalgebra (see Module Type MHasTerminal).
>>
>> More specifically, Peter refers to the axiom
>>
>> Axiom coind : ∀ (R : M A B → M A B → Prop)
>> (R_destr : ∀ {s₁ s₂}, R s₁ s₂ → Feq R (destr s₁) (destr s₂)),
>> ∀ {s₁ s₂}, R s₁ s₂ → s₁ = s₂.
>
> You postulate that bisimilarity implies equality, which, in the
> terminology of my message, amounts to saying that s o r is the identity,
> and hence sequences and streams form isomorphic types, solving
> Vladimir's problem. Right? Then, if I understand you correctly, you are
> solving Vladimir's problem by postulating its solution. Or please tell
> me if I have misinterpreted what you say.

Your interpretation seems entirely adequate to me.

Benedikt

[Peter LeFanu Lumsdaine]

On Wed, Jun 4, 2014 at 11:51 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>
> I say this to emphasize that the (apparent) failure of the coincidence
> of bisimilarity with equality is not an intrinsic problem of identity
> types versus bisimilarity, but an oddity of the way
> coinduction/recursion is (attempted to be) realized in Coq and
> Agda.

[…]

> It is disturbing that the addition of coinduction as a primitive doesn't behave as it should (even when one does have funext, as in HoTT) and *can* (by direct construction from what we already have in our type theory with funext).

I also found this a bit weird earlier, but I’ve somewhat come round to it now.  It’s not so different, after all, from the situation with function types: one can consistently have two Pi-type constructors in the theory simultaneously, with one extensionality holding for one but failing for the other.  And we don’t conclude from that that there’s anything wrong with the rules for Pi-types — or, at least, not apart from possibly “extensionality should be added to them”.

–p.