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

Visibility: public export

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

Visibility: public export