Pinned toot

In the spirit of the season, I want to share some of my recommendations for the things I really enjoyed in 2022. So without further adieu, here is my

I'm just casually gonna quickly learn some Lean syntax during my algos lecture

Sandy Maguire's #BOBkonf2023 tutorial "An Introduction to Doing Software Proofs in Agda" explains how to prove properties about our software in Agda, what’s productive to prove, and more.

Read more:
bobkonf.de/2023/maguire.html

My PhD thesis, supervised by @MartinEscardo, on domain theory in constructive and predicative HoTT/UF is now publicly available!
It's both on my homepage (tdejong.com/phd-thesis.pdf) and on arXiv (arxiv.org/abs/2301.12405).

The January 2023 release of Functional Programming in Lean is now out! This release adds a chapter on monad transformers and some of the fancier features of do-notation in Lean.

leanprover.github.io/functiona

I handed in my thesis!

people.compute.dtu.dk/ahfrom/ahfrom-thesis.pdf

ANN: 2.6.3 is out today! 🐔🎉
Get yours here: hackage.haskell.org/package/Ag

Here on types, I can make a longer post, rather than a tiny thread, about the headline changes:

⏩ A ton of performance improvements, which total to a ~30% improvement over 2.6.2.2 in time spent for the standard library;

🧊 Erased Cubical Agda, which marks all marks all Cubical Agda definitions (primitives and imports from other --cubical modules) as @​0, quantity-0. The upshot is that you can reason about your programs using cubical machinery (funext!
HITs! univalence!), but nothing cubical "survives to runtime" — because unlike plain Cubical Agda, Erased Cubical can be compiled, using any of our backends (Haskell, JS) or agda2hs.

🇰 For a while during 2.6.3's development, --without-K also meant "generate support code for Cubical Agda". This was widely regarded as a bad move and made a lot of people very unhappy, so we rolled it back: Your --without-K code will no
longer suffer from cubical breakouts, and especially no longer enjoy surprise hcomps in error messages. The trade-off is that, if you want your modules to be usable from Cubical Agda (--cubical), you need to use the new
--cubical-compatible flag. Since --cubical-compatible does a ton extra (required!) internal work, modules using it will generally take longer to check, and generate larger interfaces files than, the same modules --without-K.

⚠️ Note that --cubical-compatible and --without-K should accept the exact same programs; This means you could develop against --without-K, then change to --cubical-compatible for release, for example. If you find something that one
accepts and the other rejects, please do file a bug report! On GitHub. Not on my DMs.

🪞 Reflection can now generate data types, as long as you pre-declare the names of the type and all the constructors, using the declareData and defineData primitives, together with the unquoteDecl data syntactic form. These even work for
inductive-recursive and inductive-inductive definitions!

🙏 A massive thanks to everyone who contributed to this release. Git tells me that, since the last tag, these lovely folks authored commits on the master branch:

Moisés Ackerman, Andrej Bauer, Jacques Carette, Evan Cavallo, Felix Cherubini, Jonathan Coates, Lucas Escot, Robert Estelle, Alexandre Esteves, Naïm Favier, Sean Gloumeau, Oleg Grenrus, Marcin Grzybowski, Matthias Hutzler, Tom Jack, Andre Knispel, Thomas Lamiaux, Shea Levy, Viktor Lin, Vladimir Lopatin, Sandy Maguire, James Martin, Orestis Melkonian, Fredrik Nordvall Forsberg, Andreas Nuyts, Kyle Raftogianis, Prabhakar Ragde, Christian Sattler, Peter Selinger, Artem Shinkarov, Mike Shulman, Alissa Tung, Andrea Vezzosi, Szumi Xie, Tesla Zhang, Fangyi Zhou; Favonia, lawcho, Maštarija, oskeri, person-with-a-username, Riccardo, tensorknower69, and thorimur.

Some of them are here on Fedi, but I don't want to bother them all with pings, so I won't.

🧑‍💻 Our tireless main developers (🤓❤️) also deserve a great big round of applause, not only for finishing the release, but for all they do for the language,
especially since most have real jobs, too!

Andreas Abel, Guillaume Allais, Nils Anders Danielsson, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Ulf Norell, and Andrés Sicard-Ramírez.

If you want to get involved, please reach out! We always welcome pull requests and issue reports, be them to Agda itself, the Emacs mode, both their documentations, the standard, cubical, and categories libraries. We promise nobody will get
bitten for submitting a pull request 🙂

2.6.3 has (finally) been released! Get yours now at hackage.haskell.org/package/Ag and get a complimentary performance boost to your Agda code FOR FREE!

Trying out a web client for mastodon @phanpy by @cheeaun and it's just sooooo pleasant 💞

I love-love-love colour-coded boosts and overall it's just so clean.

Definitely the best website I've seen in a few weeks

New paper on open science and artifacts in software research: cacm.acm.org/magazines/2023/2/ w/ Teresa Baldassarre, @benhermann @timmenzies

"This article is written as a protest, of sorts, against how we currently assess science and scientific output."

Good overview article in the Belgian newspaper De Standaard on the “15 minute city”, with a beautiful cartoon by @lectrr.

I really appreciate a newspaper taking two full pages to give a fair overview of the concept, its challenges, its promises… and how its deployment in Flanders seems to be going.

