|
264
|
1 module libbijection where
|
|
141
|
2
|
|
|
3 open import Level renaming ( zero to Zero ; suc to Suc )
|
|
|
4 open import Data.Nat
|
|
142
|
5 open import Data.Maybe
|
|
256
|
6 open import Data.List hiding ([_] ; sum )
|
|
141
|
7 open import Data.Nat.Properties
|
|
|
8 open import Relation.Nullary
|
|
|
9 open import Data.Empty
|
|
256
|
10 open import Data.Unit hiding ( _≤_ )
|
|
142
|
11 open import Relation.Binary.Core hiding (_⇔_)
|
|
141
|
12 open import Relation.Binary.Definitions
|
|
|
13 open import Relation.Binary.PropositionalEquality
|
|
264
|
14 open import Function.Inverse hiding (sym)
|
|
|
15 open import Function.Bijection renaming (Bijection to Bijection1)
|
|
|
16 open import Function.Equality hiding (cong)
|
|
141
|
17
|
|
|
18 open import logic
|
|
256
|
19 open import nat
|
|
141
|
20
|
|
264
|
21 -- record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
|
|
|
22 -- field
|
|
|
23 -- fun← : S → R
|
|
|
24 -- fun→ : R → S
|
|
|
25 -- fiso← : (x : R) → fun← ( fun→ x ) ≡ x
|
|
|
26 -- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x
|
|
|
27 --
|
|
|
28 -- injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
|
|
|
29 -- injection R S f = (x y : R) → f x ≡ f y → x ≡ y
|
|
164
|
30
|
|
141
|
31 open Bijection
|
|
|
32
|
|
264
|
33 b→injection1 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection S R (fun← b)
|
|
|
34 b→injection1 R S b x y eq = trans ( sym ( fiso→ b x ) ) (trans ( cong (λ k → fun→ b k ) eq ) ( fiso→ b y ))
|
|
|
35
|
|
263
|
36 --
|
|
|
37 -- injection as an uniquneness of bijection
|
|
|
38 --
|
|
164
|
39 b→injection0 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection R S (fun→ b)
|
|
|
40 b→injection0 R S b x y eq = begin
|
|
|
41 x
|
|
|
42 ≡⟨ sym ( fiso← b x ) ⟩
|
|
|
43 fun← b ( fun→ b x )
|
|
|
44 ≡⟨ cong (λ k → fun← b k ) eq ⟩
|
|
|
45 fun← b ( fun→ b y )
|
|
|
46 ≡⟨ fiso← b y ⟩
|
|
|
47 y
|
|
|
48 ∎ where open ≡-Reasoning
|
|
|
49
|
|
264
|
50 open import Relation.Binary using (Rel; Setoid; Symmetric; Total)
|
|
|
51 open import Function.Surjection
|
|
263
|
52
|
|
264
|
53 ≡-Setoid : {n : Level} (R : Set n) → Setoid n n
|
|
|
54 ≡-Setoid R = record {
|
|
|
55 Carrier = R
|
|
|
56 ; _≈_ = _≡_
|
|
|
57 ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }
|
|
|
58 }
|
|
256
|
59
|
|
|
60
|
|
264
|
61 libBijection : {n m : Level} (R : Set n) (S : Set m) → Bijection R S → Bijection1 (≡-Setoid R) (≡-Setoid S)
|
|
|
62 libBijection R S b = record {
|
|
|
63 to = record { _⟨$⟩_ = λ x → fun→ b x ; cong = λ i=j → cong (fun→ b) i=j }
|
|
|
64 ; bijective = record {
|
|
|
65 injective = λ {x} {y} eq → b→injection0 R S b x y eq
|
|
|
66 ; surjective = record { from = record { _⟨$⟩_ = λ x → fun← b x ; cong = λ i=j → cong (fun← b) i=j }
|
|
|
67 ; right-inverse-of = λ x → fiso→ b x }
|
|
|
68 }
|
|
|
69 }
|
|
256
|
70
|
|
264
|
71 fromBijection1 : {n m : Level} (R : Set n) (S : Set m) → Bijection1 (≡-Setoid R) (≡-Setoid S) → Bijection R S
|
|
|
72 fromBijection1 R S b = record {
|
|
|
73 fun← = Π._⟨$⟩_ (Surjective.from (Bijective.surjective (Bijection1.bijective b)))
|
|
|
74 ; fun→ = Π._⟨$⟩_ (Bijection1.to b)
|
|
|
75 ; fiso← = λ x → Bijective.injective (Bijection1.bijective b) (fb1 x)
|
|
|
76 ; fiso→ = Surjective.right-inverse-of (Bijective.surjective (Bijection1.bijective b))
|
|
|
77 } where
|
|
|
78 -- fun← b x ≡ fun← b y → x ≡ y
|
|
|
79 -- fun← (fun→ ( fun← x )) ≡ fun← x
|
|
|
80 -- fun→ ( fun← x ) ≡ x
|
|
|
81 fb1 : (x : R) → Π._⟨$⟩_ (Bijection1.to b) (Surjective.from (Bijective.surjective (Bijection1.bijective b)) ⟨$⟩ (Bijection1.to b ⟨$⟩ x)) ≡ Π._⟨$⟩_ (Bijection1.to b) x
|
|
|
82 fb1 x = begin
|
|
|
83 Π._⟨$⟩_ (Bijection1.to b) (Surjective.from (Bijective.surjective (Bijection1.bijective b)) ⟨$⟩ (Bijection1.to b ⟨$⟩ x))
|
|
|
84 ≡⟨ Surjective.right-inverse-of (Bijective.surjective (Bijection1.bijective b)) _ ⟩
|
|
|
85 Π._⟨$⟩_ (Bijection1.to b) x ∎ where open ≡-Reasoning
|
|
260
|
86
|
