Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: What is a coindexed coalgebra?

Antoine Van Muylder (Apr 17 2024 at 16:38):

I'm pretty sure this has been asked before but had trouble finding the information.

Let $F$ be a functor and let $\alpha$ be a functor algebra. From what I know there are 2 ways to define what "an algebra depending on $\alpha$" should be (in what follows $|\alpha|$ is the carrier of $\alpha$).

• A fibered algebra over $\alpha$ is simply an algebra morphism into $\alpha$
• (edit) In the case of $\mathbb{N}$ which is the intial algebra of $X\mapsto 1+X$, $\mathbb{N}$-indexed algebras are predicates $P : \mathbb{N} \to \mathrm{Set}$ that have $P0$ and $\forall n.\, Pn\to P(n+1)$. More generally, assuming that $F$ has some sort of action on relations/predicates, we can define a $\alpha$-indexed F-algebra to be a logical predicate (i.e. unary logical relation, unary bisimulation, structured predicate) $P : |\alpha| \to \mathrm{Set}$. These are the predicates one need to provide to make use of induction in proof assistants.

To get an indexed algebra out of a fibered one you use the fibers predicate. In the other direction you "sigma up" your indexed algebra.

Induction is then the fact that each $\mu\,F$ fibered algebra has a section or that each indexed algebra is "inhabited".

My question is what happens for coalgebras?

• An $\alpha$-cofibered coalgebra is a coalgebra morphism from $\alpha$
• But then what is a coindexed coalgebra?

Stelios Tsampas (Apr 18 2024 at 19:17):

On your example on $P$: If we let your $P$ be a mono $p : P \rightarrowtail \mathbb{N}$ into the natural numbers, then what you presented as an $\mathbb{N}$-indexed algebra is

• The existence of a subalgebra $[p_{0},p_{\text{ind}}] : 1 + P \to P$ into the initial $1 + (-)$ algebra $\mathbb{N}$, such that
• $p$ is an algebra homomorphism.

By initiality, $P \cong \mathbb{N}$, hence $Pn$ for all $n$. Like you said, this is what a proof by induction looks like categorically (i.e. showing the existence of such an algebra $1 + P \to P$), I just found your notation and viewpoint a bit unfamiliar to me. Also, I don't get why you would call this a logical predicate. Is it simply because it is a subcoalgebra? I disagree with this terminology, because to me a logical predicate (or relation) is a certain predicate on an initial algebra, where the carrier of said initial algebra exhibits some higher-order "applicative" behavior and said predicate maps inputs in the predicate to output in the predicate. I gave a (lousy?) presentation (edit: better slides here) on precisely this topic in your university two weeks ago (see also relevant paper) ;).

Stelios Tsampas (Apr 18 2024 at 19:20):

I will henceforth assume that the notion of a subalgebra on an initial algebra adequately captures the essence of a "predicate proven true by induction" and I hope that you will agree.

Stelios Tsampas (Apr 18 2024 at 19:23):

So, to answer your question, I will simply consider the dual of a subalgebra, a subcoalgebra. A predicate $p : P \rightarrowtail X$ to the state space of a coalgebra $X \to FX$ is what is known as a (coalgebraic) invariant, i.e. in Set this corresponds to a subset on states which is preserved through computation.

Stelios Tsampas (Apr 18 2024 at 19:41):

If $F$ has, as you mention, an action on relations/predicates, e.g. $\overline{F}$, the correct thing to say would be that a $P$ is an $\overline{F}$-algebra (dually, an $\overline{F}$-coalgebra). Furthermore, in his 2016 book, Jacobs calls the relational counterpart of the above a logical bisimulation, which justifies the terminology you used :grinning_face_with_smiling_eyes:.

Antoine Van Muylder (Apr 19 2024 at 13:25):

Stelios Tsampas said:

On your example on $P$: If we let your $P$ be a mono $p : P \rightarrowtail \mathbb{N}$ into the natural numbers, then what you presented as an $\mathbb{N}$-indexed algebra is

• The existence of a subalgebra $[p_{0},p_{\text{ind}}] : 1 + P \to P$ into the initial $1 + (-)$ algebra $\mathbb{N}$, such that
• $p$ is an algebra homomorphism.

