Hi all, My formalization doesn't work because of the open bug: https://github.com/agda/agda/issues/2888 (Location of the error: Forcing.hs:230) Is there a work around so that I can keep on working? What agda commit should I revert to? (I.e., in which commit was the new forcing translation introduced?) Best, Stephan