#UrbanPlanning #15MinuteCity #UrbanDesign #UrbanMobility

standaard.be/cnt/dmf20230127_9

I have no mathematical point to share here, just a recoloring of an old image I made of the Folkman graph (en.wikipedia.org/wiki/Folkman_) that I thought came out interesting-looking.

It is something like one of Escher's impossible figures: Locally it looks like it could be made from overlapping translucent sheets of blue material, cut out in this pattern, but globally it doesn't all fit together.

@ionchy Petition to increase the character limit on types.pl so I do not to split up my Cubical Agda error messages.

Show thread

I just realized I can probably just paste the full error message here 

(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n f))
(suc l))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) l
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₁ →
((λ i₂ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₂))
∙ (λ i₂ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₂))))
i₁

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n f))
(suc l))
a)
})
((λ { north → 0ₖ (suc (suc l))
; south → 0ₖ (suc (suc l))
; (merid a i)
→ EM→ΩEM+1 (suc l)
(elim+2 (_⊗_ (EM-raw'→EM H' zero y))
(elimGroupoid (L' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM H' zero y ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM H' zero y ⊗ h))
(emloop (EM-raw'→EM H' zero y ⊗ l₁))
(emloop
(EM-raw'→EM H' zero y ⊗
(H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp ((H' ⨂₁ L') , AbGroupStr→GroupStr (snd (H' ⨂ L')))
(EM-raw'→EM H' zero y ⊗ h) (EM-raw'→EM H' zero y ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ (EM-raw'→EM H' zero y) h l₁ (~ i₃))))
i₂

emloop
(EM-raw'→EM H' zero y ⊗
(H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM H' zero y ⊗
(H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l₁)))
(~ i₁))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y) n f))
(suc l) (EM-raw→EM L' (suc l) a))
i
; (hcomp {_} {.(Susp (EM-raw _ (suc _)))} {φ = φ} u a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y) l
(elim+2 (_⊗_ (EM-raw'→EM H' zero y))
(elimGroupoid (L' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM H' zero y ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM H' zero y ⊗ h))
(emloop (EM-raw'→EM H' zero y ⊗ l₁))
(emloop
(EM-raw'→EM H' zero y ⊗
(H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp ((H' ⨂₁ L') , AbGroupStr→GroupStr (snd (H' ⨂ L')))
(EM-raw'→EM H' zero y ⊗ h) (EM-raw'→EM H' zero y ⊗ l₁) (~ i₃))
(~ i))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y) n f))
(suc l))
a)
})
z)))
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc l)))
(suc (suc (suc l)))
(blocked on _p_9977)
when scope checking the declaration
open import Cubical.Homotopy.EilenbergMacLane.CupProductTensor renaming (_⌣ₖ_ to _⌣ₖ⊗_;
⌣ₖ-0ₖ to ⌣ₖ-0ₖ⊗;
0ₖ-⌣ₖ to 0ₖ-⌣ₖ⊗)
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda:8,1-9,63
Unsolved metas at the following locations:
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:994,41-42
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:993,19-996,58
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1027,41-42
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1026,19-1030,67
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1097,52-53
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1097,19-1099,73
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1195,35-36
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1195,19-1196,40
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1214,12-13
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1215,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1216,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1217,29-46
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1208,17-32
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1208,33-34
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1208,69-70
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1208,37-70
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1208,12-73
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1207,19-1208,73
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1245,12-13
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1246,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1247,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1248,29-46
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1237,17-32
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1237,33-34
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1237,74-75
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1237,36-75
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1237,12-77
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1236,12-1237,77
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1277,12-13
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1278,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1279,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1280,29-46
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1269,18-33
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1269,34-35
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1269,78-79
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1269,37-79
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1269,13-81
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1268,13-1269,81
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1308,28-32
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1321,35-36
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1321,19-1323,43
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1309,34-51
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1304,34-35
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1304,72-73
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1303,13-1304,75
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1335,28-32
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1347,37-38
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1347,21-1349,34
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1336,34-51
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1331,34-35
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1331,75-76
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1330,13-1331,78
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1361,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1362,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1363,29-46
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1357,34-35
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1357,75-76
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1356,13-1357,78
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1387,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1388,23-27
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1389,29-46
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1383,33-34
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1383,77-78
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1382,12-1383,80
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1418,28-32
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1419,34-51
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1413,34-35
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1413,72-73
/home/runner/work/agda/agda/cubical/Cubical/Homotopy/EilenbergMacLane/CupProductTensor.agda:1412,13-1413,75
when scope checking the declaration
open import Cubical.Homotopy.EilenbergMacLane.CupProductTensor renaming (_⌣ₖ_ to _⌣ₖ⊗_;
⌣ₖ-0ₖ to ⌣ₖ-0ₖ⊗;
0ₖ-⌣ₖ to 0ₖ-⌣ₖ⊗)

Show thread