By initiality, $P \cong \mathbb{N}$, hence $Pn$ for all $n$. Like you said, this is what a proof by induction looks like categorically (i.e. showing the existence of such an algebra $1 + P \to P$), I just found your notation and viewpoint a bit unfamiliar to me. Also, I don't get why you would call this a logical predicate. Is it simply because it is a subcoalgebra? I disagree with this terminology, because to me a logical predicate (or relation) is a certain predicate on an initial algebra, where the carrier of said initial algebra exhibits some higher-order "applicative" behavior and said predicate maps inputs in the predicate to output in the predicate. I gave a (lousy?) presentation (edit: better slides here) on precisely this topic in your university two weeks ago (see also relevant paper) ;).

Hi Stelios thanks for the answer.

Isn't it the case, still looking at $\mathbb{N}$, that a family $P_{n},n\in \mathbb{N}$ with $P0$ and $\forall n.\, Pn \to P(n+1)$ is a logical predicate in your terminology?
I have to give your presentation a second look

Antoine Van Muylder (Apr 19 2024 at 13:32):

Stelios Tsampas said:

I will henceforth assume that the notion of a subalgebra on an initial algebra adequately captures the essence of a "predicate proven true by induction" and I hope that you will agree.

What you propose is a proof irrelevant "restriction" of what I described above. More specifically a subalgebra of $\alpha$ is in particular a $\alpha$ fibered algebra (since it is a morphism into $\alpha$).

Through the correspondence I laid out above, it is equivalently a map $P : |\alpha| \to \mathrm{hProp}$ such that structure is respected.
I did not specify the meta theory in my question, and it was kind of assumed that we are working in HoTT, sorry :-)

If you work in HoTT you can hopefully prove an equivalence between the 2 notions but this equivalence will not be a definitional one (ie roundtrip proofs will not go by refl). That is why I make a distinction between fibered and indexed algebras.

Antoine Van Muylder (Apr 19 2024 at 13:47):

Stelios Tsampas said:

So, to answer your question, I will simply consider the dual of a subalgebra, a subcoalgebra. A predicate $p : P \rightarrowtail X$ to the state space of a coalgebra $X \to FX$ is what is known as a (coalgebraic) invariant, i.e. in Set this corresponds to a subset on states which is preserved through computation.

I think I was rather interested in morphisms out of a coalgebra. In my terminology "cofibered coalgebras"

Antoine Van Muylder (Apr 19 2024 at 13:51):

Because I think that you can formulate coinduction with these? In fact is it possible to formulate coinduction as it can be done for induction?

Principle 1.
Induction is the property that any $\mu F$-fibered algebra has a section
Spelled out: if $f : P \to \mu F$ is an algebra morphism then there is a $s : \mu F \to P$ such that $f\circ s = id$

Naively I would think that coinduction can read

Principle 2.
Coinduction is the fact that any $\nu F$-cofibered coalgebra has a retraction.
Spelled out: if $f : \nu F \to T$ then there is $r : T \to \nu F$ such that $r \circ f = id$

Antoine Van Muylder (Apr 19 2024 at 17:17):

@Stelios Tsampas for what it's worth I think I've found some answer to my question.
Principle 1 above can be formulated as

$$\text{Principle 1 bis.}\\ \mu F \vDash P\;\text{idxAlg}\\ ------\\ i:\mu F \vDash ind : P(i)$$

where $\mu F \vDash P\;\text{idxAlg}$ is defined as "P is an indexed algebra", the same way I "define" it in my initial question.
So for $\mathbb{N}$ it's exactly what you get in the proof assistant.

I think "Principle 2 bis" probably looks like "bisimilarity is equality".
The following comes from Practical coinduction - D. Kozen, A. Silva

For set-based coalgebras, one form of the classical coinduction principle states that if two
elements are bisimilar, then their unique images in the final coalgebra are the same.

So my best guess for now is that a coindexed coalgbera is a bisimulation relation. I still have to understand how it all fits together.

Stelios Tsampas (Apr 19 2024 at 17:30):

Antoine Van Muylder said:

Isn't it the case, still looking at $\mathbb{N}$, that a family $P_{n},n\in \mathbb{N}$ with $P0$ and $\forall n.\, Pn \to P(n+1)$ is a logical predicate in your terminology?
I have to give your presentation a second look

