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

156 | Cocartesian Cat Sum Zero where

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

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

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

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

161 |       MkFunctorR (either f g)

162 |         {impl = MkCatFunctor $ \case

163 |           Left f => map f

164 |           Right f => map f}

165 |   merge {a=MkCategoryR{}} =

166 |     MkFunctorR fromEither {impl = MkCatFunctor $ \case

167 |       Left f => f

168 |       Right f => f}

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

171 | public export

172 | Bimonoidal Cat Sum Prod Zero One where

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

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

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

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

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

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

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

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

181 |     in MkFunctorR fn {impl = MkCatFunctor mp}

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

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

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

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

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

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

188 |     in MkFunctorR fn {impl = MkCatFunctor mp}

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

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

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

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

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

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

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

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

197 |     in MkFunctorR fn {impl = MkCatFunctor mp}

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

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

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

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

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

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

204 |     in MkFunctorR fn {impl = MkCatFunctor mp}

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

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

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

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

210 | public export

211 | Closed Cat Prod FunCat One where

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

213 |     f@(MkFunctorR {fun}) =

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

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

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

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

218 |     f@(MkFunctorR {fun}) =

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

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

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

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

223 |       in MkFunctorR fn {impl = MkCatFunctor mp}

227 | public export

228 | Category Cat0 where

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

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

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

233 | public export %hint

234 | SemigroupoidCat0 : Semigroupoid Cat0

235 | SemigroupoidCat0 = FromCategory

237 | public export

238 | CatBifunctor Cat0 Cat0 Cat0 Cat0Prod where

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

241 | public export

242 | CatBifunctor Cat0 Cat0 Cat0 Cat0Sum where

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

245 | public export

246 | Monoidal Cat0 Cat0Prod (W0 One) where

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

248 |     where

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

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

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

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

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

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

255 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

257 |     where

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

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

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

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

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

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

264 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

266 |     where

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

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

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

270 |     where

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

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

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

274 |     where

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

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

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

278 |     where

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

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

282 | public export

283 | Monoidal Cat0 Cat0Sum (W0 Zero) where

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

285 |     where

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

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

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

289 |             fn (Left (Left x)) = Left x

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

291 |             fn (Right x) = Right (Right x)

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

293 |             mp (Left (Left f)) = Left f

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

295 |             mp (Right f) = Right (Right f)

296 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

298 |     where

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

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

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

302 |             fn (Left x) = Left (Left x)

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

304 |             fn (Right (Right x)) = Right x

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

306 |             mp (Left f) = Left (Left f)

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

308 |             mp (Right (Right f)) = Right f

309 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

311 |     where

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

313 |       unitl_ {a=MkCategoryR{}} =

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

315 |             fn = either absurd id

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

317 |             mp (Left _) impossible

318 |             mp (Right f) = f

319 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

321 |     where

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

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

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

325 |     where

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

327 |       unitr_ {a=MkCategoryR{}} =

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

329 |             fn = either id absurd

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

331 |             mp (Left f) = f

332 |             mp (Right _) impossible

333 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

335 |     where

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

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

339 | public export

340 | Braided Cat0 Cat0Prod (W0 One) where

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

342 |     where

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

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

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

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

347 |         in MkFunctorR swap {impl = MkCatFunctor mp}

349 | public export

350 | Braided Cat0 Cat0Sum (W0 Zero) where

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

352 |     where

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

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

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

356 |             mp (Left f) = Right f

357 |             mp (Right f) = Left f

358 |         in MkFunctorR mirror {impl = MkCatFunctor mp}

360 | public export

361 | Cartesian Cat0 Cat0Prod (W0 One) where

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

363 |     where

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

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

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

367 |     where

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

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

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

371 |     where

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

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

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

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

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

378 | public export

379 | Cocartesian Cat0 Cat0Sum (W0 Zero) where

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

381 |     where

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

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

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

385 |     where

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

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

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

389 |     where

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

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

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

393 |           MkFunctorR (either f g)

394 |             {impl = MkCatFunctor $ \case

395 |               Left f => map f

396 |               Right f => map f}

398 | public export

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

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

