A modern programming language that makes developers happier.

kotlinlang

```@Proof(Subtyping)
inline fun &lt;A&gt; A.first(): Union4&lt;A, Any?, Any?, Any?&gt;```

I have inverted the runtime as encoded in Arrow to make it leaners so there is a single interface and single inline class. Nothing in a proof position is assignable to unions that would have included types not in the unions based on this encoding

<https://github.com/arrow-kt/arrow-meta/blob/829176e97454c6653b1b1332675837f5513225cc/prelude/src/main/kotlin/arrow/unions.kt#L13>

proofs need to be applicable by their upperbound since they are polymorphic

Proofs are a way to encode the Curry - Howard correspondence as a meta library for Kotlin

since you can draw morphisms in the category of the Kotlin Types where the types are the objects

and in a directed graph you can walk the graph with Dijstra shortest path or similar to find inductive proofs like the ones for tuples and hlist