Hey I'm not really a mathematician but I struggled with this myself.

There are more than a few ways to do this but I don't think there's really any standard notation.

## Interpret typed lambda calculus backwards

The typed lambda calculus can be mapped to cartesian closed categories. We can also map it to the opposite of co cartesian closed categories.

Instead of the (negative) rules for tuples.

$$ \frac{\Gamma \vdash x : A , \Gamma \vdash y : B}{\Gamma \vdash \langle x , y \rangle : A \times B} $$

$$ \frac{\Gamma \vdash x : A \times B}{\Gamma \vdash \pi_1 x: A} $$

We have the rules for sums:

$$ \frac{\Gamma \vdash x : A , \Gamma \vdash y : B}{\Gamma \vdash [ x ; y ] : A + B} $$

However, we have to interpret the environment as a *sum* of variables instead of a product of variables.

If we have two patterns/case statements/contravariant functors we can sum them together.

$$ \frac{\Gamma \vdash x : A + B}{\Gamma \vdash \mathbb{left} \,x: A} $$

If we have a pattern match patterns/case statements/contravariant functor matching a sum type we can contravariantly make it more specific.

In a similar manner coexponential types are dual to exponential types.

$$ \frac{ \Gamma , x : A \vdash e : B}{\Gamma \vdash \, \mathbb{adbmal} \, x : A . e : B - A } $$

$$ \frac{ \Gamma \vdash f : B - A , \Gamma \vdash x : A}{\Gamma \vdash \, f x : B } $$

Interpreting everything backwards works but it's just really really confusing.

## Directly work with the categorical point-free combinators

Just have the usual sum types and

$$ \mathbb{councurry} : \mathbb{Hom}(A - C, B) \rightarrow \mathbb{Hom}(C, A + B) $$
$$ \mathbb{cocurry} : \mathbb{Hom}(C, A + B) \rightarrow \mathbb{Hom}(A - C, B) $$

This is kind of nice sometimes but really I miss variables.

## Reverse the categorical kappa/zeta decomposition

I wanted a nicely categorical language but with also nice variables so I found
Decomposing typed lambda calculus into a couple of categorical programming languages
In Proc. 6th International Conference on Category Theory and Computer Science (CTCS'95), Springer LNCS 953 (1995) 200-219

Pretty directly you get a sort of continuation passing style

Reversing (the positive tuple rules)

$$ \frac{\Gamma , x : 1 \rightarrow A \vdash e : B \rightarrow C }{\Gamma \vdash \kappa \, x : 1 \rightarrow A . e : A \times B \rightarrow C } $$

to

$$ \frac{\Gamma , x : A \rightarrow 0 \vdash e : C \rightarrow B }{\Gamma \vdash \mathbb{cokappa} \, x : A \rightarrow 0 . e : C \rightarrow A + B } $$

$$ \frac{\Gamma \vdash x : A \rightarrow 0}{\Gamma \vdash \mathbb{colift} \, x : A + B \rightarrow B } $$

You can kinda interpret this as like a case statement. It's still pretty confusing though.

Coexponentials become something like

$$ \frac{\Gamma , x : A \rightarrow 0 \vdash e : C \rightarrow B }{\Gamma \vdash \mathbb{cozeta} \, x : A \rightarrow 0 . e : A - C \rightarrow B } $$

$$ \frac{\Gamma \vdash x : A \rightarrow 0}{\Gamma \vdash \mathbb{copass} \, x : B \rightarrow B - A } $$

It's maybe a little clearer but still pretty awful.

## Summary

**Just do intuitionistic logic but in reverse.**

Yeah I don't really have any better ideas. Currently I'm trying to figure out the positive polarity presentation of functions. My guess is that finding dual of the positive presentation might be cleaner. I'm also still looking at the dependently typed setting. I'm going to try to reverse the calculus of constructions after I look at it enough.