Deterministic timeout building an equivalence

Stream: new members

[Rémi Bottinelli]

Hey! Here, trying to construct an equivalence between sections of two functors on inverse systems, I get deterministic timeouts when unfolding my maps to prove left and right inverses. Is something in the code here particularly slow?