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