Control.Lens.Equality

Definitions

data IsEquality : (k -> k' -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsEquality : IsEquality p

0 Equality : k -> k' -> k -> k' -> Type

  An `Equality s t a b` is a witness that `(s = a, t = b)` that can be used
  as an optic.
  
  The canonical `Equality` is `id : Equality a b a b`.
  
  An `Equality` can be coerced to any other optic.

Totality: total
Visibility: public export

0 Equality' : k -> k -> Type

  An `Equality' s a` is a witness that `s = a` that can be used as an optic.
  This is the `Simple` version of `Equality`.

Totality: total
Visibility: public export

runEq : Equality s t a b -> (s = a, t = b)

  Extract the two `Equal` values from an `Equality`.

Totality: total
Visibility: public export

runEq' : Equality s t a b -> s = a

  Extract an `Equal` value from an `Equality`.

Totality: total
Visibility: public export

congEq : {0 f : {type_of_a:10786} -> {k:10784}} -> {0 g : {type_of_b:10787} -> {k':10785}} -> Equality s t a b -> Equality (f s) (g t) (f a) (g b)

  `Equality` is a congruence.

Totality: total
Visibility: public export

symEq : Equality s t a b -> Equality b a t s

  Symmetry of an `Equality` optic.

Totality: total
Visibility: public export

substEq : {0 p : {type_of_a:10955} -> {type_of_b:10956} -> {type_of_a:10955} -> {type_of_b:10956} -> Type} -> Equality s t a b -> p a b a b -> p s t a b

Totality: total
Visibility: public export

simple : Equality' a a

  The trivial `Simple Equality`.
  Composing this optic with any other can force it to be a `Simple` optic.

Totality: total
Visibility: public export