# Leibniz Scala Library

The Leibniz’ equality law states that if `a`

and `b`

are identical then they
must have identical properties. Leibniz’ original definition reads as follows:

```
a ≡ b = ∀ f .f a ⇔ f b
```

and can be proven to be equivalent to:

```
a ≡ b = ∀ f .f a → f b
```

This library provides an encoding of Leibniz' equality and other related concepts in Scala. See my impromptu LC 2018 presentation for an overview.

### Witnesses

`Is[A, B]`

(with a type alias to`A === B`

) witnesses that types`A`

and`B`

are exactly the same.- Similarly,
`IsK[A, B]`

(with a type alias to`A =~= B`

) witnesses that types`A[_]`

and`B[_]`

are exactly the same. Combinators exist that allow you to prove that`F[A] === F[B]`

for any`F[_[_]]`

or that`A[X] === B[X]`

for any`X`

. `Leibniz[L, H, A, B]`

witnesses that types`A`

and`B`

are the same and that they both are in between types`L`

and`H`

.`Is[F, A, B]`

witnesses type-equality for F-Bounded types.`As[A, B]`

witnesses that`A`

is a subtype of`B`

.`As1[A, B]`

witnesses that`A`

is a subtype of`B`

using existential types.`Liskov[L, H, A, B]`

is a bounded counterpart to`As[A, B]`

.`Constant[F]`

witnesses that HKT`F`

is a constant type lambda.`Injective[F]`

witnesses that HKT`F`

is injective (not a constant type lambda 😃).`Covariant[F]`

witnesses that HKT`F`

is covariant (constant or strictly covariant).- Ditto other typeclasses / propositional types in
`variance`

package. - See my impromptu LC 2018 presentation for an overview.

## Quick Start

```
resolvers += Resolver.bintrayRepo("alexknvl", "maven")
libraryDependencies += "com.alexknvl" %% "leibniz" % "0.10.0"
```

## License

Code is provided under the MIT license available at https://opensource.org/licenses/MIT, as well as in the LICENSE file.