In my terminology, I would say $P$ is a subalgebra (relative to the initial algebra) or an algebraic invariant (relative to the initial algebra), but because such $P$ just holds, such a terminology is a bit redundant.

Stelios Tsampas (Apr 19 2024 at 17:35):

Again in my terminology, for a predicate $P \rightarrowtail X$ to be logical, at least in the way the people dabbling with logical relations use it, then the following should happen:

• There needs to be an "operational semantics" associated with $X$, which categorically translates to a (higher-order) coalgebra $c : X \to B(X,X)$ for some bifunctor B.
• Assuming a bifunctorial predicate lifting $\overline{B}$, the predicate must be compatible with c in that the successor states under $c$ must be in $\overline{B}(P,P)$.

Stelios Tsampas (Apr 19 2024 at 17:40):

Basically the property of $P \rightarrowtail X$ being a logical predicate is some sort of a generalization of the notion of a coalgebraic invariant, only for higher-order coalgebras! And indeed, the way I define the logical predicate is "an invariant that is relative to itself", or "an invariant that maps inputs in itself to outputs in itself".

Stelios Tsampas (Apr 19 2024 at 17:43):

Antoine Van Muylder said:

Because I think that you can formulate coinduction with these? In fact is it possible to formulate coinduction as it can be done for induction?

Naively I would think that coinduction can read

Principle 2.
Coinduction is the fact that any $\nu F$-cofibered coalgebra has a retraction.
Spelled out: if $f : \nu F \to T$ then there is $r : T \to \nu F$ such that $r \circ f = id$

You are correct I believe :).

Stelios Tsampas (Apr 19 2024 at 18:02):

Antoine Van Muylder said:

So my best guess for now is that a coindexed coalgbera is a bisimulation relation. I still have to understand how it all fits together.

I'm trying to think how a "coindexed coalgebra" would look like for relations...

Stelios Tsampas (Apr 19 2024 at 18:11):

Antoine Van Muylder said:

Stelios Tsampas said:

I will henceforth assume that the notion of a subalgebra on an initial algebra adequately captures the essence of a "predicate proven true by induction" and I hope that you will agree.

What you propose is a proof irrelevant "restriction" of what I described above. More specifically a subalgebra of $\alpha$ is in particular a $\alpha$ fibered algebra (since it is a morphism into $\alpha$).

Through the correspondence I laid out above, it is equivalently a map $P : |\alpha| \to \mathrm{hProp}$ such that structure is respected.
I did not specify the meta theory in my question, and it was kind of assumed that we are working in HoTT, sorry :-)

If you work in HoTT you can hopefully prove an equivalence between the 2 notions but this equivalence will not be a definitional one (ie roundtrip proofs will not go by refl). That is why I make a distinction between fibered and indexed algebras.

Ah OK, thank you for explaining. Did you assume that we are working in HoTT simply because it is your default mathematical universe, or are you explicitly looking to explore notions of (categorical) induction and coinduction in a HoTT foundations? I am generally curious to know more about your motivation.

Stelios Tsampas (Apr 19 2024 at 18:13):

By the way, to give you and idea of where I'm coming from, my recent work on logical predicates and logical relations involve the categorical modelling/systematization of the common proof methods of resp. logical relations and logical predicates, and in the process expose lightweight reasoning principles.

Antoine Van Muylder (Apr 19 2024 at 18:51):

Stelios Tsampas said:

Again in my terminology, for a predicate $P \rightarrowtail X$ to be logical, at least in the way the people dabbling with logical relations use it, then the following should happen:

• There needs to be an "operational semantics" associated with $X$, which categorically translates to a (higher-order) coalgebra $c : X \to B(X,X)$ for some bifunctor B.
• Assuming a bifunctorial predicate lifting $\overline{B}$, the predicate must be compatible with c in that the successor states under $c$ must be in $\overline{B}(P,P)$.

So here $X$ is the carrier of a coalgebra?

Stelios Tsampas (Apr 19 2024 at 18:52):

Yeah!

Stelios Tsampas (Apr 19 2024 at 18:52):

Technically not a coalgebra, but a higher-order coalgebra, if you will. Without $X$ being such a carrier the notion of logicality (related inputs to related outputs) does not really apply.

