316 views

Skip to first unread message

Jun 4, 2014, 7:57:22 AM6/4/14

to homotopytypetheory, Prof. 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.

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.

Jun 4, 2014, 8:37:33 AM6/4/14

to Vladimir Voevodsky, homotopytypetheory

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.

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.

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

Jun 4, 2014, 10:10:41 AM6/4/14

to Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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

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

Jun 4, 2014, 10:52:34 AM6/4/14

to Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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

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".

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/

Jun 4, 2014, 10:53:59 AM6/4/14

to Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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
> 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).

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

Jun 4, 2014, 11:14:49 AM6/4/14

to homotopytypetheory

> 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
> types.

in? The rules for N* would probably suffice, so perhaps a kind soul

can just post them for us.

With kind regards,

Andrej

Jun 4, 2014, 11:26:26 AM6/4/14

to Andreas Abel, Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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.

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

Jun 4, 2014, 11:29:47 AM6/4/14

to Andrej Bauer, homotopytypetheory

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

terminal coalgebra of X \mapsto 1 + X such that the coalgebra map N*

-> 1 + N* has a section.

Paolo

Jun 4, 2014, 11:44:02 AM6/4/14

to Altenkirch Thorsten, Andreas Abel, Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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

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

Jun 4, 2014, 11:49:54 AM6/4/14

to Peter LeFanu Lumsdaine, Prof. Vladimir Voevodsky, homotopytypetheory

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.

Jun 4, 2014, 11:52:02 AM6/4/14

to Peter LeFanu Lumsdaine, Prof. Vladimir Voevodsky, homotopytypetheory

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:

Jun 4, 2014, 11:52:48 AM6/4/14

to Paolo Capriotti, homotopytypetheory

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
> For example, how can you define globular

> types without coinduction?

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)

Jun 4, 2014, 12:05:06 PM6/4/14

to Dan Licata, Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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

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

Jun 4, 2014, 12:06:53 PM6/4/14

to Dan Licata, Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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:

>

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:

>

Jun 4, 2014, 12:07:35 PM6/4/14

to Michael Shulman, homotopytypetheory

Paolo

Jun 4, 2014, 12:10:11 PM6/4/14

to Altenkirch Thorsten, Prof. Vladimir Voevodsky, Andreas Abel, Michael Shulman, Peter LeFanu Lumsdaine, homotopytypetheory

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

Vladimir.

Jun 4, 2014, 12:13:37 PM6/4/14

to Paolo Capriotti, homotopytypetheory

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.

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.

Jun 4, 2014, 12:17:58 PM6/4/14

to Altenkirch Thorsten, Andreas Abel, Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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

Jun 4, 2014, 12:30:06 PM6/4/14

to Michael Shulman, homotopytypetheory

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

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.

"coinductive type" to be a synonym of (indexed) M-type.

Paolo

Jun 4, 2014, 12:50:19 PM6/4/14

to Dan Doel, Andreas Abel, Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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

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

Jun 4, 2014, 12:54:55 PM6/4/14

to Paolo Capriotti, homotopytypetheory

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

> What is a "coinductive definition" then? So far I've always taken

> "coinductive type" to be a synonym of (indexed) M-type.

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

Jun 4, 2014, 1:08:35 PM6/4/14

to Michael Shulman, homotopytypetheory

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

Paolo

Jun 4, 2014, 1:20:15 PM6/4/14

to Paolo Capriotti, homotopytypetheory

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.

coinductive definition that I couldn't see how to write as an M-type,

but right now I'm not thinking of it.

Jun 4, 2014, 2:47:18 PM6/4/14

to Dan Licata, Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, homotopytypetheory

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

> 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

Jun 4, 2014, 3:20:45 PM6/4/14

to Paolo Capriotti, Altenkirch Thorsten, Andreas Abel, Michael Shulman, Vladimir Voevodsky, homotopytypetheory

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.

Jun 4, 2014, 3:21:59 PM6/4/14

to Paolo Capriotti, Altenkirch Thorsten, Andreas Abel, Michael Shulman, Vladimir Voevodsky, homotopytypetheory

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.

Jun 4, 2014, 3:31:23 PM6/4/14

to Peter LeFanu Lumsdaine, Altenkirch Thorsten, Andreas Abel, Michael Shulman, Vladimir Voevodsky, homotopytypetheory

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

Jun 4, 2014, 3:36:50 PM6/4/14

to Paolo Capriotti, homotopytypetheory

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.

Jun 4, 2014, 3:45:58 PM6/4/14

to Peter LeFanu Lumsdaine, Paolo Capriotti, homotopytypetheory

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

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

Jun 4, 2014, 4:23:45 PM6/4/14

to Vladimir Voevodsky, homotopytypetheory

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

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

Jun 4, 2014, 4:24:35 PM6/4/14

to Bas Spitters, Peter LeFanu Lumsdaine, Paolo Capriotti, homotopytypetheory

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

Jun 4, 2014, 4:53:44 PM6/4/14

to Martin Escardo, Prof. Vladimir Voevodsky, homotopytypetheory

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.

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.

Jun 4, 2014, 4:54:06 PM6/4/14

to Benedikt Ahrens, Bas Spitters, Peter LeFanu Lumsdaine, Paolo Capriotti, homotopytypetheory

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₂.

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

Jun 4, 2014, 4:58:39 PM6/4/14

to Vladimir Voevodsky, homotopytypetheory

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 .

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

Jun 4, 2014, 5:51:38 PM6/4/14

to Vladimir Voevodsky, homotopytypetheory

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

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

Jun 4, 2014, 6:08:41 PM6/4/14

to Martin Escardo, homotopytypetheory

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

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

Benedikt

Jun 4, 2014, 6:14:44 PM6/4/14

to Martin Escardo, Vladimir Voevodsky, homotopytypetheory

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.

>

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

–p.

Jun 4, 2014, 6:14:54 PM6/4/14