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

{-# OPTIONS --cubical-compatible --safe #-}

module Function.Related.Propositional where

open import Level using (Level; _⊔_)
open import Relation.Binary
  using (Rel; REL; Sym; Reflexive; Trans; IsEquivalence; Setoid; IsPreorder; Preorder)
open import Function.Bundles
  using (Func; Inverse; _⇔_; _↣_; _↠_; _↪_; _⟶_; _↔_; mk⟶; Equivalence; Injection
        ; Surjection; RightInverse)
open import Function.Base using (id; flip; _∘_; _∘′_; _$_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as ≡
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  _∼[_]_

_∼[_]_ : 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
≡⇒ ≡.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 ≡.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  _↔⟨⟩_
  _↔⟨⟩_ : (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 = ≡.isEquivalence
    ; reflexive     = reflexive ∘
                      K-reflexive ∘
                      ≡.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 = ≡.isEquivalence
    ; reflexive     = λ x≡y {z} →
                        reflexive $
                        K-reflexive $
                        ≡.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 _ _)