search

pufferffish / agda-symmetries

MIT License
5 stars 1 forks source link

Define free symmetric monoidal groupoids as a HIT #50

Closed github-actions[bot] closed 8 months ago

github-actions[bot] commented 1 year ago

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


-- TODO: Define free symmetric monoidal groupoids as a HIT

{-# OPTIONS --cubical #-}
module Cubical.Structures.Gpd.SMon.Free where
github-actions[bot] commented 8 months ago

Closed in 6932d2673de844e3070dcaac4c47b0730726c444