Control.Lens.Equality

A witness that (a ~ s, b ~ t).

Note: Composition with an Equality is index-preserving.

A Simple Equality.

When you see this as an argument to a function, it expects an Equality.

A Simple AnEquality.

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Extract a witness of type Equality.

Substituting types with Equality.

We can use Equality to do substitution into anything.

Equality is symmetric.

This is an adverb that can be used to modify many other Lens combinators to make them require simple lenses, simple traversals, simple prisms or simple isos as input.

Composition with this isomorphism is occasionally useful when your Lens, Control.Lens.Traversal.Traversal or Iso has a constraint on an unused argument to force that argument to agree with the type of a used argument and avoid ScopedTypeVariables or other ugliness.

Construct an Equality from explicit equality evidence.

A Simple version of equality

A version of substEq that provides explicit, rather than implicit, equality evidence.

The opposite of working overEquality is working underEquality.

Recover a "profunctor lens" form of equality. Reverses fromLeibniz.

Convert a "profunctor lens" form of equality to an equality. Reverses overEquality.

The type should be understood as

fromLeibniz :: (forall p. p a b -> p s t) -> Equality s t a b

Convert Leibniz equality to equality. Reverses mapEq in Simple cases.

The type should be understood as

fromLeibniz' :: (forall f. f s -> f a) -> Equality' s a

Provides witness that (s ~ a, b ~ t) holds.