Control.Function

Definitions

interface Injective : (a -> b) -> Type

  An injective function maps distinct elements to distinct elements.

Parameters: f
Constructor: MkInjective
Methods:

injective : f x = f y -> x = y

Implementations:

Injective Just

Injective S

Injective FS

Injective finToNat

injective : Injective f => f x = f y -> x = y

Totality: total
Visibility: public export

inj : (0 f : (a -> b)) -> {auto 0 _ : Injective f} -> (0 _ : f x = f y) -> x = y

Totality: total
Visibility: public export

interface Biinjective : (a -> b -> c) -> Type

  An bi-injective function maps distinct elements to distinct elements in both arguments.
  This is more strict than injectivity on each of arguments.
  For instance, list appending is injective on both arguments but is not biinjective.

Parameters: f
Constructor: MkBiinjective
Methods:

biinjective : f x v = f y w -> (x = y, v = w)

Implementations:

Biinjective (::)

Biinjective MkPair

Biinjective (:<)

biinjective : Biinjective f => f x v = f y w -> (x = y, v = w)

Totality: total
Visibility: public export

biinj : (0 f : ({type_of_y:1506} -> {type_of_w:1505} -> {a:1507})) -> {auto 0 _ : Biinjective f} -> (0 _ : f x v = f y w) -> (x = y, v = w)

Totality: total
Visibility: public export