Antoine Van Muylder (Apr 19 2024 at 18:58):

Right. I think my question regarded coalgebraic "coinvariants" if that is even a thing :grinning:
So instead of a coalgebra morphism $P \rightarrowtail X$, a coalgebra morphism $X \twoheadrightarrow Q$ (or more generally a morphism $X \to Q$)

Antoine Van Muylder (Apr 19 2024 at 19:04):

Stelios Tsampas said:

Antoine Van Muylder said:

Stelios Tsampas said:

I will henceforth assume that the notion of a subalgebra on an initial algebra adequately captures the essence of a "predicate proven true by induction" and I hope that you will agree.

What you propose is a proof irrelevant "restriction" of what I described above. More specifically a subalgebra of $\alpha$ is in particular a $\alpha$ fibered algebra (since it is a morphism into $\alpha$).

Through the correspondence I laid out above, it is equivalently a map $P : |\alpha| \to \mathrm{hProp}$ such that structure is respected.
I did not specify the meta theory in my question, and it was kind of assumed that we are working in HoTT, sorry :-)

If you work in HoTT you can hopefully prove an equivalence between the 2 notions but this equivalence will not be a definitional one (ie roundtrip proofs will not go by refl). That is why I make a distinction between fibered and indexed algebras.

Ah OK, thank you for explaining. Did you assume that we are working in HoTT simply because it is your default mathematical universe, or are you explicitly looking to explore notions of (categorical) induction and coinduction in a HoTT foundations? I am generally curious to know more about your motivation.

I formulated my question in HoTT because it is nowadays my default math setting, but also because I'm interested not only in algebra monos $P \rightarrowtail X$ but also arbitrary morphisms $P \to X$. Under the fibered-indexed correspondence these translate respectively to $P : X \to \mathrm{hProp}$ and $P : X \to \mathrm{Type}$

i.e. induction can be used to prove things but also build objects that are more than proofs

Also it is a setting where I can make sense of why the fibered and indexed view are different: both are weakly equivalent

Stelios Tsampas (Apr 19 2024 at 19:05):

Maybe you'll find Theorem 3.3.4 (also exercise 4.5.6) in Jacob's book interesting.

Abstractly, the principle of coinduction is presented in Theorem 4.5.8 in the same book (and it says that equality in the final coalgebra is also a final object in its own right). You can perhaps translate it in terms of "coindexing" somehow.

Stelios Tsampas (Apr 19 2024 at 19:10):

Antoine Van Muylder said:

Stelios Tsampas said:

Antoine Van Muylder said:

Stelios Tsampas said:

I will henceforth assume that the notion of a subalgebra on an initial algebra adequately captures the essence of a "predicate proven true by induction" and I hope that you will agree.

What you propose is a proof irrelevant "restriction" of what I described above. More specifically a subalgebra of $\alpha$ is in particular a $\alpha$ fibered algebra (since it is a morphism into $\alpha$).

Through the correspondence I laid out above, it is equivalently a map $P : |\alpha| \to \mathrm{hProp}$ such that structure is respected.
I did not specify the meta theory in my question, and it was kind of assumed that we are working in HoTT, sorry :-)

If you work in HoTT you can hopefully prove an equivalence between the 2 notions but this equivalence will not be a definitional one (ie roundtrip proofs will not go by refl). That is why I make a distinction between fibered and indexed algebras.

Ah OK, thank you for explaining. Did you assume that we are working in HoTT simply because it is your default mathematical universe, or are you explicitly looking to explore notions of (categorical) induction and coinduction in a HoTT foundations? I am generally curious to know more about your motivation.

I formulated my question in HoTT because it is nowadays my default math setting, but also because I'm interested not only in algebra monos $P \rightarrowtail X$ but also arbitrary morphisms $P \to X$. Under the fibered-indexed correspondence these translate respectively to $P : X \to \mathrm{hProp}$ and $P : X \to \mathrm{Type}$

i.e. induction can be used to prove things but also build objects that are more than proofs

Also it is a setting where I can make sense of why the fibered and indexed view are different: both a weakly equivalent

I see! Indeed, you should be able to generalize this induction principle (no prober subalgebras on initial algebras) for arbitrary morphisms $f : X \to \mu F$, also epi-mono factorize $f$ and see what happens, etc.

