Vojtěch Štěpančík
Vojtěch Štěpančík
Oh nice, so it's just our current formalization which could be more general 👌
For additional details you can consult the following two conversations on the Univalent Agda Discord: - https://discord.com/channels/954089080197611551/963813799557738536/1113756767197876325 - https://discord.com/channels/954089080197611551/963813799557738536/1114984006954524764
I made the scope of this PR smaller so that we could potentially merge it sooner. I'm marking it ready for review.
@EgbertRijke could I eventually get your input, mainly on the organization of the Papers section? Not to discourage you from looking at the rest of the PR.
I agree; on it
I just pushed the solution to the the last hole, making this the first complete proof of correctness of the zigzag construction. 🎉 As noted in the PR description there's...
As expected, the CI fails on insufficient memory
I bumped the heap size available to Agda, so the CI now has a chance to pass. This change should be reverted before merging
``` Checking synthetic-homotopy-theory.zigzag-construction-identity-type-pushouts (/Users/runner/work/agda-unimath/agda-unimath/master/src/synthetic-homotopy-theory/zigzag-construction-identity-type-pushouts.lagda.md). agda: internal error: evacuate: strange closure type 1487223629 (GHC version 9.10.1 for x86_64_apple_darwin) Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug time: command terminated abnormally 1673.95...
I know, right? "Strange closure type"? Buddy, the closures here can get *way* freakier