0 | module Control.Function
 1 |
 2 | %default total
 3 |
 4 | ||| An injective function maps distinct elements to distinct elements.
 5 | public export
 6 | interface Injective (f : a -> b) | f where
 7 |   constructor MkInjective
 8 |   injective : {x, y : a} -> f x = f y -> x = y
 9 |
10 | public export
11 | inj : (0 f : a -> b) -> {auto 0 _ : Injective f} -> {0 x, y : a} -> (0 _ : f x = f y) -> x = y
12 | inj _ eq = irrelevantEq (injective eq)
13 |
14 | ----------------------------------------
15 |
16 | ||| The composition of injective functions is injective.
17 | public export
18 | [ComposeInjective] {f : a -> b} -> {g : b -> c} ->
19 |   (Injective f, Injective g) => Injective (g . f) where
20 |     injective = injective . injective
21 |
22 | ||| If (g . f) is injective, so is f.
23 | public export
24 | [InjFromComp] {f : a -> b} -> {g : b -> c} ->
25 |   Injective (g . f) => Injective f where
26 |     injective prf = injective {f = (g . f)} $ cong g prf
27 |
28 | public export
29 | [IdInjective] Injective Prelude.id where
30 |   injective = id
31 |
32 | ----------------------------------------
33 |
34 | ||| An bi-injective function maps distinct elements to distinct elements in both arguments.
35 | ||| This is more strict than injectivity on each of arguments.
36 | ||| For instance, list appending is injective on both arguments but is not biinjective.
37 | public export
38 | interface Biinjective (0 f : a -> b -> c) | f where
39 |   constructor MkBiinjective
40 |   biinjective : {x, y : a} -> {v, w : b} -> f x v = f y w -> (x = y, v = w)
41 |
42 | public export
43 | biinj : (0 f : _) -> (0 _ : Biinjective f) => (0 _ : f x v = f y w) -> (x = y, v = w)
44 | biinj _ eq = let 0 bii = biinjective eq in (irrelevantEq $ fst bii, irrelevantEq $ snd bii)
45 |
46 | public export
47 | [ComposeBiinjective] {f : a -> b -> c} -> {g : c -> d} ->
48 |   Biinjective f => Injective g => Biinjective (g .: f) where
49 |     biinjective = biinjective . injective
50 |
51 | ||| If (g .: f) is biinjective, so is f.
52 | public export
53 | [BiinjFromComp] {f : a -> b -> c} -> {g : c -> d} ->
54 |   Biinjective (g .: f) => Biinjective f where
55 |     biinjective prf = biinjective {f = (g .: f)} $ cong g prf
56 |
57 | public export
58 | [FlipBiinjective] {f : a -> b -> c} ->
59 |   Biinjective f => Biinjective (flip f) where
60 |     biinjective = swap . biinjective
61 |
62 | public export
63 | [FromBiinjectiveL] {f : a -> b -> c} -> {x : a} ->
64 |   Biinjective f => Injective (f x) where
65 |     injective = snd . biinjective
66 |
67 | public export
68 | [FromBiinjectiveR] {f : a -> b -> c} -> {y : b} ->
69 |   Biinjective f => Injective (`f` y) where
70 |     injective = fst . biinjective
71 |
72 | export
73 | Biinjective MkPair where
74 |   biinjective Refl = (Refl, Refl)
75 |