Higher Coinductive Types

[Francisco Mota]

Hello folks,

Have higher coinductive types have gotten any/much attention? A google search reveals no work on this.

We can define normal coinductive types fairly easily, by analogy to inductive types. For example, streams of natural numbers:

coinductive Stream : Type {

peek : Stream -> Nat 

next : Stream -> Stream

} 

Here, peek and next are destructors of Stream, rather than constructors. (I'm using my own syntax here.) We end up with a corecursive principle (to define functions into Stream):

Stream_corec : {A:Type} -> (A -> Nat) -> (A -> A) -> (A -> Stream) 

And a bisimulation prunciple (to define dependant functions into paths in Stream):

Stream_bisim : {R : Stream -> Stream -> Type}

-> ({a b : Stream} -> R(a,b) -> (peek(a) = peek(b)))

-> ({a b : Stream} -> R(a,b) -> R(next(a), next(b)))

-> ({a b : Stream} -> R(a,b) -> (a = b))

(Is there a more direct analogue to the induction principle for coinductive types?)

For higher coinductive types, we are allowed to specify higher destructors, that take values from paths. For example...

coinductive T : Type { 

pointValue : T -> Nat

pathValue  : {a b : T} -> (a = b) -> Nat 

}

 

We end up with a corecursive principle:

T_corec : {A : Type} -> (A -> Nat) -> ({a b : A} -> (a = b) -> Nat) -> (A -> T)

 

And a bisimulation principle. This time, since R(a,b) is supposed to represent (some) paths from a to b, we must have a pathValue for every R(a,b). So, the bisimulation requires a function of type  R(a,b) -> Nat  for every  a,b:

T_bisim : {R : T -> T -> Type}

-> ({a b : T} -> R(a,b) -> (pointValue(a) = pointValue(b)))

-> ({a b : T} -> R(a,b) -> Nat)

-> ({a b : T} -> R(a,b) -> (a = b))

 

So what is this good for? I'm not sure. But here are three things to consider.

1. [Higher] Coinductive types may warrant a higher bisimulation principle -- one between higher paths. When are two paths equal? When they have the same behavior. The path behavior is dictated by its value (as given by higher destructors), and by its behavior in the groupoid.

2. Higher destructors can be used to forcibly separate two or more points in a higher coinductive type, dually to how higher constructors can be used to forcibly identify two or more points in an inductive type. For example, we can define the type of infinite binary trees in which the left and right subtree must be different:

coinductive DiffBinTree : Type {

node : DiffBinTree -> Nat

leftT : DiffBinTree -> DiffBinTree

rightT : DiffBinTree -> DiffBinTree

mustBeDiff : {a : DiffBinTree} -> (leftT(a) = rightT(a)) -> 0

}

The trick, of course, is to have certain kinds of path lead to contradiction.

3. The groupoid structure of types can be exploited to define some interesting objects. For example, the type of algebraic groups over a base type A:

coinductive Group : Type -> Type {

value : {A : Type} {a b : Group A} -> (a = b) -> A  

} 

Now each inhabitant of Group A represents an algebraic group whose members are inhabitatnts of type A. The group structure is actually present at the path level. Each point g : Group A has a group  (g = g), in which reflexivity is the identity, symmetry is the inverse, and transitivity is multiplication.

What do you folks think?

Thank you for reading.
Cheers,
Francisco Mota

[Nicolai Kraus]

Hi Francisco,

thanks for sharing these thoughts. I'm not aware of much work on Coinduction in HoTT (surely, some people have considered it though). It seems to be a bit tricky.

We certainly would want (Stream A) to be isomorphic to (Nat -> A), which does not leave us any choice of what the equality has to be: (at least intuitively) the equality of two streams is the type of streams of equalities, as in
  Id(a::as,b::bs) := Id(a,b) x Id(as,bs).
I think that with your bisimilation principle (as a primitive) the equality type will not be the correct thing.

On Sat, Dec 21, 2013 at 1:01 AM, Francisco Mota <fmo...@gmail.com> wrote:

And a bisimulation prunciple (to define dependant functions into paths in Stream):

Stream_bisim : {R : Stream -> Stream -> Type}

-> ({a b : Stream} -> R(a,b) -> (peek(a) = peek(b)))

-> ({a b : Stream} -> R(a,b) -> R(next(a), next(b)))

-> ({a b : Stream} -> R(a,b) -> (a = b))

There would be too many equalities. For example, you would get equalities from the bisimilation principle if you put R(a,b) to be Id(a,b) x 2.

In particular, the "correct" equality between two streams over Nat should be propositional!
On the other hand, if we take equality to be the obvious coinductive type, the bisimilation principle can be derived. But actually, I would not find it nice to "define" the equality for such a coinductive type at all. For inductive types, their equality is automatic. Where does this mismatch come from?
 

2. Higher destructors can be used to forcibly separate two or more points in a higher coinductive type, dually to how higher constructors can be used to forcibly identify two or more points in an inductive type. For example, we can define the type of infinite binary trees in which the left and right subtree must be different:

coinductive DiffBinTree : Type {

node : DiffBinTree -> Nat

leftT : DiffBinTree -> DiffBinTree

rightT : DiffBinTree -> DiffBinTree

mustBeDiff : {a : DiffBinTree} -> (leftT(a) = rightT(a)) -> 0

}

The trick, of course, is to have certain kinds of path lead to contradiction.

Interesting point. However, this possibility probably does not make "higher" coinductive types more powerful than ordinary coinductive types (we could take a dependent sum of a co-tree and its "diff"-property). Equality between two points in a higher inductive type can have an interesting structure while "un-equality" is always propositional - that makes this duality a bit disappointing, unfortunately. But I expect that there are other (more far-reaching) possibilities.

 

3. The groupoid structure of types can be exploited to define some interesting objects. For example, the type of algebraic groups over a base type A:

coinductive Group : Type -> Type {

value : {A : Type} {a b : Group A} -> (a = b) -> A  

} 

Now each inhabitant of Group A represents an algebraic group whose members are inhabitatnts of type A. The group structure is actually present at the path level. Each point g : Group A has a group  (g = g), in which reflexivity is the identity, symmetry is the inverse, and transitivity is multiplication.

Okay, but we can do this without coinduction, right?
-- Nicolai

 

What do you folks think?

Thank you for reading.
Cheers,
Francisco Mota

--
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/groups/opt_out.

[Michael Shulman]

Hi Francisco,

Some people have tossed around vague ideas about higher coinductive
types, but as far as I know, no notion of "higher coinductive type"
has emerged which is both useful and justifiable.

Your proposal is interesting, but I suspect it may be inconsistent.
In general, you cannot universally (or couniversally) force two things
to be unequal, because functions do not preserve inequality.

For instance, consider the type X of infinite binary trees whose nodes
are labeled by both a natural number and a color red or black, and
with the property that the left child of every node is red and the
right child of every node is black. The latter condition ensures that
the left and right subtrees of every such tree are different.
Therefore, it seems that the coinduction principle of your DiffBinTree
would give a map from X to DiffBinTree which preserves the tree
structure and number labels, but forgetting the colors. However, such
a map will not preserve the property of left and right subtrees being
different, yielding a contradiction. Am I misunderstanding?

Also, I don't know what you mean by "the type of algebraic groups over
a base type A", but whatever it is, I don't think that your definition
is that. The universal property of identity types means that to give
a function {a b : B} -> (a = b) -> A is equivalent to giving a
function B -> A, so I think under any sensible interpretation, your
type "Group A" will be equivalent to A.

Mike

[Francisco Mota]

Hi Mike,

Thank you for your response.

Your proposal is interesting, but I suspect it may be inconsistent.
In general, you cannot universally (or couniversally) force two things
to be unequal, because functions do not preserve inequality.

For instance, consider the type X of infinite binary trees whose nodes
are labeled by both a natural number and a color red or black, and
with the property that the left child of every node is red and the
right child of every node is black.  The latter condition ensures that
the left and right subtrees of every such tree are different.
Therefore, it seems that the coinduction principle of your DiffBinTree
would give a map from X to DiffBinTree which preserves the tree
structure and number labels, but forgetting the colors.  However, such
a map will not preserve the property of left and right subtrees being
different, yielding a contradiction.  Am I misunderstanding?

I see what you mean. I think this is a compelling argument as to why DiffBinTree cannot exist. Actually, I don't think DiffBinTree really satisfies the spirit of higher coinduction to the letter, since the higher destructor mustBeDiff doesn't come from every path but only from some paths. So I think we can rule out higher destructors of that form. In other words, the only kind of higher constructor between paths, is one of the form:

higherDestructor : {a b : Type} -> (a = b) -> [...]

Naturally, there are some restrictions on what can be inside the [...], but I don't know what they are. I would imagine that a polynomial functor over (A) or over (a=b) or both, would not yield a contradiction. I may be wrong, of course.

I think this restriction actually would make it easier to say what a higher coinductive type is. If we take any type A, and consider the type A', which is the type of paths in A (i.e., the dependent sum  exists (a b : A), (a = b)), and we consider A'', and A''', and so on... A higher coinductive path allows us to define destructors from A, A', A'', A''', and so forth, giving results polynomial in types A, A', A'', A''', and so forth.

This rules out constructions like DiffBinTree. Does it rule out too much?

 

Also, I don't know what you mean by "the type of algebraic groups over
a base type A", but whatever it is, I don't think that your definition
is that.  The universal property of identity types means that to give
a function {a b : B} -> (a = b) -> A is equivalent to giving a
function B -> A, so I think under any sensible interpretation, your
type "Group A" will be equivalent to A.

I'm not sure what you mean. Could you show me?

Thinking more about it, I'm pretty sure Group A doesn't do what I thought it did. As long as A is inhabited, it seems really easy to show that Group A  is a proposition -- you just need to exhibit a relation R : Group A -> Group A -> Type  such that R(a,b) is inhabited for all a b : Group A, and you need a function  R(a,b) -> A. Then you can conclude (a = b)  for any  a b : Group A .

Regardless, the point I was tryng to make is still valid -- the path behave like a groupoid, and this must be considered when performing higher bisimulation. In other words, there are (or there might be) more paths between points than immediately suggested by higher destructors. I need to look into this further.

Best regards,
Fran

[Andrej Bauer]

There is the other possibility to study this: coinductive types are
final coalgebras for a functor. So one "just" has to port final
coalgebras to a higher-categorical setting and see what comes out.
Maybe we can try some easy cases first. What happens in the 2-category
of groupoids, for example?

With kind regards,

Andrej

[Michael Shulman]

On Sat, Dec 21, 2013 at 8:46 PM, Francisco Mota <fmo...@gmail.com> wrote:
> I think this restriction actually would make it easier to say what a higher
> coinductive type is. If we take any type A, and consider the type A', which
> is the type of paths in A (i.e., the dependent sum exists (a b : A), (a =
> b)), and we consider A'', and A''', and so on... A higher coinductive path
> allows us to define destructors from A, A', A'', A''', and so forth, giving
> results polynomial in types A, A', A'', A''', and so forth.
>
> This rules out constructions like DiffBinTree. Does it rule out too much?

I don't think it leaves anything nontrivial, for the reason I
mentioned in response to your (3). Namely, the type A' is equivalent
to the type A, so allowing ourselves to use it instead of A doesn't
give us the ability to construct anything really new.

Mike

[Michael Shulman]

On Sun, Dec 22, 2013 at 1:00 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> There is the other possibility to study this: coinductive types are
> final coalgebras for a functor. So one "just" has to port final
> coalgebras to a higher-categorical setting and see what comes out.

However, *higher* inductive types are not just initial algebras for a
functor -- they are initial monad-algebras for a presented monad.
This would suggest a dual notion of final comonad-coalgebras for a
"copresented" comonad.

Mike

[Francisco Mota]

Hi folks,

Thank you for the discussion. You've given me a lot to think about.

Firstly, I was confusing the path space and the loop space of a type. So where before I said A' was the type of all paths between points in A, I really should have said that A' was the type of all loops inA. Thus A' == exists (a:A). (a=a). This doesn't result in trivial types, as before.

Secondly, i believe that DiffTree above can exist after all, but it must have a complicated corecursion principle. In particular, one must show that for any two element in the base type A that are indistinguishible over the given coalgebra (node, leftT, rightT) over A, they satisfy the higher destructor mustBeDiff. I can't offhand think of a way to generalize this for non-propositional codomains, but this should work fine just for DiffTree. This isn't too promising, but it's something.

Two point five-ly, this kind of construction requires higher destructors to only consider paths between, one element in the coalgebra a, and element that can be obtained by applying zero or more destructors. For instance, a higher destructor with domain {a : A} (a = next(a)) -> ... is fine, but a destructor with domain {a b : A} (a = next(b)) -> ... is not fine. That's because it's generally impossible to produce a final coalgebra, because a and b might have come from completely different coalgebras, so an application of the corecursion principle wouldn't give us a way of executing the higher destructor. At least, I believe this to be true. But I have no proof.

Thirdly, it doesn't make sense to restrict ourselves to higher destructors that only consume paths. We could have higher destructors that consume points and produce paths, for instance. The following higher coinductive type seems (to me) completely natural:

coinductive BiStream : Type -> Type {

    peek : {A : Type} BiStream A -> A
    next : {A : Type} BiStream A -> BiStream A
    prev : {A : Type} BiStream A -> BiStream A
    prev-cancels-next : {A : Type} (bs : BiStream A) -> bs = prev(next(bs))
    next-cancels-prev : {A : Type} (bs : BiStream A) -> bs = next(prev(bs))
}

Even though prev-cancels-next and next-cancels-prev look like higher constructors in a higher inductive type, I submit that they are really higher destructors -- they are destructing elements of BiStream A and producing paths over BiStream A. This type BiStream A is isomorphic to the type Int -> A, but I think it gives us a new perspective.

Fourthly, is there a reason "difference" must be propositional? Can't we define a separation type, say a # b, between two points in the same type  a b : A,that isn't necessarily propositional? I mention this because it seems to me that such separation types are dual to identity types (in the sense that given a function f : A -> B, any equality over A can be mapped onto an equality in B, and dually any separation in B can be mapped onto a separation in A). i think this might be an interesting subject in its own right (function coextensionality? a counivalence axiom, anyone?). Normal coinductive types already yield some pretty interesting separation types -- a separation tells you which destructors to apply in order to exhibit a separation in a different type. The DiffTree example above suggests that higher coinductive types could take advantage of a non-propositional version of inequality.

> However, *higher* inductive types are not just initial algebras for a
> functor -- they are initial monad-algebras for a presented monad.
> This would suggest a dual notion of final comonad-coalgebras for a

> "copresented" comonad.

I'd like to look into this angle. I'm only aware of the duality for non-higher inductive and coinductivetypes (initial algebra / final coalgebra). But I'm not too good at category theory ... yet. Do you have a reference and/or a layman-ish explanation for higher inductive types being initial monad-algebras for a presented monad?

Thank you for everything.
Best wishes and happy new year!

P.S. Mike, sorry for the double posting. i forgot to "reply-all" the first time.