search

pufferffish / agda-symmetries

MIT License
5 stars 1 forks source link

Prove SList is free symmetric monoidal on groupoids #51

Closed github-actions[bot] closed 3 months ago

github-actions[bot] commented 9 months ago

https://api.github.com/pufferffish/agda-symmetries/blob/0ff92bdb19aba58e89e9690583a23f811cdcca95/Cubical/Structures/Gpd/SMon/SList.agda#L115


--                     ∙ ++-assocr bs [ a ] as
-- ++-comm (swap a b as i) bs = {!!}

-- TODO: Prove SList is free symmetric monoidal on groupoids
--
github-actions[bot] commented 3 months ago

Closed in 6932d2673de844e3070dcaac4c47b0730726c444