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 Left

Injective Right

Injective (\{arg:0} => x ::: {arg:0})

Injective (\{arg:0} => {arg:0} ::: ys)

Injective This

Injective That

Injective (Both x)

Injective (\{arg:0} => Both {arg:0} y)

Injective ((x ::))

Injective (\x => x :: xs)

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 Both

Biinjective (::)

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:1507} -> {type_of_w:1506} -> {a:1508})) -> {auto 0 _ : Biinjective f} -> (0 _ : f x v = f y w) -> (x = y, v = w)

Totality: total
Visibility: public export