------------------------------------------------------------------------ -- The Agda standard library -- -- Relatedness for the function hierarchy ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Related.Propositional where open import Level open import Relation.Binary using (Rel; REL; Sym; Reflexive; Trans; IsEquivalence; Setoid; IsPreorder; Preorder) open import Function.Bundles open import Function.Base open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P open import Relation.Binary.Reasoning.Syntax open import Function.Properties.Surjection using (↠⇒↪; ↠⇒⇔) open import Function.Properties.RightInverse using (↪⇒↠) open import Function.Properties.Bijection using (⤖⇒↔; ⤖⇒⇔) open import Function.Properties.Inverse using (↔⇒⤖; ↔⇒⇔; ↔⇒↣; ↔⇒↠) import Function.Construct.Symmetry as Symmetry import Function.Construct.Identity as Identity import Function.Construct.Composition as Composition ------------------------------------------------------------------------ -- Relatedness -- There are several kinds of "relatedness". -- The idea to include kinds other than equivalence and bijection came -- from Simon Thompson and Bengt Nordström. /NAD data Kind : Set where implication : Kind reverseImplication : Kind equivalence : Kind injection : Kind reverseInjection : Kind leftInverse : Kind surjection : Kind bijection : Kind private variable a b c p : Level A B C : Set a k : Kind -- Interpretation of the codes above. The code "bijection" is -- interpreted as Inverse rather than Bijection; the two types are -- equivalent. infix 4 _∼[_]_ _∼[_]_ : Set a → Kind → Set b → Set _ A ∼[ implication ] B = A ⟶ B A ∼[ reverseImplication ] B = B ⟶ A A ∼[ equivalence ] B = A ⇔ B A ∼[ injection ] B = A ↣ B A ∼[ reverseInjection ] B = B ↣ A A ∼[ leftInverse ] B = A ↪ B A ∼[ surjection ] B = A ↠ B A ∼[ bijection ] B = A ↔ B -- A non-infix synonym. Related : Kind → Set a → Set b → Set _ Related k A B = A ∼[ k ] B -- The bijective equality implies any kind of relatedness. ↔⇒ : A ∼[ bijection ] B → A ∼[ k ] B ↔⇒ {k = implication} = mk⟶ ∘ Inverse.to ↔⇒ {k = reverseImplication} = mk⟶ ∘ Inverse.from ↔⇒ {k = equivalence} = ↔⇒⇔ ↔⇒ {k = injection} = ↔⇒↣ ↔⇒ {k = reverseInjection} = ↔⇒↣ ∘ Symmetry.inverse ↔⇒ {k = leftInverse} = Inverse.rightInverse ↔⇒ {k = surjection} = ↔⇒↠ ↔⇒ {k = bijection} = id -- Propositional equality also implies any kind of relatedness. ≡⇒ : A ≡ B → A ∼[ k ] B ≡⇒ P.refl = ↔⇒ (Identity.↔-id _) ------------------------------------------------------------------------ -- Special kinds of kinds -- Kinds whose interpretation is symmetric. data SymmetricKind : Set where equivalence : SymmetricKind bijection : SymmetricKind -- Forgetful map. ⌊_⌋ : SymmetricKind → Kind ⌊ equivalence ⌋ = equivalence ⌊ bijection ⌋ = bijection -- The proof of symmetry can be found below. -- Kinds whose interpretation include a function which "goes in the -- forward direction". data ForwardKind : Set where implication : ForwardKind equivalence : ForwardKind injection : ForwardKind leftInverse : ForwardKind surjection : ForwardKind bijection : ForwardKind -- Forgetful map. ⌊_⌋→ : ForwardKind → Kind ⌊ implication ⌋→ = implication ⌊ equivalence ⌋→ = equivalence ⌊ injection ⌋→ = injection ⌊ leftInverse ⌋→ = leftInverse ⌊ surjection ⌋→ = surjection ⌊ bijection ⌋→ = bijection -- The function. ⇒→ : ∀ {k} → A ∼[ ⌊ k ⌋→ ] B → A → B ⇒→ {k = implication} = Func.to ⇒→ {k = equivalence} = Equivalence.to ⇒→ {k = injection} = Injection.to ⇒→ {k = leftInverse} = RightInverse.to ⇒→ {k = surjection} = Surjection.to ⇒→ {k = bijection} = Inverse.to -- Kinds whose interpretation include a function which "goes backwards". data BackwardKind : Set where reverseImplication : BackwardKind equivalence : BackwardKind reverseInjection : BackwardKind leftInverse : BackwardKind surjection : BackwardKind bijection : BackwardKind -- Forgetful map. ⌊_⌋← : BackwardKind → Kind ⌊ reverseImplication ⌋← = reverseImplication ⌊ equivalence ⌋← = equivalence ⌊ reverseInjection ⌋← = reverseInjection ⌊ leftInverse ⌋← = leftInverse ⌊ surjection ⌋← = surjection ⌊ bijection ⌋← = bijection -- The function. ⇒← : ∀ {k} → A ∼[ ⌊ k ⌋← ] B → B → A ⇒← {k = reverseImplication} = Func.to ⇒← {k = equivalence} = Equivalence.from ⇒← {k = reverseInjection} = Injection.to ⇒← {k = leftInverse} = RightInverse.from ⇒← {k = surjection} = RightInverse.to ∘ ↠⇒↪ ⇒← {k = bijection} = Inverse.from -- Kinds whose interpretation include functions going in both -- directions. data EquivalenceKind : Set where equivalence : EquivalenceKind leftInverse : EquivalenceKind surjection : EquivalenceKind bijection : EquivalenceKind -- Forgetful map. ⌊_⌋⇔ : EquivalenceKind → Kind ⌊ equivalence ⌋⇔ = equivalence ⌊ leftInverse ⌋⇔ = leftInverse ⌊ surjection ⌋⇔ = surjection ⌊ bijection ⌋⇔ = bijection -- The functions. ⇒⇔ : ∀ {k} → A ∼[ ⌊ k ⌋⇔ ] B → A ∼[ equivalence ] B ⇒⇔ {k = equivalence} = id ⇒⇔ {k = leftInverse} = RightInverse.equivalence ⇒⇔ {k = surjection} = ↠⇒⇔ ⇒⇔ {k = bijection} = ↔⇒⇔ -- Conversions between special kinds. ⇔⌊_⌋ : SymmetricKind → EquivalenceKind ⇔⌊ equivalence ⌋ = equivalence ⇔⌊ bijection ⌋ = bijection →⌊_⌋ : EquivalenceKind → ForwardKind →⌊ equivalence ⌋ = equivalence →⌊ leftInverse ⌋ = leftInverse →⌊ surjection ⌋ = surjection →⌊ bijection ⌋ = bijection ←⌊_⌋ : EquivalenceKind → BackwardKind ←⌊ equivalence ⌋ = equivalence ←⌊ leftInverse ⌋ = leftInverse ←⌊ surjection ⌋ = surjection ←⌊ bijection ⌋ = bijection ------------------------------------------------------------------------ -- Opposites -- For every kind there is an opposite kind. _op : Kind → Kind implication op = reverseImplication reverseImplication op = implication equivalence op = equivalence injection op = reverseInjection reverseInjection op = injection leftInverse op = surjection surjection op = leftInverse bijection op = bijection -- For every morphism there is a corresponding reverse morphism of the -- opposite kind. reverse : A ∼[ k ] B → B ∼[ k op ] A reverse {k = implication} = id reverse {k = reverseImplication} = id reverse {k = equivalence} = Symmetry.⇔-sym reverse {k = injection} = id reverse {k = reverseInjection} = id reverse {k = leftInverse} = ↪⇒↠ reverse {k = surjection} = ↠⇒↪ reverse {k = bijection} = Symmetry.↔-sym ------------------------------------------------------------------------ -- For a fixed universe level every kind is a preorder and each -- symmetric kind is an equivalence K-refl : Reflexive (Related {a} k) K-refl {k = implication} = Identity.⟶-id _ K-refl {k = reverseImplication} = Identity.⟶-id _ K-refl {k = equivalence} = Identity.⇔-id _ K-refl {k = injection} = Identity.↣-id _ K-refl {k = reverseInjection} = Identity.↣-id _ K-refl {k = leftInverse} = Identity.↪-id _ K-refl {k = surjection} = Identity.↠-id _ K-refl {k = bijection} = Identity.↔-id _ K-reflexive : _≡_ Relation.Binary.⇒ Related {a} k K-reflexive P.refl = K-refl K-trans : Trans (Related {a} {b} k) (Related {b} {c} k) (Related {a} {c} k) K-trans {k = implication} = flip Composition._⟶-∘_ K-trans {k = reverseImplication} = Composition._⟶-∘_ K-trans {k = equivalence} = flip Composition._⇔-∘_ K-trans {k = injection} = flip Composition._↣-∘_ K-trans {k = reverseInjection} = Composition._↣-∘_ K-trans {k = leftInverse} = flip Composition._↪-∘_ K-trans {k = surjection} = flip Composition._↠-∘_ K-trans {k = bijection} = flip Composition._↔-∘_ SK-sym : ∀ {k} → Sym (Related {a} {b} ⌊ k ⌋) (Related {b} {a} ⌊ k ⌋) SK-sym {k = equivalence} = reverse SK-sym {k = bijection} = reverse SK-isEquivalence : ∀ k → IsEquivalence {ℓ = a} (Related ⌊ k ⌋) SK-isEquivalence k = record { refl = K-refl ; sym = SK-sym ; trans = K-trans } SK-setoid : SymmetricKind → (ℓ : Level) → Setoid _ _ SK-setoid k ℓ = record { isEquivalence = SK-isEquivalence {ℓ} k } K-isPreorder : ∀ k → IsPreorder {ℓ = a} _↔_ (Related k) K-isPreorder k = record { isEquivalence = SK-isEquivalence bijection ; reflexive = ↔⇒ ; trans = K-trans } K-preorder : Kind → (ℓ : Level) → Preorder _ ℓ _ K-preorder k ℓ = record { isPreorder = K-isPreorder k } ------------------------------------------------------------------------ -- Equational reasoning -- Equational reasoning for related things. Note that we don't use -- the `Relation.Binary.Reasoning.Syntax` for this as this relation -- is heterogeneous. module EquationalReasoning {k : Kind} where -- Combinators with one heterogeneous relation module _ {a b : Level} where open begin-syntax (Related {a} {b} k) id public open ≡-noncomputing-syntax (Related {a} {b} k) public -- Combinators with two heterogeneous relations module _ {a b c : Level} where private rel1 = Related {b} {c} k rel2 = Related {a} {c} k open ∼-syntax rel1 rel2 K-trans public open ⤖-syntax rel1 rel2 (K-trans ∘′ ↔⇒ ∘′ ⤖⇒↔) Symmetry.⤖-sym public open ↔-syntax rel1 rel2 (K-trans ∘′ ↔⇒) Symmetry.↔-sym public -- Combinators with homogeneous relations module _ {a : Level} where open end-syntax (Related {a} k) K-refl public infixr 2 _↔⟨⟩_ _↔⟨⟩_ : (A : Set a) → A ∼[ k ] B → A ∼[ k ] B A ↔⟨⟩ A⇔B = A⇔B {-# WARNING_ON_USAGE _↔⟨⟩_ "Warning: _↔⟨⟩_ was deprecated in v2.0. Please use _≡⟨⟩_ instead. " #-} ------------------------------------------------------------------------ -- Every unary relation induces a preorder and, for symmetric kinds, -- an equivalence. (No claim is made that these relations are unique.) InducedRelation₁ : Kind → (P : A → Set p) → A → A → Set _ InducedRelation₁ k P = λ x y → P x ∼[ k ] P y InducedPreorder₁ : Kind → (P : A → Set p) → Preorder _ _ _ InducedPreorder₁ k P = record { _≈_ = _≡_ ; _≲_ = InducedRelation₁ k P ; isPreorder = record { isEquivalence = P.isEquivalence ; reflexive = reflexive ∘ K-reflexive ∘ P.cong P ; trans = K-trans } } where open Preorder (K-preorder _ _) InducedEquivalence₁ : SymmetricKind → (P : A → Set p) → Setoid _ _ InducedEquivalence₁ k P = record { _≈_ = InducedRelation₁ ⌊ k ⌋ P ; isEquivalence = record { refl = K-refl ; sym = SK-sym ; trans = K-trans } } ------------------------------------------------------------------------ -- Every binary relation induces a preorder and, for symmetric kinds, -- an equivalence. (No claim is made that these relations are unique.) InducedRelation₂ : Kind → ∀ {s} → (A → B → Set s) → B → B → Set _ InducedRelation₂ k _S_ = λ x y → ∀ {z} → (z S x) ∼[ k ] (z S y) InducedPreorder₂ : Kind → ∀ {s} → (A → B → Set s) → Preorder _ _ _ InducedPreorder₂ k _S_ = record { _≈_ = _≡_ ; _≲_ = InducedRelation₂ k _S_ ; isPreorder = record { isEquivalence = P.isEquivalence ; reflexive = λ x≡y {z} → reflexive $ K-reflexive $ P.cong (_S_ z) x≡y ; trans = λ i↝j j↝k → K-trans i↝j j↝k } } where open Preorder (K-preorder _ _) InducedEquivalence₂ : SymmetricKind → ∀ {s} → (A → B → Set s) → Setoid _ _ InducedEquivalence₂ k _S_ = record { _≈_ = InducedRelation₂ ⌊ k ⌋ _S_ ; isEquivalence = record { refl = refl ; sym = λ i↝j → sym i↝j ; trans = λ i↝j j↝k → trans i↝j j↝k } } where open Setoid (SK-setoid _ _)