s/ﬁ/fi.
s/Bisimilarity.agda/Type.agda.
Fixed ≈-coind (incomplete).