401 |     where

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

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

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

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

406 |             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)

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

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

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

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

411 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

413 |     where

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

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

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

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

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

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

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

421 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

423 |     where

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

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

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

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

428 |             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)

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

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

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

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

433 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

435 |     where

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

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

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

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

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

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

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

443 |         in MkFunctorR fn {impl = MkCatFunctor mp}

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

445 |     where

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

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

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

449 |     where

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

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

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

453 |     where

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

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

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

457 |     where

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

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

466 | namespace SemigroupoidR

467 |   public export

468 |   Cat : SemigroupoidR

469 |   Cat = MkSemigroupoidR Cat

471 |   public export

472 |   Cat0 : SemigroupoidR

473 |   Cat0 = MkSemigroupoidR Cat0

475 | namespace CategoryR

476 |   public export

477 |   Cat : CategoryR

478 |   Cat = MkCategoryR Cat

480 |   public export

481 |   Cat0 : CategoryR

482 |   Cat0 = MkCategoryR Cat0

484 | namespace MonoidalR

485 |   public export

486 |   CatProd : MonoidalR

487 |   CatProd = MkMonoidalR Cat Prod One

489 |   public export

490 |   CatSum : MonoidalR

491 |   CatSum = MkMonoidalR Cat Sum Zero

493 |   public export

494 |   Cat0Prod : MonoidalR

495 |   Cat0Prod = MkMonoidalR Cat0 Cat0Prod (W0 One)

497 |   public export

498 |   Cat0Sum : MonoidalR

499 |   Cat0Sum = MkMonoidalR Cat0 Cat0Sum (W0 Zero)

501 | namespace BraidedR

502 |   public export

503 |   CatProd : BraidedR

504 |   CatProd = MkBraidedR Cat Prod One

506 |   public export

507 |   CatSum : BraidedR

508 |   CatSum = MkBraidedR Cat Sum Zero

510 |   public export

511 |   Cat0Prod : BraidedR

512 |   Cat0Prod = MkBraidedR Cat0 Cat0Prod (W0 One)

514 |   public export

515 |   Cat0Sum : BraidedR

516 |   Cat0Sum = MkBraidedR Cat0 Cat0Sum (W0 Zero)

518 | namespace CartesianR

519 |   public export

520 |   Cat : CartesianR

521 |   Cat = MkCartesianR Cat Prod One

523 |   public export

524 |   Cat0 : CartesianR

525 |   Cat0 = MkCartesianR Cat0 Cat0Prod (W0 One)

527 | namespace CocartesianR

528 |   public export

529 |   Cat : CocartesianR

530 |   Cat = MkCocartesianR Cat Sum Zero

532 |   public export

533 |   Cat0 : CocartesianR

534 |   Cat0 = MkCocartesianR Cat0 Cat0Sum (W0 Zero)

536 | namespace BimonoidalR

537 |   public export

538 |   Cat : BimonoidalR

539 |   Cat = MkBimonoidalR Cat Sum Prod Zero One

541 |   public export

542 |   Cat0 : BimonoidalR

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

545 | namespace RigCategoryR

546 |   public export

547 |   Cat : RigCategoryR

548 |   Cat = MkRigCategoryR Cat Sum Prod Zero One

550 |   public export

551 |   Cat0 : RigCategoryR

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

554 | namespace SymRigCategoryR

555 |   public export

556 |   Cat : SymRigCategoryR

557 |   Cat = MkSymRigCategoryR Cat Sum Prod Zero One

559 |   public export

560 |   Cat0 : SymRigCategoryR

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

563 | namespace DistributiveR

564 |   public export

565 |   Cat : DistributiveR

566 |   Cat = MkDistributiveR Cat Sum Prod Zero One

568 |   public export

569 |   Cat0 : DistributiveR

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

572 | namespace ClosedR

573 |   public export

574 |   Cat : ClosedR

575 |   Cat = MkClosedR Cat Prod FunCat One

577 | namespace CartesianClosedR

578 |   public export

579 |   Cat : CartesianClosedR

580 |   Cat = MkCartesianClosedR Cat Prod FunCat One