blob: 4f7ea4307ad5d3cc5af771d1ee665e0ac89796da (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
{-# OPTIONS --without-K --safe #-}
module Data.Fin.Preimage where
open import Data.Nat.Base using (ℕ)
open import Data.Fin.Base using (Fin)
open import Function.Base using (∣_⟩-_; _∘_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
open import Data.Subset.Functional using (Subset; foldl; _∪_; ⊥; ⁅_⁆)
private
variable A B C : ℕ
preimage : (Fin A → Fin B) → Subset B → Subset A
preimage f Y = Y ∘ f
⋃ : Subset A → (Fin A → Subset B) → Subset B
⋃ S f = foldl (∣ _∪_ ⟩- f) ⊥ S
image : (Fin A → Fin B) → Subset A → Subset B
image f X = ⋃ X (⁅_⁆ ∘ f)
preimage-cong₁
: {f g : Fin A → Fin B}
→ f ≗ g
→ (S : Subset B)
→ preimage f S ≗ preimage g S
preimage-cong₁ f≗g S x = ≡.cong S (f≗g x)
preimage-cong₂
: (f : Fin A → Fin B)
{S₁ S₂ : Subset B}
→ S₁ ≗ S₂
→ preimage f S₁ ≗ preimage f S₂
preimage-cong₂ f S₁≗S₂ = S₁≗S₂ ∘ f
preimage-∘
: (f : Fin A → Fin B)
(g : Fin B → Fin C)
(z : Fin C)
→ preimage (g ∘ f) ⁅ z ⁆ ≗ preimage f (preimage g ⁅ z ⁆)
preimage-∘ f g S x = ≡.refl
preimage-⊥
: {n m : ℕ}
(f : Fin n → Fin m)
→ preimage f ⊥ ≗ ⊥
preimage-⊥ f x = ≡.refl
|