I just realized I can probably just paste the full error message here 

Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a)
})
∣ y ∣ .fst (EM-raw'→EM L' (suc l) z))))
= Cubical.HITs.Truncation.Base.transpHubAndSpoke
(λ i →
EM-raw ((G' ⨂ H') ⨂ L')
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0) (λ .o₁ → suc (+-suc n l i₁))
(λ .o₁ → suc (+-suc n l i₁)) _)))
(n + suc l)))))
(λ i →
suc
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0) (λ .o₁ → suc (+-suc n l i₁))
(λ .o₁ → suc (+-suc n l i₁)) _)))
(n + suc l)))))
i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc (suc (n + l)))))))
(λ a →

inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + suc (n + l)) a
∣ₕ)
(rec₊ (isOfHLevelTrunc (4 + suc (n + l)))
(λ { north → 0ₖ (suc (suc (suc (n + l))))
; south → 0ₖ (suc (suc (suc (n + l))))
; (merid a i)
→ EM→ΩEM+1 (suc (suc (n + l)))
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₃))))
i₂

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n₁ f))
(suc (suc (n + l))) (EM-raw→EM (H' ⨂ L') (suc (suc (n + l))) a))
i
; (hcomp {.(ℓ-max _ _)}
{.(Susp (EM-raw (_ ⨂ _) (suc (suc (_ + _)))))}
{φ = φ}
u
a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) (suc (n + l))
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₃))))
i₂

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n₁ f))
(suc (suc (n + l))))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) (suc (n + l))
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₁ →
((λ i₂ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₂))
∙ (λ i₂ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₂))))
i₁

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n₁ f))
(suc (suc (n + l))))
a)
})
((λ { north → (λ z₁ → 0ₖ (3 + (n + l))) , (λ _ → 0ₖ (3 + (n + l)))
; south → (λ z₁ → 0ₖ (3 + (n + l))) , (λ _ → 0ₖ (3 + (n + l)))
; (merid a i)
→ (λ x₁ →
EM→ΩEM+1 (2 + (n + l))
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n) (suc l) (EM-raw→EM H' (suc n) a) .fst x₁)
i)
,
(λ j →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.pp n l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a j i)
; (hcomp {_} {.(Susp (EM-raw _ (suc _)))} {φ = φ} u a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a)
})
y .fst (EM-raw'→EM L' (suc l) z))))
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + l)))))
(suc (suc (suc (suc (n + l)))))
(blocked on _p_11369)
transp (λ i → EM ((G' ⨂ H') ⨂ L') (_p_10556 i)) i0
(swapFun zero 1 (suc l)
(x ⌣ₖ (EM-raw'→EM H' 1 y ⌣ₖ EM-raw'→EM L' (suc l) z)))
= Cubical.HITs.Truncation.Base.transpHubAndSpoke
(λ i →
EM-raw ((G' ⨂ H') ⨂ L')
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0) (λ .o₁ → suc l) (λ .o₁ → suc l)
_)))
l))))
(λ i →
suc
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0) (λ .o₁ → suc l) (λ .o₁ → suc l)
_)))
l))))
i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc l)))))
(λ a →
∣ inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + l) a ∣ₕ)
(rec₊ (isOfHLevelTrunc (4 + l))
(λ { north → 0ₖ (suc (suc l))
; south → 0ₖ (suc (suc l))
; (merid a i)
→ EM→ΩEM+1 (suc l)
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₃))))
i₂

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n f))
(suc l) (EM-raw→EM (H' ⨂ L') (suc l) a))
i
; (hcomp {.(ℓ-max _ _)} {.(Susp (EM-raw (_ ⨂ _) (suc _)))} {φ = φ}
u
a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) l
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₃))))
i₂

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n f))
(suc l))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) l
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₁ →
((λ i₂ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₂))
∙ (λ i₂ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₂))))
i₁

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n f))
(suc l))
a)
})
(elimGroupoid (H' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → isOfHLevel↑∙ 1 l)
(snd (EM∙ L' (suc l) →∙ EM∙ (H' ⨂ L') (suc (suc l)) ∙))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.f l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n f →
ℕelim (λ g → (λ h → ·₀' h (suc n) g) , 0·₀' (suc n) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n m f))
0)
l)
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.finalpp l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n f →
ℕelim (λ g → (λ h → ·₀' h (suc n) g) , 0·₀' (suc n) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n m f))
0)
l)
(EM₁-raw→EM₁ (H' Cubical.Homotopy.EilenbergMacLane.Base.*) y) .fst
(EM-raw'→EM L' (suc l) z))))
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc l)))
(suc (suc (suc l)))
(blocked on _p_10556)
transp (λ i → EM ((G' ⨂ H') ⨂ L') (_p_9977 i)) i0
(swapFun zero zero (2 + l) (x ⌣ₖ (y ⌣ₖ EM-raw'→EM L' (2 + l) z)))
= Cubical.HITs.Truncation.Base.transpHubAndSpoke
(λ i →
EM-raw ((G' ⨂ H') ⨂ L')
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0) (λ .o₁ → suc l) (λ .o₁ → suc l)
_)))
l))))
(λ i →
suc
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0) (λ .o₁ → suc l) (λ .o₁ → suc l)
_)))
l))))
i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc l)))))
(λ a →
∣ inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + l) a ∣ₕ)
(rec₊ (isOfHLevelTrunc (4 + l))
(λ { north → 0ₖ (suc (suc l))
; south → 0ₖ (suc (suc l))
; (merid a i)
→ EM→ΩEM+1 (suc l)
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₃))))
i₂

emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n f →
trRec (isOfHLevelTrunc (4 + n))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) n f))
(suc l) (EM-raw→EM (H' ⨂ L') (suc l) a))
i
; (hcomp {.(ℓ-max _ _)} {.(Susp (EM-raw (_ ⨂ _) (suc _)))} {φ = φ}
u
a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM G' zero x) l
(elim+2 (_⊗_ (EM-raw'→EM G' zero x))
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (EM-raw'→EM G' zero x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (EM-raw'→EM G' zero x ⊗ h))
(emloop (EM-raw'→EM G' zero x ⊗ l₁))
(emloop
(EM-raw'→EM G' zero x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(EM-raw'→EM G' zero x ⊗ h) (EM-raw'→EM G' zero x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ (EM-raw'→EM G' zero x) h l₁ (~ i₃))))
i₂

emloop
(EM-raw'→EM G' zero x ⊗

Show thread

I just realized I can probably just paste the full error message here 

(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z) n₁ f))
(suc n))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z) n
(elim+2 (_⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
(elimGroupoid (G' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase
(λ g → emloop (g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(λ g l →
compPathR→PathP
(λ i →
(∙assoc
(emloop (g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(emloop (l ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
⁻¹)
∙∙
(λ i₁ →
((λ i₂ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
(l ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)) (~ i₂))

(λ i₂ →
emloop
(⊗DistL+⊗ g l (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)
(~ i₂))))
i₁

emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
⁻¹)
∙∙
rCancel
(emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))))
(~ i))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z) n₁ f))
(suc n))
a)
})
x))
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc n)))
(suc (suc (suc n)))
(blocked on _p_13121)
EM ((G' ⨂ H') ⨂ L') _n_13120
= HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc n)))
(suc (suc (suc n)))
: Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
(blocked on _n_13120)
HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc n)))
(suc (suc (suc n)))
=< EM ((G' ⨂ H') ⨂ L') _n_13120
(blocked on _n_13120)
∣ ptEM-raw ∣
= _12936 (n = n) (ind = ind) (x = north) (y = y) (z = z)
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc n)))
(suc (suc (suc n)))
(blocked on _12936)
∣ ptEM-raw ∣
= _12936 (n = n) (ind = ind) (x = south) (y = y) (z = z)
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc n)))
(suc (suc (suc n)))
(blocked on _12936)
rec₊ (isOfHLevelTrunc (suc (suc (suc (suc n)))))
(λ a₁ →
∣ inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + n) a₁ ∣ₕ)
(σ-EM' n (EM-raw→EM G' (suc n) a ⌣ₖ (y ⊗ z)) i)
= _12936 (n = n) (ind = ind) (x = (merid a i)) (y = y) (z = z)
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc n)))
(suc (suc (suc n)))
(blocked on _12936)
transp (λ i₁ → EM ((G' ⨂ H') ⨂ L') (_p_12272 i₁)) i0
(swapFun zero zero (suc (suc n)) (g ⌣ₖ (y ⌣ₖ ∣ z ∣)))
= Cubical.HITs.Truncation.Base.transpHubAndSpoke
(λ i₁ →
EM-raw ((G' ⨂ H') ⨂ L')
(suc
(suc
(hcomp
(λ i₂ .o →
transp (λ i₃ → ℕ) i₂
(Agda.Builtin.Nat.suc-0
(primPOr (i₁ ∧ i1) ((~ i₁ ∧ i1) ∨ i0) (λ .o₁ → suc n)
(λ .o₁ → suc n) _)))
n))))
(λ i₁ →
suc
(suc
(suc
(hcomp
(λ i₂ .o →
transp (λ i₃ → ℕ) i₂
(Agda.Builtin.Nat.suc-0
(primPOr (i₁ ∧ i1) ((~ i₁ ∧ i1) ∨ i0) (λ .o₁ → suc n)
(λ .o₁ → suc n) _)))
n))))
i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc n)))))
(λ a →
∣ inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + n) a ∣ₕ)
(rec₊ (isOfHLevelTrunc (4 + n))
(λ { north → 0ₖ (suc (suc n))
; south → 0ₖ (suc (suc n))
; (merid a i)
→ EM→ΩEM+1 (suc n)
(elim+2 (_⊗_ g)
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (g ⊗ h))
(λ h l →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (g ⊗ h)) (emloop (g ⊗ l))
(emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(g ⊗ h) (g ⊗ l) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ g h l (~ i₃))))
i₂

emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
rCancel
(emloop
(g ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
g n₁ f))
(suc n) (EM-raw→EM (H' ⨂ L') (suc n) a))
i
; (hcomp {.(ℓ-max _ _)} {.(Susp (EM-raw (_ ⨂ _) (suc _)))} {φ = φ}
u
a)
→ comp
(λ i₁ .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
g n
(elim+2 (_⊗_ g)
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (g ⊗ h))
(λ h l →
compPathR→PathP
(λ i₂ →
(∙assoc (emloop (g ⊗ h)) (emloop (g ⊗ l))
(emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
(λ i₃ →
((λ i₄ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(g ⊗ h) (g ⊗ l) (~ i₄))
∙ (λ i₄ → emloop (⊗DistR+⊗ g h l (~ i₄))))
i₃

emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
rCancel
(emloop
(g ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)))
(~ i₂))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
g n₁ f))
(suc n))
(u i₁ _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
g n
(elim+2 (_⊗_ g)
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (g ⊗ h))
(λ h l →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (g ⊗ h)) (emloop (g ⊗ l))
(emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(g ⊗ h) (g ⊗ l) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ g h l (~ i₃))))
i₂

emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
rCancel
(emloop
(g ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
g n₁ f))
(suc n))
a)
})
((λ { north → 0ₖ (suc (suc n))
; south → 0ₖ (suc (suc n))
; (merid a i)
→ EM→ΩEM+1 (suc n)
(elim+2 (_⊗_ y)
(elimGroupoid (L' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (y ⊗ h))
(λ h l →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (y ⊗ h)) (emloop (y ⊗ l))
(emloop
(y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp ((H' ⨂₁ L') , AbGroupStr→GroupStr (snd (H' ⨂ L')))
(y ⊗ h) (y ⊗ l) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ y h l (~ i₃))))
i₂

emloop (y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)
⁻¹)
∙∙
rCancel
(emloop
(y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
y n₁ f))
(suc n) (EM-raw→EM L' (suc n) a))
i
; (hcomp {_} {.(Susp (EM-raw _ (suc _)))} {φ = φ} u a)
→ comp
(λ i₁ .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
y n
(elim+2 (_⊗_ y)
(elimGroupoid (L' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (y ⊗ h))
(λ h l →
compPathR→PathP
(λ i₂ →
(∙assoc (emloop (y ⊗ h)) (emloop (y ⊗ l))
(emloop
(y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)
⁻¹)
∙∙
(λ i₃ →
((λ i₄ →
emloop-comp ((H' ⨂₁ L') , AbGroupStr→GroupStr (snd (H' ⨂ L')))
(y ⊗ h) (y ⊗ l) (~ i₄))
∙ (λ i₄ → emloop (⊗DistR+⊗ y h l (~ i₄))))
i₃

emloop (y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)
⁻¹)
∙∙
rCancel
(emloop
(y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)))
(~ i₂))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
y n₁ f))
(suc n))
(u i₁ _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
y n
(elim+2 (_⊗_ y)
(elimGroupoid (L' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (y ⊗ h))
(λ h l →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (y ⊗ h)) (emloop (y ⊗ l))
(emloop
(y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp ((H' ⨂₁ L') , AbGroupStr→GroupStr (snd (H' ⨂ L')))
(y ⊗ h) (y ⊗ l) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ y h l (~ i₃))))
i₂

emloop (y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)
⁻¹)
∙∙
rCancel
(emloop
(y ⊗ (H' Cubical.Algebra.AbGroup.TensorProduct._.+B L') h l)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
y n₁ f))
(suc n))
a)
})
z)))
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc n)))
(suc (suc (suc n)))
(blocked on _p_12272)
transp (λ i → EM ((G' ⨂ H') ⨂ L') (_p_11369 i)) i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc (suc (n + l)))))))
(λ a →

inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + suc (n + l)) a
∣ₕ)
(rec₊ (isOfHLevelTrunc (4 + suc (n + l)))
(λ { north → 0ₖ (suc (suc (suc (n + l))))
; south → 0ₖ (suc (suc (suc (n + l))))
; (merid a i)
→ EM→ΩEM+1 (suc (suc (n + l)))
(elim+2 (_⊗_ x)
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (x ⊗ h)) (emloop (x ⊗ l₁))
(emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(x ⊗ h) (x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ x h l₁ (~ i₃))))
i₂

emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
x n₁ f))
(suc (suc (n + l))) (EM-raw→EM (H' ⨂ L') (suc (suc (n + l))) a))
i
; (hcomp {.(ℓ-max _ _)}
{.(Susp (EM-raw (_ ⨂ _) (suc (suc (_ + _)))))}
{φ = φ}
u
a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
x (suc (n + l))
(elim+2 (_⊗_ x)
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (x ⊗ h)) (emloop (x ⊗ l₁))
(emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(x ⊗ h) (x ⊗ l₁) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ x h l₁ (~ i₃))))
i₂

emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
x n₁ f))
(suc (suc (n + l))))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
x (suc (n + l))
(elim+2 (_⊗_ x)
(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (x ⊗ h))
(λ h l₁ →
compPathR→PathP
(λ i →
(∙assoc (emloop (x ⊗ h)) (emloop (x ⊗ l₁))
(emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
(λ i₁ →
((λ i₂ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(x ⊗ h) (x ⊗ l₁) (~ i₂))
∙ (λ i₂ → emloop (⊗DistR+⊗ x h l₁ (~ i₂))))
i₁

emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)
⁻¹)
∙∙
rCancel
(emloop
(x ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l₁)))
(~ i))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
x n₁ f))
(suc (suc (n + l))))
a)
})
(elim₊ (λ _ → isOfHLevel↑∙ (2 + n) l)
(λ { north → (λ z₁ → 0ₖ (3 + (n + l))) , (λ _ → 0ₖ (3 + (n + l)))
; south → (λ z₁ → 0ₖ (3 + (n + l))) , (λ _ → 0ₖ (3 + (n + l)))
; (merid a i)
→ (λ x₁ →
EM→ΩEM+1 (2 + (n + l))
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n) (suc l) (EM-raw→EM H' (suc n) a) .fst x₁)
i)
,
(λ j →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.pp n l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a j i)
; (hcomp {_} {.(Susp (EM-raw _ (suc _)))} {φ = φ} u a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n l
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →

Show thread

I just realized I can probably just paste the full error message here 

(elimGroupoid ((H' ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ h → emloop (g ⊗ h))
(λ h l →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (g ⊗ h)) (emloop (g ⊗ l))
(emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(g ⊗ h) (g ⊗ l) (~ i₃))
∙ (λ i₃ → emloop (⊗DistR+⊗ g h l (~ i₃))))
i₂

emloop
(g ⊗ (G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)
⁻¹)
∙∙
rCancel
(emloop
(g ⊗
(G' Cubical.Algebra.AbGroup.TensorProduct._.+B (H' ⨂ L')) h l)))
(~ i₁)))
(elimGroupoid (H' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase (λ g₁ → emloop (g₁ ⊗ z))
(λ g₁ l →
compPathR→PathP
(λ i₁ →
(∙assoc (emloop (g₁ ⊗ z)) (emloop (l ⊗ z))
(emloop
((H' Cubical.Algebra.AbGroup.TensorProduct._.+A L') g₁ l ⊗ z)
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp ((H' ⨂₁ L') , AbGroupStr→GroupStr (snd (H' ⨂ L')))
(g₁ ⊗ z) (l ⊗ z) (~ i₃))
∙ (λ i₃ → emloop (⊗DistL+⊗ g₁ l z (~ i₃))))
i₂

emloop
((H' Cubical.Algebra.AbGroup.TensorProduct._.+A L') g₁ l ⊗ z)
⁻¹)
∙∙
rCancel
(emloop
((H' Cubical.Algebra.AbGroup.TensorProduct._.+A L') g₁ l ⊗ z)))
(~ i₁)))
(EM₁-raw→EM₁ (H' Cubical.Homotopy.EilenbergMacLane.Base.*) y))))
: EM₁ (((G' ⨂ H') ⨂ L') Cubical.Homotopy.EilenbergMacLane.Base.*)
(blocked on _p_13727)
fst (assL (suc (suc n)) zero (suc (suc l)))
(EM-raw'→EM G'' (suc (suc n)) south) .fst (EM-raw'→EM H'' zero y)
.fst (EM-raw'→EM L'' (suc (suc l)) z)
= flipSquare (help n l ind a i1 y z) i1 i
: HubAndSpoke
(EM-raw ((G'' ⨂ H'') ⨂ L'') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
(blocked on any(_13386, _13518))
fst (assL (suc (suc n)) zero (suc (suc l)))
(EM-raw'→EM G'' (suc (suc n)) north) .fst (EM-raw'→EM H'' zero y)
.fst (EM-raw'→EM L'' (suc (suc l)) z)
= flipSquare (help n l ind a i0 y z) i0 i
: HubAndSpoke
(EM-raw ((G'' ⨂ H'') ⨂ L'') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
(blocked on any(_13381, _13518))
fst (assL (suc (suc n)) zero 1)
(EM-raw'→EM G'' (suc (suc n)) south) .fst (EM-raw'→EM H'' zero y)
.fst (EM-raw'→EM L'' 1 z)
= flipSquare
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.Assoc.help n
ind a i1 y z)
i1 i
: HubAndSpoke
(EM-raw ((G'' ⨂ H'') ⨂ L'') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
(blocked on any(_13176, _13308))
fst (assL (suc (suc n)) zero 1)
(EM-raw'→EM G'' (suc (suc n)) north) .fst (EM-raw'→EM H'' zero y)
.fst (EM-raw'→EM L'' 1 z)
= flipSquare
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.Assoc.help n
ind a i0 y z)
i0 i
: HubAndSpoke
(EM-raw ((G'' ⨂ H'') ⨂ L'') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
(blocked on any(_13171, _13308))
fst (assL (suc (suc n)) zero zero)
(EM-raw'→EM G'' (suc (suc n)) south) .fst (EM-raw'→EM H'' zero y)
.fst (EM-raw'→EM L'' zero z)
= flipSquare
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.Assoc.help n
ind a i1 y z)
i1 i
: HubAndSpoke (EM-raw ((G'' ⨂ H'') ⨂ L'') (suc (suc n)))
(suc (suc (suc n)))
(blocked on any(_12946, _13096))
fst (assL (suc (suc n)) zero zero)
(EM-raw'→EM G'' (suc (suc n)) north) .fst (EM-raw'→EM H'' zero y)
.fst (EM-raw'→EM L'' zero z)
= flipSquare
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.Assoc.help n
ind a i0 y z)
i0 i
: HubAndSpoke (EM-raw ((G'' ⨂ H'') ⨂ L'') (suc (suc n)))
(suc (suc (suc n)))
(blocked on any(_12941, _13096))
transp (λ i → EM ((G' ⨂ H') ⨂ L') (_p_13541 i)) i0
(_13376 (n = n) (l = l) (ind = ind) (x = x) (y = y) (z = z))
= Cubical.HITs.Truncation.Base.transpHubAndSpoke
(λ i →
EM-raw ((G' ⨂ H') ⨂ L')
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0)
(λ .o₁ → suc (+-suc (+-zero n i₁) (suc l) i₁))
(λ .o₁ → suc (+-suc n (suc l) i₁)) _)))
(+-assoc n zero (suc (suc l)) i)))))
(λ i →
suc
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0)
(λ .o₁ → suc (+-suc (+-zero n i₁) (suc l) i₁))
(λ .o₁ → suc (+-suc n (suc l) i₁)) _)))
(+-assoc n zero (suc (suc l)) i)))))
i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc (suc (n + suc l)))))))
(λ a →

inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc)
(2 + suc (n + suc l)) a
∣ₕ)
((λ { north
→ (λ z₁ → 0ₖ (3 + (n + suc l))) , (λ _ → 0ₖ (3 + (n + suc l)))
; south
→ (λ z₁ → 0ₖ (3 + (n + suc l))) , (λ _ → 0ₖ (3 + (n + suc l)))
; (merid a i)
→ (λ x₁ →
EM→ΩEM+1 (2 + (n + suc l))
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n) (suc (suc l)) (EM-raw→EM G' (suc n) a) .fst x₁)
i)
,
(λ j →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.pp n (suc l)
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a j i)
; (hcomp {_} {.(Susp (EM-raw _ (suc _)))} {φ = φ} u a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n (suc l)
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n (suc l)
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a)
})
x .fst (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' (suc (suc l)) z)))
: HubAndSpoke
(EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
(blocked on _p_13541)
EM ((G' ⨂ H') ⨂ L') _n_13540
= HubAndSpoke
(EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
: Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
(blocked on _n_13540)
HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
=< EM ((G' ⨂ H') ⨂ L') _n_13540
(blocked on _n_13540)
∣ ptEM-raw ∣
= _13376 (n = n) (l = l) (ind = ind) (x = north) (y = y) (z = z)
: HubAndSpoke
(EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
(blocked on _13376)
∣ ptEM-raw ∣
= _13376 (n = n) (l = l) (ind = ind) (x = south) (y = y) (z = z)
: HubAndSpoke
(EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
(blocked on _13376)
rec₊ (isOfHLevelTrunc (suc (suc (suc (suc (suc (n + suc l)))))))
(λ a₁ →

inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc)
(2 + suc (n + suc l)) a₁
∣ₕ)
(elim₊
(λ _ →
isOfHLevelTrunc (5 + (n + suc l))
(0ₖ (suc (suc (suc (n + suc l)))))
(0ₖ (suc (suc (suc (n + suc l))))))
(λ x i₁ → ∣ σ-EM (suc (n + suc l)) x i₁ ∣ₕ)
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n (suc l)
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
n)
(EM-raw→EM G' (suc n) a) .fst
(cup∙ zero (suc (suc l)) y .fst (EM-raw'→EM L' (suc (suc l)) z)))
i)
= _13376 (n = n) (l = l) (ind = ind) (x = (merid a i)) (y = y)
(z = z)
: HubAndSpoke
(EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + suc l)))))
(suc (suc (suc (suc (n + suc l)))))
(blocked on _13376)
transp (λ i → EM ((G' ⨂ H') ⨂ L') (_p_13331 i)) i0
(_13166 (n = n) (ind = ind) (x = x) (y = y) (z = z))
= Cubical.HITs.Truncation.Base.transpHubAndSpoke
(λ i →
EM-raw ((G' ⨂ H') ⨂ L')
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0)
(λ .o₁ → suc (+-suc (+-zero n i₁) 0 i₁))
(λ .o₁ → suc (+-suc n 0 i₁)) _)))
(+-assoc n zero 1 i)))))
(λ i →
suc
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0)
(λ .o₁ → suc (+-suc (+-zero n i₁) 0 i₁))
(λ .o₁ → suc (+-suc n 0 i₁)) _)))
(+-assoc n zero 1 i)))))
i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc (suc (n + 0)))))))
(λ a →

inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + suc (n + 0)) a
∣ₕ)
((λ { north → (λ z₁ → 0ₖ (3 + (n + 0))) , (λ _ → 0ₖ (3 + (n + 0)))
; south → (λ z₁ → 0ₖ (3 + (n + 0))) , (λ _ → 0ₖ (3 + (n + 0)))
; (merid a i)
→ (λ x₁ →
EM→ΩEM+1 (2 + (n + 0))
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n) 1 (EM-raw→EM G' (suc n) a) .fst x₁)
i)
,
(λ j →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.pp n 0
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a j i)
; (hcomp {_} {.(Susp (EM-raw _ (suc _)))} {φ = φ} u a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n 0
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
(u i _))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
n 0
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
(suc n))
a)
})
x .fst (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' 1 z)))
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
(blocked on _p_13331)
EM ((G' ⨂ H') ⨂ L') _n_13330
= HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
: Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
(blocked on _n_13330)
HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
=< EM ((G' ⨂ H') ⨂ L') _n_13330
(blocked on _n_13330)
∣ ptEM-raw ∣
= _13166 (n = n) (ind = ind) (x = north) (y = y) (z = z)
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
(blocked on _13166)
∣ ptEM-raw ∣
= _13166 (n = n) (ind = ind) (x = south) (y = y) (z = z)
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
(blocked on _13166)
rec₊ (isOfHLevelTrunc (suc (suc (suc (suc (suc (n + 0)))))))
(λ a₁ →

inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + suc (n + 0)) a₁
∣ₕ)
(elim₊
(λ _ →
isOfHLevelTrunc (5 + (n + 0)) (0ₖ (suc (suc (suc (n + 0)))))
(0ₖ (suc (suc (suc (n + 0))))))
(λ x i₁ → ∣ σ-EM (suc (n + 0)) x i₁ ∣ₕ)
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n 0
(ℕelim (λ m g → ·₀ g m , ·₀0 m g)
(λ n₁ f →
ℕelim (λ g → (λ h → ·₀' h (suc n₁) g) , 0·₀' (suc n₁) g)
(λ m _ →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor.main n₁ m f))
n)
(EM-raw→EM G' (suc n) a) .fst
(cup∙ zero 1 y .fst (EM-raw'→EM L' 1 z)))
i)
= _13166 (n = n) (ind = ind) (x = (merid a i)) (y = y) (z = z)
: HubAndSpoke (EM-raw ((G' ⨂ H') ⨂ L') (suc (suc (suc (n + 0)))))
(suc (suc (suc (suc (n + 0)))))
(blocked on _13166)
transp (λ i → EM ((G' ⨂ H') ⨂ L') (_p_13121 i)) i0
(_12936 (n = n) (ind = ind) (x = x) (y = y) (z = z))
= Cubical.HITs.Truncation.Base.transpHubAndSpoke
(λ i →
EM-raw ((G' ⨂ H') ⨂ L')
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0)
(λ .o₁ → suc (+-zero (+-zero n i₁) i₁)) (λ .o₁ → suc (+-zero n i₁))
_)))
(+-assoc n zero zero i)))))
(λ i →
suc
(suc
(suc
(hcomp
(λ i₁ .o →
transp (λ i₂ → ℕ) i₁
(Agda.Builtin.Nat.suc-0
(primPOr (i ∧ i1) ((~ i ∧ i1) ∨ i0)
(λ .o₁ → suc (+-zero (+-zero n i₁) i₁)) (λ .o₁ → suc (+-zero n i₁))
_)))
(+-assoc n zero zero i)))))
i0
(rec₊ (isOfHLevelTrunc (suc (suc (suc (suc n)))))
(λ a →
∣ inducedFun-EM-raw (GroupEquiv→GroupHom ⨂assoc) (2 + n) a ∣ₕ)
((λ { north → 0ₖ (suc (suc n))
; south → 0ₖ (suc (suc n))
; (merid a i)
→ EM→ΩEM+1 (suc n)
(elim+2 (_⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
(elimGroupoid (G' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase
(λ g → emloop (g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(λ g l →
compPathR→PathP
(λ i₁ →
(∙assoc
(emloop (g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(emloop (l ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
(l ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)) (~ i₃))

(λ i₃ →
emloop
(⊗DistL+⊗ g l (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)
(~ i₃))))
i₂

emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
⁻¹)
∙∙
rCancel
(emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))
(Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z) n₁ f))
(suc n) (EM-raw→EM G' (suc n) a))
i
; (hcomp {_} {.(Susp (EM-raw _ (suc _)))} {φ = φ} u a)
→ comp
(λ i .o →
Cubical.Homotopy.EilenbergMacLane.CupProductTensor..extendedlambda0
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z) n
(elim+2 (_⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
(elimGroupoid (G' Cubical.Homotopy.EilenbergMacLane.Base.*)
(λ _ → emsquash) embase
(λ g → emloop (g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(λ g l →
compPathR→PathP
(λ i₁ →
(∙assoc
(emloop (g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(emloop (l ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)))
(emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
⁻¹)
∙∙
(λ i₂ →
((λ i₃ →
emloop-comp
((G' ⨂₁ (H' ⨂ L')) , AbGroupStr→GroupStr (snd (G' ⨂ (H' ⨂ L'))))
(g ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
(l ⊗ (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)) (~ i₃))

(λ i₃ →
emloop
(⊗DistL+⊗ g l (EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z)
(~ i₃))))
i₂

emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))
⁻¹)
∙∙
rCancel
(emloop
((G' Cubical.Algebra.AbGroup.TensorProduct._.+A (H' ⨂ L')) g l ⊗
(EM-raw'→EM H' zero y ⌣ₖ EM-raw'→EM L' zero z))))
(~ i₁))))
(λ n₁ f →
trRec (isOfHLevelTrunc (4 + n₁))

Show thread
I'm trying to get clear in my head what I want to see from Agda. I want it to be a language where I can program, and where I can do mathematics, and where the line between the two is so blurry it might as well be non-existent -- without making life worse for either hemisphere. What can I do to effect this? I can keep contributing little things to stdlib, things that I've reached for and not found, things that maybe other people will reach for too. To find out what those things will be, I've got to keep trying to build things, to program and prove things, in Agda using stdlib. It's a long road and there's still a lot of distance to cover.

@agdakx @xenaproject You will notice that, in large contrast to Agda, Lean the language has 2 developers and mathlib has hundreds.

I'm not against having quite a few more people contribute to the core language, I'm merely sad to see so very few contribute to stdlib. The poor installation experience of the agda ecosystem, i.e. a fully functional agda toolchain, is yet another serious braking factor on adoption.

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.