<p>Googling something else I stumbled on <a href="https://groups.google.com/g/homotopytypetheory/c/tYRTcI2Opyo/m/PIrI6t5me-oJ" rel="nofollow noreferrer">a conversation titled &quot;coinductives&quot;</a> initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and left on me an impression of something like a text by Conan Doyle abruptly interrupted at the most thrilling moment.</p>
<p>Could somebody update me on it? What happened afterwards? Most intriguing question that remains unanswered there is whether one can construct a more or less complete duality between inductive and coinductive types. The phenomenon of limit-colimit coincidence somehow suggests that in at least some circumstances that stem from endofunctors in the category-theoretic semantics, the types that correspond to initial algebras and final coalgebras of these endofunctors should be equivalent in some sense. There is a controversy in that discussion whether to expect that.</p>
<p>As an aside, let me remark that there does not even seem to exist any tags related to coinduction here.</p>

CC BY-SA 4.0
2020-11-20T14:46:17.500Z
[This](https://hott.github.io/M-types/m-types.pdf) happened. I can provide more references if needed.
Andrej Bauer
CC BY-SA 4.0
2020-11-20T16:05:50.837Z
@AndrejBauer Please do! More importantly, please say few more words about it.
მამუკა ჯიბლაძე
CC BY-SA 4.0
2020-11-23T10:19:08.670Z
One note about the paper mentioned by Andrej: The construction of final coalgebras from final coalgebras has been investigated as a form of completion, see _Terminal coalgebras in well-founded set theory_ by Michael Barr, as the mentioned paper shows that this construction can be carried out in HoTT. The problem in plain MLTT, as you have seen in the mentioned discussion, is that equality usually does not play along with this construction. Instead, one needs to enforce bisimilarity somewhere. Also, please note that this does _not_ mean initial algebras and final coalgebras coincide!
Henning Basold
CC BY-SA 4.0
2020-11-23T10:24:53.180Z
Unfortunately, this is not ripe for an answer. But I had a student who recently showed how coinductive types can get the right notion of equality in various ways. For instance, eta-equivalence + univalence, bisimilarity + coherence, or finality + coherence. This is similar to what the HoTT book does for inductive types. He then showed that these are all equivalent. What is interesting about this is that it shows that coinductive types need some extra assumption if you want to have that equality coincides with bisimilarity on coinductive types. I hope to find time for the paper soon!
Henning Basold
CC BY-SA 4.0
2020-11-23T16:38:40.737Z
One other tidbit is that cubical Agda has shown a very natural way for equality of coinductive types to work. Bisimulation can easily be given as/shown equivalent to a corecursive definition `I -> T`, which is the way paths are presented. So similar theories almost automatically make proper coinductive equality proofs just as natural as inductive equality proofs.
Dan Doel
CC BY-SA 4.0
2020-11-23T17:45:34.890Z
@HenningBasold Very interesting! So do you know what is required of a type theory to make them coincide? Is this consistent with univalence? Is it consistent at all?
მამუკა ჯიბლაძე
CC BY-SA 4.0
2020-11-23T17:47:29.523Z
@DanDoel Excuse me please, too quick for me. What do you mean by "which is the way paths are presented"?
მამუკა ჯიბლაძე
CC BY-SA 4.0
2020-11-23T18:16:03.797Z
In cubical type theory, an equality/path `p : Path T x y` is like a function `p : I -> T` such that `p i0 = x` and `p i1 = y`, where `i0` and `i1` are the endpoints of the interval. The interval `I` is not exactly a normal type, so paths aren't exactly normal function types, but there are at least analogous constructs, and the way you create a path is analogous to lambda abstraction. So defining a path between values of a coinductive type is analogous to defining a function by corecursion. "Cubical type theory" should be googleable for more information.
Dan Doel
CC BY-SA 4.0
2020-11-23T18:27:08.920Z
@DanDoel I honestry tried, but even the entry labeled [Cubical type theory for dummies](https://gist.github.com/AndyShiue/cfc8c75f8b8655ca7ef2ffeb8cfb1faf/) freaks me out. But all this is extremely interesting. I am aware of two sort of opposite contexts for the interval. The generic interval (living in simplicial sets and, I presume, also in cubical sets) is tiny in the sense of Lawvere ($(-)^I$ has a right adjoint), while the intervals of Pavlovic-Pratt and Freyd are final coalgebras and are, on the contrary, huge in some sense. Which of them would you say is closer to the one you mean here?
მამუკა ჯიბლაძე
CC BY-SA 4.0
2020-11-23T18:36:19.233Z
I don't have a great understanding of the categorical semantics, but I think it's the tiny one. There is a recent paper (Transpension: The Right Adjoint to the Pi-type) on how the right adjoint could be usefully incorporated into type theories (although the paper is more general than just cubical type theory).
Dan Doel
CC BY-SA 4.0
2020-11-23T18:55:45.610Z
@DanDoel Thanks a lot! Looks like I am understanding something in that one.
მამუკა ჯიბლაძე
<reference-request><type-theory><homotopy-type-theory><inductive-type>
Request for an update on a discussion about coinductive types in HoTT (or anywhere else)
მამუკა ჯიბლაძე
# Request for an update on a discussion about coinductive types in HoTT (or anywhere else)

(Asked by: username_0 on 2020-11-20)

Googling something else I stumbled on [a conversation titled "coinductives"](https://groups.google.com/g/homotopytypetheory/c/tYRTcI2Opyo/m/PIrI6t5me-oJ) initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and left on me an impression of something like a text by Conan Doyle abruptly interrupted at the most thrilling moment.

Could somebody update me on it? What happened afterwards? Most intriguing question that remains unanswered there is whether one can construct a more or less complete duality between inductive and coinductive types. The phenomenon of limit-colimit coincidence somehow suggests that in at least some circumstances that stem from endofunctors in the category-theoretic semantics, the types that correspond to initial algebras and final coalgebras of these endofunctors should be equivalent in some sense. There is a controversy in that discussion whether to expect that.

As an aside, let me remark that there does not even seem to exist any tags related to coinduction here.

**Tags:** reference-request, type-theory, homotopy-type-theory, inductive-type

> **Comments:**
> **username_1**: [This](https://hott.github.io/M-types/m-types.pdf) happened. I can provide more references if needed.  
> **username_0**: @AndrejBauer Please do! More importantly, please say few more words about it.  
> **username_2**: One note about the paper mentioned by Andrej: The construction of final coalgebras from final coalgebras has been investigated as a form of completion, see _Terminal coalgebras in well-founded set theory_ by Michael Barr, as the mentioned paper shows that this construction can be carried out in HoTT. The problem in plain MLTT, as you have seen in the mentioned discussion, is that equality usually does not play along with this construction. Instead, one needs to enforce bisimilarity somewhere. Also, please note that this does _not_ mean initial algebras and final coalgebras coincide!  
> **username_2**: Unfortunately, this is not ripe for an answer. But I had a student who recently showed how coinductive types can get the right notion of equality in various ways. For instance, eta-equivalence + univalence, bisimilarity + coherence, or finality + coherence. This is similar to what the HoTT book does for inductive types. He then showed that these are all equivalent. What is interesting about this is that it shows that coinductive types need some extra assumption if you want to have that equality coincides with bisimilarity on coinductive types. I hope to find time for the paper soon!  
> **username_3**: One other tidbit is that cubical Agda has shown a very natural way for equality of coinductive types to work. Bisimulation can easily be given as/shown equivalent to a corecursive definition `I -> T`, which is the way paths are presented. So similar theories almost automatically make proper coinductive equality proofs just as natural as inductive equality proofs.  
> **username_0**: @HenningBasold Very interesting! So do you know what is required of a type theory to make them coincide? Is this consistent with univalence? Is it consistent at all?  
> **username_0**: @DanDoel Excuse me please, too quick for me. What do you mean by "which is the way paths are presented"?  
> **username_3**: In cubical type theory, an equality/path `p : Path T x y` is like a function `p : I -> T` such that `p i0 = x` and `p i1 = y`, where `i0` and `i1` are the endpoints of the interval. The interval `I` is not exactly a normal type, so paths aren't exactly normal function types, but there are at least analogous constructs, and the way you create a path is analogous to lambda abstraction. So defining a path between values of a coinductive type is analogous to defining a function by corecursion. "Cubical type theory" should be googleable for more information.  
> **username_0**: @DanDoel I honestry tried, but even the entry labeled [Cubical type theory for dummies](https://gist.github.com/AndyShiue/cfc8c75f8b8655ca7ef2ffeb8cfb1faf/) freaks me out. But all this is extremely interesting. I am aware of two sort of opposite contexts for the interval. The generic interval (living in simplicial sets and, I presume, also in cubical sets) is tiny in the sense of Lawvere ($(-)^I$ has a right adjoint), while the intervals of Pavlovic-Pratt and Freyd are final coalgebras and are, on the contrary, huge in some sense. Which of them would you say is closer to the one you mean here?  
> **username_3**: I don't have a great understanding of the categorical semantics, but I think it's the tiny one. There is a recent paper (Transpension: The Right Adjoint to the Pi-type) on how the right adjoint could be usefully incorporated into type theories (although the paper is more general than just cubical type theory).  
> **username_0**: @DanDoel Thanks a lot! Looks like I am understanding something in that one.  

---

## 0 answers