Antoine Van Muylder (Apr 19 2024 at 19:10):

Stelios Tsampas said:

By the way, to give you and idea of where I'm coming from, my recent work on logical predicates and logical relations involve the categorical modelling/systematization of the common proof methods of resp. logical relations and logical predicates, and in the process expose lightweight reasoning principles.

Yes I was trying to follow along during your talk 2weeks ago because I remember that classical normalization proofs are not so elegant. I still have to understand how you solve this:)

Antoine Van Muylder (Apr 19 2024 at 19:13):

cool I have to look at Jacobs book. thanks for the discussion

Stelios Tsampas (Apr 19 2024 at 19:21):

Awesome! Yeah, there's quite a lot of moving parts, but only because the concrete setting has a lot of moving parts. I would be very happy to help you with specific questions, but some things to keep in mind:

• The outer layer of proving that a logical predicate $\square P \rightarrowtail \mu F$ holds is structural induction, as expected.
• The "inner" layer proof terms, one for each constructor, are based on coinduction (so we're talking about mixed induction and coinduction, also keep in mind that in the literature coinduction is quite degenerate, but it's there).
• $\square (-)$ is a predicate transfomer.
• The "delta" between normal proofs and the lightweight proof methods can be seen at the attached slide.
  image.png
  

Stelios Tsampas (Apr 19 2024 at 19:22):

This attached slide might also be instructive.
image.png

Stelios Tsampas (Apr 19 2024 at 19:22):

Antoine Van Muylder said:

cool I have to look at Jacobs book. thanks for the discussion

Cool discussion indeed!

Stelios Tsampas (Apr 19 2024 at 19:40):

Antoine Van Muylder said:

I formulated my question in HoTT because it is nowadays my default math setting, but also because I'm interested not only in algebra monos $P \rightarrowtail X$ but also arbitrary morphisms $P \to X$. Under the fibered-indexed correspondence these translate respectively to $P : X \to \mathrm{hProp}$ and $P : X \to \mathrm{Type}$

i.e. induction can be used to prove things but also build objects that are more than proofs

Also it is a setting where I can make sense of why the fibered and indexed view are different: both are weakly equivalent

By the way this is quite compelling a question.

Mike Shulman (Apr 19 2024 at 21:55):

I agree that the proper analogy is "recursion : induction :: corecursion : bisimulation". But it takes a bit of creativity to reformulate this in a way that brings out the categorical duality.

Mike Shulman (Apr 19 2024 at 22:02):

Antoine Van Muylder said:

Naively I would think that coinduction can read

Principle 2.
Coinduction is the fact that any νF-cofibered coalgebra has a retraction.
Spelled out: if f:νF→T then there is r:T→νF such that r∘f=id

...

So my best guess for now is that a coindexed coalgbera is a bisimulation relation.

I would say the connection between these two is that a surjective map $\nu F \to T$ is the quotient of its kernel $K$, which is an equivalence relation in $\nu F$ (though in HoTT it will in general be a "higher equivalence relation", i.e. a groupoid object). Thus, by the universal property of the quotient, to define a map $T\to \nu F$, it suffices to define a map from $K$ to $\mathsf{Id}_{\nu F}$, which we can do by bisimulation.

Mike Shulman (Apr 19 2024 at 22:03):

I am not sure what to say about non-surjective maps $\nu F \to T$.

Stelios Tsampas (Apr 20 2024 at 08:12):

Antoine Van Muylder said:

So my best guess for now is that a coindexed coalgbera is a bisimulation relation. I still have to understand how it all fits together.

Hmmm if I was to focus on the "bisimulation relation" part of the above quote, forget about the coindexing and follow along the ideas of Antoine from the beginning of the topic, then clearly an $X \times X$-indexed coalgebra is a bisimulation. Let me sketch this, although it's really basic: suppose there is a coalgebra $h : X \to X + 1$ (keep in mind we can generalize to any functor F with a relation lifting) and a relation $R$ on $X$. An $X \times X$-indexed coalgebra on $R$ amounts to the following:

If $R(t,s)$ then

• either $h(t) = h(s) = \star$, or
• $h(t) = t', h(s) = s'$ and $R((h(t),h(s))$.