Agda Smash

Formal specification of Haskell smash library in Agda.

From programming point of view provided data types Smash, Wedge and Can can treated as different possiblities how to combine two types same as: Product, Sum and These:

Product, Sum and These show how to combine types in sets, where Smash, Wedge and Can do the same for pointed ses:

description	sets	algebra in setss	pointed sets	algebra in pointed sets
both	Product	A * B	Smash product	1 + (A * B)
on of them	Sum	A + B	Wedge sum	1 + A + B
bot of one of them	These	A + B + (A * B)	Can	1 + A + B + (A * B)

Smash product is canonical tensor product of pointed sets in a category, vien by taking product of underlying objects and indentifying with new basepoint - basepoints from ingredients.

data Smash (A : Set) (B : Set) : Set where
  nada  :           Smash A B
  smash : A -> B -> Smash A B

nada ----+---- smash A B

Wedge sum of two pointed sets A and B is the quotient set of the disjoint union A + B where both copies of the basepoint are identified.

data Wedge (A : Set)(B : Set) : Set where
  nowhere :           Wedge A B
  here    : A ->      Wedge A B
  there   :      B -> Wedge A B

         here A
            |
            |
nowhere ----+
            |
            |
          there B

Can combines smash product with wedge sum:

data Can (A : Set)(B : Set) : Set where
  non : Can A B
  one : A      -> Can A B
  eno :      B -> Can A B
  two : A -> B -> Can A B

      one A
        |
        |
Non ----+----- two A B
        |
        |
      eno B

Building

Project can be build using make:

make

or nix:

nix build

Update nix flakes:

nix flake update