13 | module Control.Category.Instances.Thin

 15 | import Control.Category

 16 | import Control.Category.Records

 17 | import public Control.Relation

 18 | import public Control.Order

 20 | %default total

 22 | public export

 23 | [Thin] Preorder ty rel => Category rel where

 24 |   id = reflexive

 25 |   (.) = flip transitive

 28 | public export

 29 | record RelMonoid ty (rel : Rel ty) where

 30 |   constructor MkRelMonoid

 31 |   {auto impl : Monoid ty}

 32 |   cong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')

 33 |   assoc : {x,y,z : ty} -> rel ((x <+> y) <+> z) (x <+> (y <+> z))

 34 |   assoc' : {x,y,z : ty} -> rel (x <+> (y <+> z)) ((x <+> y) <+> z)

 35 |   unitl : {x : ty} -> rel (Prelude.neutral <+> x) x

 36 |   unitl' : {x : ty} -> rel x (Prelude.neutral <+> x)

 37 |   unitr : {x : ty} -> rel (x <+> Prelude.neutral) x

 38 |   unitr' : {x : ty} -> rel x (x <+> Prelude.neutral)

 40 | public export %inline

 41 | mkRelMonoid :

 42 |   forall ty,rel. Reflexive ty rel =>

 43 |   {auto impl : Monoid ty} ->

 44 |   (cong : {x,x',y,y': ty} -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')) ->

 45 |   (0 assoc : {x,y,z : ty} -> (x <+> y) <+> z = x <+> (y <+> z)) ->

 46 |   (0 unitl : {x : ty} -> Prelude.neutral <+> x = x) ->

 47 |   (0 unitr : {x : ty} -> x <+> Prelude.neutral = x) ->

 48 |   RelMonoid ty rel

 49 | mkRelMonoid c a l r =

 50 |   MkRelMonoid c

 51 |     (replace {p = rel _} a reflexive)

 52 |     (replace {p = rel _} (sym a) reflexive)

 53 |     (replace {p = rel _} l reflexive)

 54 |     (replace {p = rel _} (sym l) reflexive)

 55 |     (replace {p = rel _} r reflexive)

 56 |     (replace {p = rel _} (sym r) reflexive)

 58 | public export

 59 | record RelCommMonoid ty (rel : Rel ty) where

 60 |   constructor MkRelCommMonoid

 61 |   {auto impl : Monoid ty}

 62 |   cong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')

 63 |   assoc : {x,y,z : ty} -> rel ((x <+> y) <+> z) (x <+> (y <+> z))

 64 |   unit : {x : ty} -> rel (Prelude.neutral <+> x) x

 65 |   unit' : {x : ty} -> rel x (Prelude.neutral <+> x)

 66 |   comm : {x,y : ty} -> rel (x <+> y) (y <+> x)

 68 | namespace RelCommMonoid

 69 |   public export %inline

 70 |   relMonoid : Preorder ty rel => (rec : RelCommMonoid ty rel) -> RelMonoid ty rel

 71 |   relMonoid (MkRelCommMonoid c a u u' cm) =

 72 |     MkRelMonoid c a

 73 |     (transitive (c reflexive cm) $ transitive cm $ transitive a $ transitive cm $ c cm reflexive)

 74 |      u u' (transitive cm u) (transitive u' cm)

 76 |   public export %inline

 77 |   (.relMonoid) : Preorder ty rel => (rec : RelCommMonoid ty rel) -> RelMonoid ty rel

 78 |   (.relMonoid) = relMonoid

 80 | public export %inline

 81 | mkRelCommMonoid :

 82 |   forall ty,rel. Reflexive ty rel =>

 83 |   {auto impl : Monoid ty} ->

 84 |   (cong : {x,x',y,y' : _} -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')) ->

 85 |   (0 assoc : {x,y,z : ty} -> (x <+> y) <+> z = x <+> (y <+> z)) ->

 86 |   (0 unit : {x : ty} -> Prelude.neutral <+> x = x) ->

 87 |   (0 comm : {x,y : ty} -> x <+> y = y <+> x) ->

 88 |   RelCommMonoid ty rel

 89 | mkRelCommMonoid c a u cm =

 90 |   MkRelCommMonoid c

 91 |     (replace {p = rel _} a reflexive)

 92 |     (replace {p = rel _} u reflexive)

 93 |     (replace {p = rel _} (sym u) reflexive)

 94 |     (replace {p = rel _} cm reflexive)

 97 | public export

 98 | record RelNearRing ty (rel : Rel ty) where

 99 |   constructor MkRelNearRing

100 |   {auto impl : Num ty}

101 |   plusCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x + x') (y + y')

102 |   multCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x * x') (y * y')

