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