Closed github-actions[bot] closed 1 year ago
https://api.github.com/pufferffish/agda-symmetries/blob/0ff92bdb19aba58e89e9690583a23f811cdcca95/Cubical/Structures/Str.agda#L24
field carrier : Type n algebra : sig σ carrier -> carrier -- TODO : Rename the fields to shorter names car = carrier alg = algebra open struct public module _ {f a x y : Level} {σ : Sig f a} (𝔛 : struct x σ) (𝔜 : struct y σ) where
Closed in c6194bce52a2a5d34847f5f2740055f0d9cfc745
https://api.github.com/pufferffish/agda-symmetries/blob/0ff92bdb19aba58e89e9690583a23f811cdcca95/Cubical/Structures/Str.agda#L24