# 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 :smiley:).
• `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"``````

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

# Leibniz

## Leibniz equivalence and Liskov substitutability library for Scala.

### Leibniz Info

⭐ Stars 35
🔗 Source Code github.com
🕒 Last Update 8 months ago
🕒 Created 5 years ago
🐞 Open Issues 0
➗ Star-Issue Ratio Infinity
😎 Author alexknvl