2 | module Control.Category.Instances.Cat

  4 | import Control.Category

  5 | import Control.Category.Instances.Zero

  6 | import Control.Category.Instances.One

  7 | import Control.Category.Instances.Sum

  8 | import Control.Category.Instances.Prod

  9 | import Control.Category.Instances.FunCat

 10 | import Control.Category.Records

 11 | import Data.Either

 12 | import Data.Wrap0

 14 | %default total

 17 | public export

 18 | Cat : Hom CategoryR

 19 | Cat = FunctorR

 26 | public export

 27 | record Cat0 (a,b : Wrap0 CategoryR) where

 28 |   constructor MkCat0

 29 |   runCat0 : Cat a.runW0 b.runW0

 31 | public export

 32 | Cat0_ : Hom CategoryR

 33 | Cat0_ a b = Cat0 (W0 a) (W0 b)

 36 | public export

 37 | Cat0Prod : Wrap0 CategoryR -> Wrap0 CategoryR -> Wrap0 CategoryR

 38 | Cat0Prod = liftW2 Prod

 40 | public export

 41 | Cat0Sum : Wrap0 CategoryR -> Wrap0 CategoryR -> Wrap0 CategoryR

 42 | Cat0Sum = liftW2 Sum

 51 | public export

 52 | Category Cat where

 53 |   id = MkFunctorR id {impl = Id}

 54 |   MkFunctorR f {impl=fc} . MkFunctorR g {impl=gc} =

 55 |     MkFunctorR (f . g) @{Compose @{fc} @{gc}}

 57 | public export %hint

 58 | SemigroupoidCat : Semigroupoid Cat

 59 | SemigroupoidCat = FromCategory

 61 | public export

 62 | CatBifunctor Cat Cat Cat Prod where

 63 |   bimap = FunctorProd

 65 | public export

 66 | CatBifunctor Cat Cat Cat Sum where

 67 |   bimap = FunctorSum

 69 | public export

 70 | Monoidal Cat Prod One where

 71 |   assoc {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

 72 |     let fn : ((a,b),c) -> (a,(b,c))

 73 |         fn p = (fst (fst p), (snd (fst p), snd p))

 74 |         mp : Prod (Prod a b) c x y -> Prod a (Prod b c) (fn x) (fn y)

 75 |         mp (MkProd (MkProd f g) h) = MkProd f (MkProd g h)

 76 |     in MkFunctorR fn {impl = MkCatFunctor mp}

 77 |   assoc' {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

 78 |     let fn : (a,(b,c)) -> ((a,b),c)

 79 |         fn p = ((fst p, fst (snd p)), snd (snd p))

 80 |         mp : Prod a (Prod b c) x y -> Prod (Prod a b) c (fn x) (fn y)

 81 |         mp (MkProd f (MkProd g h)) = MkProd (MkProd f g) h

 82 |     in MkFunctorR fn {impl = MkCatFunctor mp}

 83 |   unitl {a=MkCategoryR{}} = MkFunctorR snd {impl = MkCatFunctor snd}

 84 |   unitl' {a=MkCategoryR{}} = MkFunctorR ((),) {impl = MkCatFunctor (MkProd MkOne)}

 85 |   unitr {a=MkCategoryR{}} = MkFunctorR fst {impl = MkCatFunctor fst}

 86 |   unitr' {a=MkCategoryR{}} = MkFunctorR (,()) {impl = MkCatFunctor (`MkProd` MkOne)}

 88 | public export

 89 | Monoidal Cat Sum Zero where

 90 |   assoc {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

 91 |     let fn : Either (Either a b) c -> Either a (Either b c)

 92 |         fn (Left (Left x)) = Left x

 93 |         fn (Left (Right x)) = Right (Left x)

 94 |         fn (Right x) = Right (Right x)

 95 |         mp : Sum (Sum a b) c x y -> Sum a (Sum b c) (fn x) (fn y)

 96 |         mp (Left (Left f)) = Left f

 97 |         mp (Left (Right f)) = Right (Left f)

 98 |         mp (Right f) = Right (Right f)

 99 |     in MkFunctorR fn {impl = MkCatFunctor mp}

100 |   assoc' {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

101 |     let fn : Either a (Either b c) -> Either (Either a b) c

102 |         fn (Left x) = Left (Left x)

103 |         fn (Right (Left x)) = Left (Right x)

104 |         fn (Right (Right x)) = Right x

105 |         mp : Sum a (Sum b c) x y -> Sum (Sum a b) c (fn x) (fn y)

106 |         mp (Left f) = Left (Left f)

107 |         mp (Right (Left f)) = Left (Right f)

108 |         mp (Right (Right f)) = Right f

109 |     in MkFunctorR fn {impl = MkCatFunctor mp}

110 |   unitl {a=MkCategoryR{}} =

111 |     let fn : Either Void a -> a

112 |         fn = either absurd id

113 |         mp : Sum Zero a x y -> a (fn x) (fn y)

114 |         mp (Left _) impossible

115 |         mp (Right f) = f

116 |     in MkFunctorR fn {impl = MkCatFunctor mp}

117 |   unitl' {a=MkCategoryR{}} = MkFunctorR Right {impl = MkCatFunctor Right}

118 |   unitr {a=MkCategoryR{}} =

119 |     let fn : Either a Void -> a

120 |         fn = either id absurd

121 |         mp : Sum a Zero x y -> a (fn x) (fn y)

122 |         mp (Left f) = f

123 |         mp (Right _) impossible

124 |     in MkFunctorR fn {impl = MkCatFunctor mp}

125 |   unitr' {a=MkCategoryR{}} = MkFunctorR Left {impl = MkCatFunctor Left}

127 | public export

128 | Braided Cat Prod One where

129 |   braid {a=MkCategoryR{},b=MkCategoryR{}} =

130 |     let mp : Prod a b x y -> Prod b a (swap x) (swap y)

131 |         mp {x=(_,_),y=(_,_)} (MkProd f g) = MkProd g f

132 |     in MkFunctorR swap {impl = MkCatFunctor mp}

134 | public export

135 | Braided Cat Sum Zero where

136 |   braid {a=MkCategoryR{},b=MkCategoryR{}} =

137 |     let mp : Sum a b x y -> Sum b a (mirror x) (mirror y)

138 |         mp (Left f) = Right f

139 |         mp (Right f) = Left f

140 |     in MkFunctorR mirror {impl = MkCatFunctor mp}

142 | public export

143 | Cartesian Cat Prod One where

144 |   projl {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR fst {impl = MkCatFunctor fst}

145 |   projr {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR snd {impl = MkCatFunctor snd}

146 |   prod {a=MkCategoryR{},b=MkCategoryR{},b'=MkCategoryR{}}

147 |     (MkFunctorR {fun=f}) (MkFunctorR {fun=g}) =

148 |       MkFunctorR (\x => (f x, g x))

149 |         {impl = MkCatFunctor $ \m => MkProd (map m) (map m)}

150 |   split {a=MkCategoryR{}} =

151 |     MkFunctorR dup {impl = MkCatFunctor $ \f => MkProd f f}

152 |   elim {a=MkCategoryR{}} =

153 |     MkFunctorR (const ()) {impl = MkCatFunctor $ const MkOne}

155 | public export %hint

156 | SymmetricCatProd : MonSymmetric Cat Prod One

157 | SymmetricCatProd = FromCartesian

159 | public export

160 | Cocartesian Cat Sum Zero where

161 |   injl {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR Left {impl = MkCatFunctor Left}

162 |   injr {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR Right {impl = MkCatFunctor Right}

163 |   coprod {a=MkCategoryR{},a'=MkCategoryR{},b=MkCategoryR{}}

164 |     (MkFunctorR {fun=f}) (MkFunctorR {fun=g}) =

165 |       MkFunctorR (either f g)

166 |         {impl = MkCatFunctor $ \case

167 |           Left f => map f

168 |           Right f => map f}

169 |   merge {a=MkCategoryR{}} =

170 |     MkFunctorR fromEither {impl = MkCatFunctor $ \case

171 |       Left f => f

172 |       Right f => f}

173 |   intro {a=MkCategoryR{}} = MkFunctorR absurd {impl = MkCatFunctor absurd}

175 | public export %hint

176 | SymmetricCatSum : MonSymmetric Cat Sum Zero

177 | SymmetricCatSum = FromCocartesian

179 | public export

180 | Bimonoidal Cat Sum Prod Zero One where

181 |   distribl {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

182 |     let fn : (a, Either b c) -> Either (a,b) (a,c)

183 |         fn (x,y) = bimap (x,) (x,) y

184 |         mp : {x,y : _} -> Prod a (Sum b c) x y -> Sum (Prod a b) (Prod a c) (fn x) (fn y)

185 |         mp {x=(_,Left _),y=(_,Left _)} (MkProd f (Left g)) = Left (MkProd f g)

186 |         mp {x=(_,Prelude.Left _),y=(_,Prelude.Right _)} (MkProd _ _) impossible

187 |         mp {x=(_,Right _),y=(_,Right _)} (MkProd f (Right g)) = Right (MkProd f g)

188 |         mp {x=(_,Prelude.Right _),y=(_,Prelude.Left _)} (MkProd _ _) impossible

189 |     in MkFunctorR fn {impl = MkCatFunctor mp}

190 |   distribl' {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

191 |     let fn : Either (a,b) (a,c) -> (a, Either b c)

192 |         fn = either (mapSnd Left) (mapSnd Right)

193 |         mp : Sum (Prod a b) (Prod a c) x y -> Prod a (Sum b c) (fn x) (fn y)

194 |         mp {x=Left (_,_),y=Left (_,_)} (Left (MkProd f g)) = MkProd f (Left g)

195 |         mp {x=Right (_,_),y=Right (_,_)} (Right (MkProd f g)) = MkProd f (Right g)

196 |     in MkFunctorR fn {impl = MkCatFunctor mp}

197 |   distribr {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

198 |     let fn : (Either a b, c) -> Either (a,c) (b,c)

199 |         fn (x,y) = bimap (,y) (,y) x

200 |         mp : {x,y : _} -> Prod (Sum a b) c x y -> Sum (Prod a c) (Prod b c) (fn x) (fn y)

201 |         mp {x=(Left _,_),y=(Left _,_)} (MkProd (Left f) g) = Left (MkProd f g)

202 |         mp {x=(Prelude.Left _,_),y=(Prelude.Right _,_)} (MkProd _ _) impossible

203 |         mp {x=(Right _,_),y=(Right _,_)} (MkProd (Right f) g) = Right (MkProd f g)

204 |         mp {x=(Prelude.Right _,_),y=(Prelude.Left _,_)} (MkProd _ _) impossible

205 |     in MkFunctorR fn {impl = MkCatFunctor mp}

206 |   distribr' {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

207 |     let fn : Either (a,c) (b,c) -> (Either a b, c)

208 |         fn = either (mapFst Left) (mapFst Right)

209 |         mp : Sum (Prod a c) (Prod b c) x y -> Prod (Sum a b) c (fn x) (fn y)

210 |         mp {x=Left (_,_),y=Left (_,_)} (Left (MkProd f g)) = MkProd (Left f) g

211 |         mp {x=Right (_,_),y=Right (_,_)} (Right (MkProd f g)) = MkProd (Right f) g

212 |     in MkFunctorR fn {impl = MkCatFunctor mp}

213 |   absorbl {a=MkCategoryR{}} = MkFunctorR snd {impl = MkCatFunctor snd}

214 |   absorbl' {a=MkCategoryR{}} = MkFunctorR absurd {impl = MkCatFunctor absurd}

215 |   absorbr {a=MkCategoryR{}} = MkFunctorR fst {impl = MkCatFunctor fst}

216 |   absorbr' {a=MkCategoryR{}} = MkFunctorR absurd {impl = MkCatFunctor absurd}

218 | public export

219 | Closed Cat Prod FunCat One where

220 |   curry {a=a@(MkCategoryR{}),b=b@(MkCategoryR{}),c=MkCategoryR{}}

221 |     f@(MkFunctorR {fun}) =

222 |         MkFunctorR (\x => MkFunctorR (curry fun x)

223 |                         {impl = MkCatFunctor $ \m => f.map (MkProd a.id m)})

224 |         {impl = MkCatFunctor $ \m => MkNatTransR (f.map (MkProd m b.id))}

225 |   uncurry {a=a@(MkCategoryR {}),b=b@(MkCategoryR {}),c=c@(MkCategoryR {})}

226 |     f@(MkFunctorR {fun}) =

227 |       let fn : (a.obj, b.obj) -> c.obj

228 |           fn p = (fun $ fst p).fun $ snd p

229 |           mp : {x,y : _} -> Prod a.hom b.hom x y -> c.hom (fn x) (fn y)

230 |           mp {x=(_,_),y=(ya,_)} (MkProd m m') = c.comp ((fun ya).map m') (f.map m).fun

231 |       in MkFunctorR fn {impl = MkCatFunctor mp}

235 | public export

236 | Category Cat0 where

237 |   id = MkCat0 $ MkFunctorR id {impl = Id}

238 |   MkCat0 (MkFunctorR f {impl=fc}) . MkCat0(MkFunctorR g {impl=gc}) =

239 |     MkCat0 (MkFunctorR (f . g) @{Compose @{fc} @{gc}})

241 | public export %hint

242 | SemigroupoidCat0 : Semigroupoid Cat0

243 | SemigroupoidCat0 = FromCategory

245 | public export

246 | CatBifunctor Cat0 Cat0 Cat0 Cat0Prod where

247 |   bimap (MkCat0 f) (MkCat0 g) = MkCat0 $ FunctorProd f g

249 | public export

250 | CatBifunctor Cat0 Cat0 Cat0 Cat0Sum where

251 |   bimap (MkCat0 f) (MkCat0 g) = MkCat0 $ FunctorSum f g

253 | public export

254 | Monoidal Cat0 Cat0Prod (W0 One) where

255 |   assoc {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ assoc_ {a,b,c}

256 |     where

257 |       assoc_ : forall a,b,c. Cat (Prod (Prod a b) c) (Prod a (Prod b c))

258 |       assoc_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

259 |         let fn : forall a,b,c. ((a,b),c) -> (a,(b,c))

260 |             fn p = (fst (fst p), (snd (fst p), snd p))

261 |             mp : forall a,b,c. Prod (Prod a b) c x y -> Prod a (Prod b c) (fn x) (fn y)

262 |             mp (MkProd (MkProd f g) h) = MkProd f (MkProd g h)

263 |         in MkFunctorR fn {impl = MkCatFunctor mp}

264 |   assoc' {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ assoc'_ {a,b,c}

265 |     where

266 |       assoc'_ : forall a,b,c. Cat (Prod a (Prod b c)) (Prod (Prod a b) c)

267 |       assoc'_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

268 |         let fn : forall a,b,c. (a,(b,c)) -> ((a,b),c)

269 |             fn p = ((fst p, fst (snd p)), snd (snd p))

270 |             mp : forall a,b,c. Prod a (Prod b c) x y -> Prod (Prod a b) c (fn x) (fn y)

271 |             mp (MkProd f (MkProd g h)) = MkProd (MkProd f g) h

272 |         in MkFunctorR fn {impl = MkCatFunctor mp}

273 |   unitl {a=W0 a} = MkCat0 $ unitl_ {a}

274 |     where

275 |       unitl_ : forall a. Cat (Prod One a) a

276 |       unitl_ {a=MkCategoryR{}} = MkFunctorR snd {impl = MkCatFunctor snd}

277 |   unitl' {a=W0 a} = MkCat0 $ unitl'_ {a}

278 |     where

279 |       unitl'_ : forall a. Cat a (Prod One a)

280 |       unitl'_ {a=MkCategoryR{}} = MkFunctorR ((),) {impl = MkCatFunctor (MkProd MkOne)}

281 |   unitr {a=W0 a} = MkCat0 $ unitr_ {a}

282 |     where

283 |       unitr_ : forall a. Cat (Prod a One) a

284 |       unitr_ {a=MkCategoryR{}} = MkFunctorR fst {impl = MkCatFunctor fst}

285 |   unitr' {a=W0 a} = MkCat0 $ unitr'_ {a}

286 |     where

287 |       unitr'_ : forall a. Cat a (Prod a One)

288 |       unitr'_ {a=MkCategoryR{}} = MkFunctorR (,()) {impl = MkCatFunctor (`MkProd` MkOne)}

290 | public export

291 | Monoidal Cat0 Cat0Sum (W0 Zero) where

292 |   assoc {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ assoc_ {a,b,c}

293 |     where

294 |       assoc_ : forall a,b,c. Cat (Sum (Sum a b) c) (Sum a (Sum b c))

295 |       assoc_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

296 |         let fn : forall a,b,c. Either (Either a b) c -> Either a (Either b c)

297 |             fn (Left (Left x)) = Left x

298 |             fn (Left (Right x)) = Right (Left x)

299 |             fn (Right x) = Right (Right x)

300 |             mp : forall a,b,c. Sum (Sum a b) c x y -> Sum a (Sum b c) (fn x) (fn y)

301 |             mp (Left (Left f)) = Left f

302 |             mp (Left (Right f)) = Right (Left f)

303 |             mp (Right f) = Right (Right f)

304 |         in MkFunctorR fn {impl = MkCatFunctor mp}

305 |   assoc' {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ assoc'_ {a,b,c}

306 |     where

307 |       assoc'_ : forall a,b,c. Cat (Sum a (Sum b c)) (Sum (Sum a b) c)

308 |       assoc'_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

309 |         let fn : forall a,b,c. Either a (Either b c) -> Either (Either a b) c

310 |             fn (Left x) = Left (Left x)

311 |             fn (Right (Left x)) = Left (Right x)

312 |             fn (Right (Right x)) = Right x

313 |             mp : forall a,b,c. Sum a (Sum b c) x y -> Sum (Sum a b) c (fn x) (fn y)

314 |             mp (Left f) = Left (Left f)

315 |             mp (Right (Left f)) = Left (Right f)

316 |             mp (Right (Right f)) = Right f

317 |         in MkFunctorR fn {impl = MkCatFunctor mp}

318 |   unitl {a=W0 a} = MkCat0 $ unitl_ {a}

319 |     where

320 |       unitl_ : forall a. Cat (Sum Zero a) a

321 |       unitl_ {a=MkCategoryR{}} =

322 |         let fn : forall a. Either Void a -> a

323 |             fn = either absurd id

324 |             mp : forall a. Sum Zero a x y -> a (fn x) (fn y)

325 |             mp (Left _) impossible

326 |             mp (Right f) = f

327 |         in MkFunctorR fn {impl = MkCatFunctor mp}

328 |   unitl' {a=W0 a} = MkCat0 $ unitl'_ {a}

329 |     where

330 |       unitl'_ : forall a. Cat a (Sum Zero a)

331 |       unitl'_ {a=MkCategoryR{}} = MkFunctorR Right {impl = MkCatFunctor Right}

332 |   unitr {a=W0 a} = MkCat0 $ unitr_ {a}

333 |     where

334 |       unitr_ : forall a. Cat (Sum a Zero) a

335 |       unitr_ {a=MkCategoryR{}} =

336 |         let fn : forall a. Either a Void -> a

337 |             fn = either id absurd

338 |             mp : forall a. Sum a Zero x y -> a (fn x) (fn y)

339 |             mp (Left f) = f

340 |             mp (Right _) impossible

341 |         in MkFunctorR fn {impl = MkCatFunctor mp}

342 |   unitr' {a=W0 a} = MkCat0 $ unitr'_ {a}

343 |     where

344 |       unitr'_ : forall a. Cat a (Sum a Zero)

345 |       unitr'_ {a=MkCategoryR{}} = MkFunctorR Left {impl = MkCatFunctor Left}

347 | public export

348 | Braided Cat0 Cat0Prod (W0 One) where

349 |   braid {a=W0 a,b=W0 b} = MkCat0 $ braid_ {a,b}

350 |     where

351 |       braid_ : forall a,b. Cat (Prod a b) (Prod b a)

352 |       braid_ {a=MkCategoryR{},b=MkCategoryR{}} =

353 |         let mp : forall a,b. Prod a b x y -> Prod b a (swap x) (swap y)

354 |             mp {x=(_,_),y=(_,_)} (MkProd f g) = MkProd g f

355 |         in MkFunctorR swap {impl = MkCatFunctor mp}

357 | public export

358 | Braided Cat0 Cat0Sum (W0 Zero) where

359 |   braid {a=W0 a,b=W0 b} = MkCat0 $ braid_ {a,b}

360 |     where

361 |       braid_ : forall a,b. Cat (Sum a b) (Sum b a)

362 |       braid_ {a=MkCategoryR{},b=MkCategoryR{}} =

363 |         let mp : forall a,b. Sum a b x y -> Sum b a (mirror x) (mirror y)

364 |             mp (Left f) = Right f

365 |             mp (Right f) = Left f

366 |         in MkFunctorR mirror {impl = MkCatFunctor mp}

368 | public export

369 | Cartesian Cat0 Cat0Prod (W0 One) where

370 |   projl {a=W0 a,b=W0 b} = MkCat0 $ projl_ {a,b}

371 |     where

372 |       projl_ : forall a,b. Cat (Prod a b) a

373 |       projl_ {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR fst {impl = MkCatFunctor fst}

374 |   projr {a=W0 a,b=W0 b} = MkCat0 $ projr_ {a,b}

375 |     where

376 |       projr_ : forall a,b. Cat (Prod a b) b

377 |       projr_ {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR snd {impl = MkCatFunctor snd}

378 |   prod {a=W0 a,b=W0 b,b'=W0 b'} (MkCat0 f) (MkCat0 g) = MkCat0 $ prod_ {a,b,b'} f g

379 |     where

380 |       prod_ : forall a,b,b'. Cat a b -> Cat a b' -> Cat a (Prod b b')

381 |       prod_ {a=MkCategoryR{},b=MkCategoryR{},b'=MkCategoryR{}}

382 |         (MkFunctorR {fun=f}) (MkFunctorR {fun=g}) =

383 |         MkFunctorR (\x => (f x, g x))

384 |             {impl = MkCatFunctor $ \m => MkProd (map m) (map m)}

386 | public export %hint

387 | SymmetricCat0Prod : MonSymmetric Cat0 Cat0Prod (W0 One)

388 | SymmetricCat0Prod = FromCartesian

390 | public export

391 | Cocartesian Cat0 Cat0Sum (W0 Zero) where

392 |   injl {a=W0 a,b=W0 b} = MkCat0 $ injl_ {a,b}

393 |     where

394 |       injl_ : forall a,b. Cat a (Sum a b)

395 |       injl_ {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR Left {impl = MkCatFunctor Left}

396 |   injr {a=W0 a,b=W0 b} = MkCat0 $ injr_ {a,b}

397 |     where

398 |       injr_ : forall a,b. Cat b (Sum a b)

399 |       injr_ {a=MkCategoryR{},b=MkCategoryR{}} = MkFunctorR Right {impl = MkCatFunctor Right}

400 |   coprod {a=W0 a,a'=W0 a',b=W0 b} (MkCat0 f) (MkCat0 g) = MkCat0 $ coprod_ f g

401 |     where

402 |       coprod_ : forall a,a',b. Cat a b -> Cat a' b -> Cat (Sum a a') b

403 |       coprod_ {a=MkCategoryR{},a'=MkCategoryR{},b=MkCategoryR{}}

404 |         (MkFunctorR {fun=f}) (MkFunctorR {fun=g}) =

405 |           MkFunctorR (either f g)

406 |             {impl = MkCatFunctor $ \case

407 |               Left f => map f

408 |               Right f => map f}

410 | public export %hint

411 | SymmetricCat0Sum : MonSymmetric Cat0 Cat0Sum (W0 Zero)

412 | SymmetricCat0Sum = FromCocartesian

414 | public export

415 | Bimonoidal Cat0 Cat0Sum Cat0Prod (W0 Zero) (W0 One) where

416 |   distribl {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ distribl_ {a,b,c}

417 |     where

418 |       distribl_ : forall a,b,c. Cat (Prod a (Sum b c)) (Sum (Prod a b) (Prod a c))

419 |       distribl_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

420 |         let fn : forall a,b,c. (a, Either b c) -> Either (a,b) (a,c)

421 |             fn (x,y) = bimap (x,) (x,) y

422 |             mp : {x,y : _} -> forall a,b,c. Prod a (Sum b c) x y -> Sum (Prod a b) (Prod a c) (fn x) (fn y)

423 |             mp {x=(_,Left _),y=(_,Left _)} (MkProd f (Left g)) = Left (MkProd f g)

424 |             mp {x=(_,Prelude.Left _),y=(_,Prelude.Right _)} (MkProd _ _) impossible

425 |             mp {x=(_,Right _),y=(_,Right _)} (MkProd f (Right g)) = Right (MkProd f g)

426 |             mp {x=(_,Prelude.Right _),y=(_,Prelude.Left _)} (MkProd _ _) impossible

427 |         in MkFunctorR fn {impl = MkCatFunctor mp}

428 |   distribl' {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ distribl'_ {a,b,c}

429 |     where

430 |       distribl'_ : forall a,b,c. Cat (Sum (Prod a b) (Prod a c)) (Prod a (Sum b c))

431 |       distribl'_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

432 |         let fn : forall a,b,c. Either (a,b) (a,c) -> (a, Either b c)

433 |             fn = either (mapSnd Left) (mapSnd Right)

434 |             mp : forall a,b,c. Sum (Prod a b) (Prod a c) x y -> Prod a (Sum b c) (fn x) (fn y)

435 |             mp {x=Left (_,_),y=Left (_,_)} (Left (MkProd f g)) = MkProd f (Left g)

436 |             mp {x=Right (_,_),y=Right (_,_)} (Right (MkProd f g)) = MkProd f (Right g)

437 |         in MkFunctorR fn {impl = MkCatFunctor mp}

438 |   distribr {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ distribr_ {a,b,c}

439 |     where

440 |       distribr_ : forall a,b,c. Cat (Prod (Sum a b) c) (Sum (Prod a c) (Prod b c))

441 |       distribr_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

442 |         let fn : forall a,b,c. (Either a b, c) -> Either (a,c) (b,c)

443 |             fn (x,y) = bimap (,y) (,y) x

444 |             mp : {x,y : _} -> forall a,b,c. Prod (Sum a b) c x y -> Sum (Prod a c) (Prod b c) (fn x) (fn y)

445 |             mp {x=(Left _,_),y=(Left _,_)} (MkProd (Left f) g) = Left (MkProd f g)

446 |             mp {x=(Prelude.Left _,_),y=(Prelude.Right _,_)} (MkProd _ _) impossible

447 |             mp {x=(Right _,_),y=(Right _,_)} (MkProd (Right f) g) = Right (MkProd f g)

448 |             mp {x=(Prelude.Right _,_),y=(Prelude.Left _,_)} (MkProd _ _) impossible

449 |         in MkFunctorR fn {impl = MkCatFunctor mp}

450 |   distribr' {a=W0 a,b=W0 b,c=W0 c} = MkCat0 $ distribr'_ {a,b,c}

451 |     where

452 |       distribr'_ : forall a,b,c. Cat (Sum (Prod a c) (Prod b c)) (Prod (Sum a b) c)

453 |       distribr'_ {a=MkCategoryR{},b=MkCategoryR{},c=MkCategoryR{}} =

454 |         let fn : forall a,b,c. Either (a,c) (b,c) -> (Either a b, c)

455 |             fn = either (mapFst Left) (mapFst Right)

456 |             mp : forall a,b,c. Sum (Prod a c) (Prod b c) x y -> Prod (Sum a b) c (fn x) (fn y)

457 |             mp {x=Left (_,_),y=Left (_,_)} (Left (MkProd f g)) = MkProd (Left f) g

458 |             mp {x=Right (_,_),y=Right (_,_)} (Right (MkProd f g)) = MkProd (Right f) g

459 |         in MkFunctorR fn {impl = MkCatFunctor mp}

460 |   absorbl {a=W0 a} = MkCat0 $ absorbl_ {a}

461 |     where

462 |       absorbl_ : forall a. Cat (Prod a Zero) Zero

463 |       absorbl_ {a=MkCategoryR{}} = MkFunctorR snd {impl = MkCatFunctor snd}

464 |   absorbl' {a=W0 a} = MkCat0 $ absorbl'_ {a}

465 |     where

466 |       absorbl'_ : forall a. Cat Zero (Prod a Zero)

467 |       absorbl'_ {a=MkCategoryR{}} = MkFunctorR absurd {impl = MkCatFunctor absurd}

468 |   absorbr {a=W0 a} = MkCat0 $ absorbr_ {a}

469 |     where

470 |       absorbr_ : forall a. Cat (Prod Zero a) Zero

471 |       absorbr_ {a=MkCategoryR{}} = MkFunctorR fst {impl = MkCatFunctor fst}

472 |   absorbr' {a=W0 a} = MkCat0 $ absorbr'_ {a}

473 |     where

474 |       absorbr'_ : forall a. Cat Zero (Prod Zero a)

475 |       absorbr'_ {a=MkCategoryR{}} = MkFunctorR absurd {impl = MkCatFunctor absurd}

482 | namespace SemigroupoidR

483 |   public export

484 |   Cat : SemigroupoidR

485 |   Cat = MkSemigroupoidR Cat

487 |   public export

488 |   Cat0 : SemigroupoidR

489 |   Cat0 = MkSemigroupoidR Cat0

491 | namespace CategoryR

492 |   public export

493 |   Cat : CategoryR

494 |   Cat = MkCategoryR Cat

496 |   public export

497 |   Cat0 : CategoryR

498 |   Cat0 = MkCategoryR Cat0

500 | namespace MonoidalR

501 |   public export

502 |   CatProd : MonoidalR

503 |   CatProd = MkMonoidalR Cat Prod One

505 |   public export

506 |   CatSum : MonoidalR

507 |   CatSum = MkMonoidalR Cat Sum Zero

509 |   public export

510 |   Cat0Prod : MonoidalR

511 |   Cat0Prod = MkMonoidalR Cat0 Cat0Prod (W0 One)

513 |   public export

514 |   Cat0Sum : MonoidalR

515 |   Cat0Sum = MkMonoidalR Cat0 Cat0Sum (W0 Zero)

517 | namespace BraidedR

518 |   public export

519 |   CatProd : BraidedR

520 |   CatProd = MkBraidedR Cat Prod One

522 |   public export

523 |   CatSum : BraidedR

524 |   CatSum = MkBraidedR Cat Sum Zero

526 |   public export

527 |   Cat0Prod : BraidedR

528 |   Cat0Prod = MkBraidedR Cat0 Cat0Prod (W0 One)

530 |   public export

531 |   Cat0Sum : BraidedR

532 |   Cat0Sum = MkBraidedR Cat0 Cat0Sum (W0 Zero)

534 | namespace SymmetricR

535 |   public export

536 |   CatProd : SymmetricR

537 |   CatProd = MkSymmetricR Cat Prod One

539 |   public export

540 |   CatSum : SymmetricR

541 |   CatSum = MkSymmetricR Cat Sum Zero

543 |   public export

544 |   Cat0Prod : SymmetricR

545 |   Cat0Prod = MkSymmetricR Cat0 Cat0Prod (W0 One)

547 |   public export

548 |   Cat0Sum : SymmetricR

549 |   Cat0Sum = MkSymmetricR Cat0 Cat0Sum (W0 Zero)

551 | namespace CartesianR

552 |   public export

553 |   Cat : CartesianR

554 |   Cat = MkCartesianR Cat Prod One

556 |   public export

557 |   Cat0 : CartesianR

558 |   Cat0 = MkCartesianR Cat0 Cat0Prod (W0 One)

560 | namespace CocartesianR

561 |   public export

562 |   Cat : CocartesianR

563 |   Cat = MkCocartesianR Cat Sum Zero

565 |   public export

566 |   Cat0 : CocartesianR

567 |   Cat0 = MkCocartesianR Cat0 Cat0Sum (W0 Zero)

569 | namespace BimonoidalR

570 |   public export

571 |   Cat : BimonoidalR

572 |   Cat = MkBimonoidalR Cat Sum Prod Zero One

574 |   public export

575 |   Cat0 : BimonoidalR

576 |   Cat0 = MkBimonoidalR Cat0 Cat0Sum Cat0Prod (W0 Zero) (W0 One)

578 | namespace RigCategoryR

579 |   public export

580 |   Cat : RigCategoryR

581 |   Cat = MkRigCategoryR Cat Sum Prod Zero One

583 |   public export

584 |   Cat0 : RigCategoryR

585 |   Cat0 = MkRigCategoryR Cat0 Cat0Sum Cat0Prod (W0 Zero) (W0 One)

587 | namespace SymRigCategoryR

588 |   public export

589 |   Cat : SymRigCategoryR

590 |   Cat = MkSymRigCategoryR Cat Sum Prod Zero One

592 |   public export

593 |   Cat0 : SymRigCategoryR

594 |   Cat0 = MkSymRigCategoryR Cat0 Cat0Sum Cat0Prod (W0 Zero) (W0 One)

596 | namespace DistributiveR

597 |   public export

598 |   Cat : DistributiveR

599 |   Cat = MkDistributiveR Cat Sum Prod Zero One

601 |   public export

602 |   Cat0 : DistributiveR

603 |   Cat0 = MkDistributiveR Cat0 Cat0Sum Cat0Prod (W0 Zero) (W0 One)

605 | namespace ClosedR

606 |   public export

607 |   Cat : ClosedR

608 |   Cat = MkClosedR Cat Prod FunCat One

610 | namespace CartesianClosedR

611 |   public export

612 |   Cat : CartesianClosedR

613 |   Cat = MkCartesianClosedR Cat Prod FunCat One