103 |   plusAssoc : {x,y,z : ty} -> rel ((x + y) + z) (x + (y + z))

104 |   plusAssoc' : {x,y,z : ty} -> rel (x + (y + z)) ((x + y) + z)

105 |   multAssoc : {x,y,z : ty} -> rel ((x * y) * z) (x * (y * z))

106 |   multAssoc' : {x,y,z : ty} -> rel (x * (y * z)) ((x * y) * z)

107 |   plusUnitl : {x : ty} -> rel (0 + x) x

108 |   plusUnitl' : {x : ty} -> rel x (0 + x)

109 |   multUnitl : {x : ty} -> rel (1 * x) x

110 |   multUnitl' : {x : ty} -> rel x (1 * x)

111 |   plusUnitr : {x : ty} -> rel (x + 0) x

112 |   plusUnitr' : {x : ty} -> rel x (x + 0)

113 |   multUnitr : {x : ty} -> rel (x * 1) x

114 |   multUnitr' : {x : ty} -> rel x (x * 1)

115 |   distribl : {x,y,z : ty} -> rel (x * (y + z)) (x * y + x * z)

116 |   distribl' : {x,y,z : ty} -> rel (x * y + x * z) (x * (y + z))

117 |   distribr : {x,y,z : ty} -> rel ((x + y) * z) (x * z + y * z)

118 |   distribr' : {x,y,z : ty} -> rel (x * z + y * z) ((x + y) * z)

119 |   absorbl : {x : ty} -> rel (x * 0) 0

120 |   absorbl' : {x : ty} -> rel 0 (x * 0)

121 |   absorbr : {x : ty} -> rel (0 * x) 0

122 |   absorbr' : {x : ty} -> rel 0 (0 * x)

124 | public export %inline

125 | mkRelNearRing :

126 |   forall ty,rel. Reflexive ty rel =>

127 |   {auto impl : Num ty} ->

128 |   (plusCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x + x') (y + y')) ->

129 |   (multCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x * x') (y * y')) ->

130 |   (0 plusAssoc : {x,y,z : ty} -> (x + y) + z = x + (y + z)) ->

131 |   (0 multAssoc : {x,y,z : ty} -> (x * y) * z = x * (y * z)) ->

132 |   (0 plusUnitl : {x : ty} -> 0 + x = x) ->

133 |   (0 multUnitl : {x : ty} -> 1 * x = x) ->

134 |   (0 plusUnitr : {x : ty} -> x + 0 = x) ->

135 |   (0 multUnitr : {x : ty} -> x * 1 = x) ->

136 |   (0 distribl : {x,y,z : ty} -> x * (y + z) = x * y + x * z) ->

137 |   (0 distribr : {x,y,z : ty} -> (x + y) * z = x * z + y * z) ->

138 |   (0 absorbl : {x : ty} -> x * 0 = 0) ->

139 |   (0 absorbr : {x : ty} -> 0 * x = 0) ->

140 |   RelNearRing ty rel

141 | mkRelNearRing pc mc pa ma pl ml pr mr dl dr al ar =

142 |   MkRelNearRing pc mc

143 |     (replace {p = rel _} pa reflexive)

144 |     (replace {p = rel _} (sym pa) reflexive)

145 |     (replace {p = rel _} ma reflexive)

146 |     (replace {p = rel _} (sym ma) reflexive)

147 |     (replace {p = rel _} pl reflexive)

148 |     (replace {p = rel _} (sym pl) reflexive)

149 |     (replace {p = rel _} ml reflexive)

