------------------------------------------------------------------------
-- The Agda standard library
--
-- Relatedness for the function hierarchy
------------------------------------------------------------------------

{-# OPTIONS --without-K --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  _∼[_]_

_∼[_]_ : 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   _∎
  infixr  _∼⟨_⟩_ _⤖⟨_⟩_ _↔⟨_⟩_ _↔⟨⟩_ _≡⟨_⟩_

  _∼⟨_⟩_ : (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 _ _)