```------------------------------------------------------------------------
-- 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 (Sym; Reflexive; Trans; IsEquivalence; Setoid; IsPreorder; Preorder)
open import Function.Bundles
open import Function.Base
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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 : Set a
B : Set b
C : Set c
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⟶ ∘ Bijection.to
⤖⇒ {k = reverseImplication} = mk⟶ ∘ Inverse.from ∘ ⤖⇒↔
⤖⇒ {k = equivalence}        = ⤖⇒⇔
⤖⇒ {k = injection}          = Bijection.injection
⤖⇒ {k = reverseInjection}   = Bijection.injection ∘ ↔⇒⤖ ∘ Symmetry.inverse ∘ ⤖⇒↔
⤖⇒ {k = leftInverse}        = Inverse.rightInverse ∘ ⤖⇒↔
⤖⇒ {k = surjection}         = Bijection.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}   = Bijection.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}        = Composition._⟶-∘_
K-trans {k = reverseImplication} = flip Composition._⟶-∘_
K-trans {k = equivalence}        = Composition._⇔-∘_
K-trans {k = injection}          = Composition._↣-∘_
K-trans {k = reverseInjection}   = flip Composition._↣-∘_
K-trans {k = leftInverse}        = Composition._↪-∘_
K-trans {k = surjection}         = Composition._↠-∘_
K-trans {k = bijection}          = 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.

module EquationalReasoning where

infix  3 _∎
infixr 2 _∼⟨_⟩_ _⤖⟨_⟩_ _↔⟨_⟩_ _↔⟨⟩_ _≡⟨_⟩_

_∼⟨_⟩_ : (A : Set a) → A ∼[ k ] B → B ∼[ k ] C → A ∼[ k ] C
_ ∼⟨ A↝B ⟩ B↝C = K-trans A↝B B↝C

-- Isomorphisms and bijections can be combined with any other kind of relatedness.

_⤖⟨_⟩_ : (A : Set a) → A ⤖ B → B ∼[ k ] C → A ∼[ k ] C
A ⤖⟨ A⤖B ⟩ B⇔C = A ∼⟨ ⤖⇒ A⤖B ⟩ B⇔C

_↔⟨_⟩_ : (A : Set a) → A ↔ B → B ∼[ k ] C → A ∼[ k ] C
A ↔⟨ A↔B ⟩ B⇔C = A ∼⟨ ⤖⇒ (↔⇒⤖ A↔B) ⟩ B⇔C

_↔⟨⟩_ : (A : Set a) → A ∼[ k ] B → A ∼[ k ] B
A ↔⟨⟩ A⇔B = A⇔B

_≡⟨_⟩_ : (A : Set a) → A ≡ B → B ∼[ k ] C → A ∼[ k ] C
A ≡⟨ A≡B ⟩ B⇔C = A ∼⟨ ≡⇒ A≡B ⟩ B⇔C

_∎ : (A : Set a) → A ∼[ k ] A
A ∎ = K-refl

------------------------------------------------------------------------
-- 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 _ _)
```