150 |     (replace {p = rel _} (sym ml) reflexive)

151 |     (replace {p = rel _} pr reflexive)

152 |     (replace {p = rel _} (sym pr) reflexive)

153 |     (replace {p = rel _} mr reflexive)

154 |     (replace {p = rel _} (sym mr) reflexive)

155 |     (replace {p = rel _} dl reflexive)

156 |     (replace {p = rel _} (sym dl) reflexive)

157 |     (replace {p = rel _} dr reflexive)

158 |     (replace {p = rel _} (sym dr) reflexive)

159 |     (replace {p = rel _} al reflexive)

160 |     (replace {p = rel _} (sym al) reflexive)

161 |     (replace {p = rel _} ar reflexive)

162 |     (replace {p = rel _} (sym ar) reflexive)

164 | namespace RelNearRing

165 |   public export %inline

166 |   plusMonoid : (rec : RelNearRing ty rel) -> RelMonoid ty rel

167 |   plusMonoid (MkRelNearRing c _ a a' _ _ l l' _ _ r r' {}) =

168 |     MkRelMonoid @{Additive} c a a' l l' r r'

170 |   public export %inline

171 |   (.plusMonoid) : (rec : RelNearRing ty rel) -> RelMonoid ty rel

172 |   (.plusMonoid) = plusMonoid

174 |   public export %inline

175 |   multMonoid : (rec : RelNearRing ty rel) -> RelMonoid ty rel

176 |   multMonoid (MkRelNearRing _ c _ _ a a' _ _ l l' _ _ r r' {}) =

177 |     MkRelMonoid @{Multiplicative} c a a' l l' r r'

179 |   public export %inline

180 |   (.multMonoid) : (rec : RelNearRing ty rel) -> RelMonoid ty rel

181 |   (.multMonoid) = multMonoid

183 | public export

184 | record RelSemiring ty (rel : Rel ty) where

185 |   constructor MkRelSemiring

186 |   {auto impl : Num ty}

187 |   plusCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x + x') (y + y')

188 |   multCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x * x') (y * y')

189 |   plusAssoc : {x,y,z : ty} -> rel ((x + y) + z) (x + (y + z))

190 |   multAssoc : {x,y,z : ty} -> rel ((x * y) * z) (x * (y * z))

191 |   multAssoc' : {x,y,z : ty} -> rel (x * (y * z)) ((x * y) * z)

192 |   plusUnit : {x : ty} -> rel (0 + x) x

193 |   plusUnit' : {x : ty} -> rel x (0 + x)

194 |   multUnitl : {x : ty} -> rel (1 * x) x

195 |   multUnitl' : {x : ty} -> rel x (1 * x)

196 |   multUnitr : {x : ty} -> rel (x * 1) x

197 |   multUnitr' : {x : ty} -> rel x (x * 1)

198 |   distribl : {x,y,z : ty} -> rel (x * (y + z)) (x * y + x * z)

199 |   distribl' : {x,y,z : ty} -> rel (x * y + x * z) (x * (y + z))

200 |   distribr : {x,y,z : ty} -> rel ((x + y) * z) (x * z + y * z)

201 |   distribr' : {x,y,z : ty} -> rel (x * z + y * z) ((x + y) * z)

202 |   absorbl : {x : ty} -> rel (x * 0) 0

203 |   absorbl' : {x : ty} -> rel 0 (x * 0)

204 |   absorbr : {x : ty} -> rel (0 * x) 0

205 |   absorbr' : {x : ty} -> rel 0 (0 * x)

206 |   plusComm : {x,y : ty} -> rel (x + y) (y + x)

208 | public export %inline

209 | mkRelSemiring :

210 |   forall ty,rel. Reflexive ty rel =>

211 |   {auto impl : Num ty} ->

212 |   (plusCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x + x') (y + y')) ->

213 |   (multCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x * x') (y * y')) ->

214 |   (0 plusAssoc : {x,y,z : ty} -> (x + y) + z = x + (y + z)) ->

215 |   (0 multAssoc : {x,y,z : ty} -> (x * y) * z = x * (y * z)) ->

