(co)Cartesian structures

ohnosequences / stuff

Useful stuff.

GNU Affero General Public License v3.0

1 stars 0 forks source link

Closed eparejatobes closed 6 years ago

eparejatobes commented 7 years ago

[x] categories with products
[x] categories with sums
[x] derive (symmetric) monoidal structures
- [x] implement assocs in terms of (co)products
[x] syntax: This is mostly implemented. Needs some cleaning and minimal tests.
[x] use only syntax for categories with (co)products when using tuples and sums
[x] aliases for (co)cartesian monoidal structure

eparejatobes commented 7 years ago

eparejatobes commented 7 years ago

I'm leaving this out of 0.4.0.

eparejatobes commented 7 years ago

I want to have a convenient arity-free syntax for products and sums. Options:

// for the product-induced map
val z: X -> (A × B × C) = 
  f ^ g ^ h
  // alternatives?

val u: (A + B + C) -> X =
  f | g | h
  // alternatives?

eparejatobes commented 6 years ago

There's already too much in here. I'm going to merge this and work on any deficiencies in separate PRs.