-
Notifications
You must be signed in to change notification settings - Fork 246
/
Copy pathConsequences.agda
114 lines (93 loc) · 4.72 KB
/
Consequences.agda
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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
------------------------------------------------------------------------
-- The Agda standard library
--
-- Relationships between properties of functions. See
-- `Function.Consequences.Propositional` for specialisations to
-- propositional equality.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Consequences where
open import Data.Product.Base as Prod
open import Function.Definitions
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
open import Relation.Nullary.Negation.Core using (¬_; contraposition)
private
variable
a b ℓ₁ ℓ₂ : Level
A B : Set a
≈₁ ≈₂ : Rel A ℓ₁
f f⁻¹ : A → B
------------------------------------------------------------------------
-- Injective
contraInjective : ∀ (≈₂ : Rel B ℓ₂) → Injective ≈₁ ≈₂ f →
∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))
contraInjective _ inj p = contraposition inj p
------------------------------------------------------------------------
-- Inverseˡ
inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) →
Inverseˡ ≈₁ ≈₂ f f⁻¹ →
Surjective ≈₁ ≈₂ f
inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ)
------------------------------------------------------------------------
-- Inverseʳ
inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f →
Reflexive ≈₂ →
Symmetric ≈₁ →
Transitive ≈₁ →
Inverseʳ ≈₁ ≈₂ f f⁻¹ →
Injective ≈₁ ≈₂ f
inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy =
trans (sym (invʳ refl)) (invʳ fx≈fy)
------------------------------------------------------------------------
-- Inverseᵇ
inverseᵇ⇒bijective : ∀ (≈₂ : Rel B ℓ₂) →
Reflexive ≈₂ →
Symmetric ≈₁ →
Transitive ≈₁ →
Inverseᵇ ≈₁ ≈₂ f f⁻¹ →
Bijective ≈₁ ≈₂ f
inverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) =
(inverseʳ⇒injective ≈₂ f refl sym trans invʳ , inverseˡ⇒surjective ≈₂ invˡ)
------------------------------------------------------------------------
-- StrictlySurjective
surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) →
Reflexive ≈₁ →
Surjective ≈₁ ≈₂ f →
StrictlySurjective ≈₂ f
surjective⇒strictlySurjective _ refl surj x =
Prod.map₂ (λ v → v refl) (surj x)
strictlySurjective⇒surjective : Transitive ≈₂ →
Congruent ≈₁ ≈₂ f →
StrictlySurjective ≈₂ f →
Surjective ≈₁ ≈₂ f
strictlySurjective⇒surjective trans cong surj x =
Prod.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x)
------------------------------------------------------------------------
-- StrictlyInverseˡ
inverseˡ⇒strictlyInverseˡ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
Reflexive ≈₁ →
Inverseˡ ≈₁ ≈₂ f f⁻¹ →
StrictlyInverseˡ ≈₂ f f⁻¹
inverseˡ⇒strictlyInverseˡ _ _ refl sinv x = sinv refl
strictlyInverseˡ⇒inverseˡ : Transitive ≈₂ →
Congruent ≈₁ ≈₂ f →
StrictlyInverseˡ ≈₂ f f⁻¹ →
Inverseˡ ≈₁ ≈₂ f f⁻¹
strictlyInverseˡ⇒inverseˡ trans cong sinv {x} y≈f⁻¹x =
trans (cong y≈f⁻¹x) (sinv x)
------------------------------------------------------------------------
-- StrictlyInverseʳ
inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
Reflexive ≈₂ →
Inverseʳ ≈₁ ≈₂ f f⁻¹ →
StrictlyInverseʳ ≈₁ f f⁻¹
inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl
strictlyInverseʳ⇒inverseʳ : Transitive ≈₁ →
Congruent ≈₂ ≈₁ f⁻¹ →
StrictlyInverseʳ ≈₁ f f⁻¹ →
Inverseʳ ≈₁ ≈₂ f f⁻¹
strictlyInverseʳ⇒inverseʳ trans cong sinv {x} y≈f⁻¹x =
trans (cong y≈f⁻¹x) (sinv x)