216 |   (0 plusUnit : {x : ty} -> 0 + x = x) ->

217 |   (0 multUnitl : {x : ty} -> 1 * x = x) ->

218 |   (0 multUnitr : {x : ty} -> x * 1 = x) ->

219 |   (0 distribl : {x,y,z : ty} -> x * (y + z) = x * y + x * z) ->

220 |   (0 distribr : {x,y,z : ty} -> (x + y) * z = x * z + y * z) ->

221 |   (0 absorbl : {x : ty} -> x * 0 = 0) ->

222 |   (0 absorbr : {x : ty} -> 0 * x = 0) ->

223 |   (0 plusComm : {x,y : ty} -> x + y = y + x) ->

224 |   RelSemiring ty rel

225 | mkRelSemiring pc mc pa ma pu ml mr dl dr al ar pcm =

226 |   MkRelSemiring pc mc

227 |     (replace {p = rel _} pa reflexive)

228 |     (replace {p = rel _} ma reflexive)

229 |     (replace {p = rel _} (sym ma) reflexive)

230 |     (replace {p = rel _} pu reflexive)

231 |     (replace {p = rel _} (sym pu) reflexive)

232 |     (replace {p = rel _} ml reflexive)

233 |     (replace {p = rel _} (sym ml) reflexive)

234 |     (replace {p = rel _} mr reflexive)

235 |     (replace {p = rel _} (sym mr) reflexive)

236 |     (replace {p = rel _} dl reflexive)

237 |     (replace {p = rel _} (sym dl) reflexive)

238 |     (replace {p = rel _} dr reflexive)

239 |     (replace {p = rel _} (sym dr) reflexive)

240 |     (replace {p = rel _} al reflexive)

241 |     (replace {p = rel _} (sym al) reflexive)

242 |     (replace {p = rel _} ar reflexive)

243 |     (replace {p = rel _} (sym ar) reflexive)

244 |     (replace {p = rel _} pcm reflexive)

246 | namespace RelSemiring

247 |   public export %inline

248 |   relNearRing : Preorder ty rel => (rec : RelSemiring ty rel) -> RelNearRing ty rel

249 |   relNearRing (MkRelSemiring pc mc pa ma ma' pu pu' ml ml' mr mr' dl dl' dr dr' al al' ar ar' pcm) =

250 |     MkRelNearRing

251 |       pc mc pa

252 |       (transitive (pc reflexive pcm) $ transitive pcm $ transitive pa $ transitive pcm $ pc pcm reflexive)

253 |       ma ma' pu pu' ml ml' (transitive pcm pu) (transitive pu' pcm) mr mr' dl dl' dr dr' al al' ar ar'

255 |   public export %inline

256 |   (.relNearRing) : Preorder ty rel => (rec : RelSemiring ty rel) -> RelNearRing ty rel

257 |   (.relNearRing) = relNearRing

259 |   public export %inline

260 |   plusMonoid : (rec : RelSemiring ty rel) -> RelCommMonoid ty rel

261 |   plusMonoid (MkRelSemiring c _ a _ _ u u' _ _ _ _ _ _ _ _ _ _ _ _ cm) =

262 |     MkRelCommMonoid @{Additive} c a u u' cm

264 |   public export %inline

265 |   (.plusMonoid) : (rec : RelSemiring ty rel) -> RelCommMonoid ty rel

266 |   (.plusMonoid) = plusMonoid

268 |   public export %inline

269 |   multMonoid : (rec : RelSemiring ty rel) -> RelMonoid ty rel

270 |   multMonoid (MkRelSemiring _ c _ a a' _ _ l l' r r' {}) =

271 |     MkRelMonoid @{Multiplicative} c a a' l l' r r'

273 |   public export %inline

274 |   (.multMonoid) : (rec : RelSemiring ty rel) -> RelMonoid ty rel

275 |   (.multMonoid) = multMonoid

277 | public export

278 | record RelCommSemiring ty (rel : Rel ty) where

279 |   constructor MkRelCommSemiring

280 |   {auto impl : Num ty}

281 |   plusCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x + x') (y + y')

282 |   multCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x * x') (y * y')

