In each of: - [ ] https://github.com/agda/agda-stdlib/blob/6d6c6df41c9ab5ae055dfed2d327ebea164e101a/src/Function/Bundles.agda#L185 - [ ] https://github.com/agda/agda-stdlib/blob/6d6c6df41c9ab5ae055dfed2d327ebea164e101a/src/Function/Bundles.agda#L195 should have `Congrunet` $\mapsto$ `Congruent`? Introduced in #1895 AFAICT.
In each of:
agda-stdlib/src/Function/Bundles.agda
Line 185 in 6d6c6df
agda-stdlib/src/Function/Bundles.agda
Line 195 in 6d6c6df
should have$\mapsto$
CongrunetCongruent? Introduced in #1895 AFAICT.