# Tag Info

It sounds like the thing you're trying to prove is this: If $X$ is a terminal $B$-coalgebra, then the greatest $B$-bisimulation on $X$ is the internal equality. First of all, the definition of internal equality as the kernel pair of $\text{id}_X$ is a bit silly. The following square is a pullback: $$\require{AMScd} \begin{CD} X @>\text{id}_X>> X\\ ... 1 If you let b=\frac54, then$$\frac nb=\frac{n}{5/4}=\frac{n}{5/4}\times \frac{4/5}{4/5}=\frac{4n}{5} which matches your original expression.
A strategy inspired by merge sort works well. First, split the hats into $\sqrt n$ piles of size $\sqrt n$, and sort each pile by repeatedly finding the smallest unsorted hat in that pile. This takes $O(n)$ queries. Second, merge the piles. To do this, take the smallest hat from each pile and find the minimum of those. That's the smallest hat of all; set it ...