283 |   plusAssoc : {x,y,z : ty} -> rel ((x + y) + z) (x + (y + z))

284 |   multAssoc : {x,y,z : ty} -> rel ((x * y) * z) (x * (y * z))

285 |   plusUnit : {x : ty} -> rel (0 + x) x

286 |   plusUnit' : {x : ty} -> rel x (0 + x)

287 |   multUnit : {x : ty} -> rel (1 * x) x

288 |   multUnit' : {x : ty} -> rel x (1 * x)

289 |   distrib : {x,y,z : ty} -> rel (x * (y + z)) (x * y + x * z)

290 |   distrib' : {x,y,z : ty} -> rel (x * y + x * z) (x * (y + z))

291 |   absorb : {x : ty} -> rel (x * 0) 0

292 |   absorb' : {x : ty} -> rel 0 (x * 0)

293 |   plusComm : {x,y : ty} -> rel (x + y) (y + x)

294 |   multComm : {x,y : ty} -> rel (x * y) (y * x)

296 | public export %inline

297 | mkRelCommSemiring :

298 |   forall ty,rel. Reflexive ty rel =>

299 |   {auto impl : Num ty} ->

300 |   (plusCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x + x') (y + y')) ->

301 |   (multCong : {x,x',y,y' : ty} -> rel x y -> rel x' y' -> rel (x * x') (y * y')) ->

302 |   (0 plusAssoc : {x,y,z : ty} -> (x + y) + z = x + (y + z)) ->

303 |   (0 multAssoc : {x,y,z : ty} -> (x * y) * z = x * (y * z)) ->

304 |   (0 plusUnit : {x : ty} -> 0 + x = x) ->

305 |   (0 multUnit : {x : ty} -> 1 * x = x) ->

306 |   (0 distrib : {x,y,z : ty} -> x * (y + z) = x * y + x * z) ->

307 |   (0 absorb : {x : ty} -> x * 0 = 0) ->

308 |   (0 plusComm : {x,y : ty} -> x + y = y + x) ->

309 |   (0 multComm : {x,y : ty} -> x * y = y * x) ->

310 |   RelCommSemiring ty rel

311 | mkRelCommSemiring pc mc pa ma pu mu d a pcm mcm =

312 |   MkRelCommSemiring pc mc

313 |     (replace {p = rel _} pa reflexive)

314 |     (replace {p = rel _} ma reflexive)

315 |     (replace {p = rel _} pu reflexive)

316 |     (replace {p = rel _} (sym pu) reflexive)

317 |     (replace {p = rel _} mu reflexive)

318 |     (replace {p = rel _} (sym mu) reflexive)

319 |     (replace {p = rel _} d reflexive)

320 |     (replace {p = rel _} (sym d) reflexive)

321 |     (replace {p = rel _} a reflexive)

322 |     (replace {p = rel _} (sym a) reflexive)

323 |     (replace {p = rel _} pcm reflexive)

324 |     (replace {p = rel _} mcm reflexive)

326 | namespace RelCommSemiring

327 |   public export %inline

328 |   relSemiring : Preorder ty rel => (rec : RelCommSemiring ty rel) -> RelSemiring ty rel

329 |   relSemiring (MkRelCommSemiring pc mc pa ma pu pu' mu mu' d d' a a' pcm mcm) =

330 |     MkRelSemiring

331 |       pc mc pa ma

332 |       (transitive (mc reflexive mcm) $ transitive mcm $ transitive ma $ transitive mcm $ mc mcm reflexive)

