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