333 |       pu pu' mu mu' (transitive mcm mu) (transitive mu' mcm) d d'

334 |       (transitive mcm $ transitive d $ pc mcm mcm)

335 |       (transitive (pc mcm mcm) $ transitive d' mcm)

336 |       a a' (transitive mcm a) (transitive a' mcm) pcm

338 |   public export %inline

339 |   (.relSemiring) : Preorder ty rel => (rec : RelCommSemiring ty rel) -> RelSemiring ty rel

340 |   (.relSemiring) = relSemiring

342 |   public export %inline

343 |   plusMonoid : (rec : RelCommSemiring ty rel) -> RelCommMonoid ty rel

344 |   plusMonoid (MkRelCommSemiring c _ a _ u u' _ _ _ _ _ _ cm _) =

345 |     MkRelCommMonoid @{Additive} c a u u' cm

347 |   public export %inline

348 |   (.plusMonoid) : (rec : RelCommSemiring ty rel) -> RelCommMonoid ty rel

349 |   (.plusMonoid) = plusMonoid

351 |   public export %inline

352 |   multMonoid : (rec : RelCommSemiring ty rel) -> RelCommMonoid ty rel

353 |   multMonoid (MkRelCommSemiring _ c _ a _ _ u u' _ _ _ _ _ cm) =

354 |     MkRelCommMonoid @{Multiplicative} c a u u' cm

356 |   public export %inline

357 |   (.multMonoid) : (rec : RelCommSemiring ty rel) -> RelCommMonoid ty rel

358 |   (.multMonoid) = multMonoid

362 | namespace CategoryR

363 |   public export

364 |   Thin : (rel : Rel ty) -> Preorder ty rel => CategoryR

365 |   Thin rel = MkCategoryR rel {impl = Thin}

367 | namespace MonoidalR

368 |   public export

369 |   Thin : (rel : Rel ty) -> Preorder ty rel => RelMonoid ty rel -> MonoidalR

370 |   Thin rel (MkRelMonoid c a a' l l' r r') =

371 |     MkMonoidalR rel (<+>) neutral

372 |       {impl = MkMonoidal @{Thin} @{MkCatBifunctor c} a a' l l' r r'}

374 | namespace BraidedR

375 |   public export

376 |   Thin : (rel : Rel ty) -> Preorder ty rel => RelCommMonoid ty rel -> BraidedR

377 |   Thin rel cm@(MkRelCommMonoid {}) =

378 |     MkBraidedR rel (<+>) neutral

379 |       {impl = MkBraided @{(Thin rel cm.relMonoid).impl} cm.comm cm.comm}

381 | namespace SymmetricR

382 |   public export

383 |   Thin : (rel : Rel ty) -> Preorder ty rel => RelCommMonoid ty rel -> SymmetricR

384 |   Thin rel cm@(MkRelCommMonoid {}) =

385 |     MkSymmetricR rel (<+>) neutral

386 |       {impl = let im = (Thin rel cm).impl in MkMonSymmetric @{im} (permuteDefault @{im})}

389 | namespace BimonoidalR

390 |   public export

391 |   Thin : (rel : Rel ty) -> Preorder ty rel => RelNearRing ty rel -> BimonoidalR

392 |   Thin rel nr@(MkRelNearRing _ _ _ _ _ _ _ _ _ _ _ _ _ _ dl dl' dr dr' al al' ar ar') =

393 |     MkBimonoidalR rel (+) (*) 0 1

394 |       {impl = MkBimonoidal

395 |         @{(Thin rel nr.plusMonoid).impl}

396 |         @{(Thin rel nr.multMonoid).impl}

397 |         dl dl' dr dr' al al' ar ar'}

399 | namespace RigCategoryR

400 |   public export

401 |   Thin : (rel : Rel ty) -> Preorder ty rel => RelSemiring ty rel -> RigCategoryR

402 |   Thin rel sr@(MkRelSemiring _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ pcm) =

403 |     MkRigCategoryR rel (+) (*) 0 1

404 |       {impl = ((Thin rel sr.relNearRing).impl, (Thin rel sr.plusMonoid).impl)}

406 | namespace SymRigCategoryR

407 |   public export

408 |   Thin : (rel : Rel ty) -> Preorder ty rel => RelCommSemiring ty rel -> SymRigCategoryR

409 |   Thin rel csr@(MkRelCommSemiring _ _ _ _ _ _ _ _ _ _ _ _ _ mcm) =

410 |     MkSymRigCategoryR rel (+) (*) 0 1

411 |       {impl = ((Thin rel csr.relSemiring).impl, (Thin rel csr.multMonoid).impl)}