------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe which includes several kinds of "relatedness" for sets,
-- such as equivalences, surjections and bijections
------------------------------------------------------------------------

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

module Function.Related where

open import Level
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq      using (Equivalence)
open import Function.Injection   as Inj     using (Injection; _↣_)
open import Function.Inverse     as Inv     using (Inverse; _↔_)
open import Function.LeftInverse as LeftInv using (LeftInverse)
open import Function.Surjection  as Surj    using (Surjection)
open import Function.Consequences.Propositional
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Bundles using (Setoid; Preorder)
open import Relation.Binary.Structures using (IsEquivalence; IsPreorder)
open import Relation.Binary.Definitions using (Reflexive; Trans; Sym)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as P
open import Data.Product.Base using (_,_; proj₁; proj₂; <_,_>)

import Function.Related.Propositional as R
import Function.Bundles as B

private
  variable
    ℓ₁ ℓ₂ : Level
    A : Set ℓ₁
    B : Set ℓ₂

------------------------------------------------------------------------
-- Re-export core concepts from non-deprecated Related code

open R public using
  ( Kind
  ; implication
  ; equivalence
  ; injection
  ; surjection
  ; bijection
  ) renaming
  ( reverseImplication to reverse-implication
  ; reverseInjection   to reverse-injection
  ; leftInverse        to left-inverse
  )

------------------------------------------------------------------------
-- Wrapper types

-- Synonyms which are used to make _∼[_]_ below "constructor-headed"
-- (which implies that Agda can deduce the universe code from an
-- expression matching any of the right-hand sides).

infix 3 _←_ _↢_

record _←_ {a b} (A : Set a) (B : Set b) : Set (a  b) where
  constructor lam
  field app-← : B  A

open _←_ public

record _↢_ {a b} (A : Set a) (B : Set b) : Set (a  b) where
  constructor lam
  field app-↢ : B  A

open _↢_ public

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

infix 4 _∼[_]_

_∼[_]_ :  {ℓ₁ ℓ₂}  Set ℓ₁  Kind  Set ℓ₂  Set _
A ∼[ implication         ] B = A  B
A ∼[ reverse-implication ] B = A  B
A ∼[ equivalence         ] B = Equivalence (P.setoid A) (P.setoid B)
A ∼[ injection           ] B = Injection   (P.setoid A) (P.setoid B)
A ∼[ reverse-injection   ] B = A  B
A ∼[ left-inverse        ] B = LeftInverse (P.setoid A) (P.setoid B)
A ∼[ surjection          ] B = Surjection  (P.setoid A) (P.setoid B)
A ∼[ bijection           ] B = Inverse     (P.setoid A) (P.setoid B)

toRelated : {K : Kind}  A R.∼[ K ] B  A ∼[ K ] B
toRelated {K = implication}         rel = B.Func.to rel
toRelated {K = reverse-implication} rel = lam (B.Func.to rel)
toRelated {K = equivalence}         rel = Eq.equivalence (B.Equivalence.to rel) (B.Equivalence.from rel)
toRelated {K = injection}           rel = Inj.injection (B.Injection.to rel) (B.Injection.injective rel)
toRelated {K = reverse-injection}   rel = lam (Inj.injection (B.Injection.to rel) (B.Injection.injective rel))
toRelated {K = left-inverse}        rel = LeftInv.leftInverse to from strictlyInverseʳ where open B.RightInverse rel
toRelated {K = surjection}          rel = Surj.surjection to (proj₁  strictlySurjective) (proj₂  strictlySurjective)
  where open B.Surjection rel
toRelated {K = bijection}           rel =
  Inv.inverse to (proj₁  strictlySurjective) (injective  proj₂  strictlySurjective  to) (proj₂  strictlySurjective)
  where open B.Bijection rel

fromRelated : {K : Kind}  A ∼[ K ] B  A R.∼[ K ] B
fromRelated {K = implication}         rel = B.mk⟶ rel
fromRelated {K = reverse-implication} rel = B.mk⟶ (app-← rel)
fromRelated {K = equivalence}         record { to = to ; from = from } = B.mk⇔ (to ⟨$⟩_) (from ⟨$⟩_)
fromRelated {K = injection}           rel = B.mk↣ (Inj.Injection.injective rel)
fromRelated {K = reverse-injection}   (lam app-↢) = B.mk↣ (Inj.Injection.injective app-↢)
fromRelated {K = left-inverse}        record { to = to ; from = from ; left-inverse-of = left-inverse-of } =
  B.mk↪ {to = to ⟨$⟩_} {from = from ⟨$⟩_} (strictlyInverseʳ⇒inverseʳ (to ⟨$⟩_) left-inverse-of)
fromRelated {K = surjection}          record { to = to ; surjective = surjective } with surjective
... | record { from = from ; right-inverse-of = right-inverse-of } =
  B.mk↠ {to = to ⟨$⟩_} < from ⟨$⟩_ ,  { x P.refl  right-inverse-of x }) >
fromRelated {K = bijection}           record { to = to ; from = from ; inverse-of = inverse-of } with inverse-of
... | record { left-inverse-of = left-inverse-of ; right-inverse-of = right-inverse-of } = B.mk⤖
  ((λ {x y} h  P.subst₂ P._≡_ (left-inverse-of x) (left-inverse-of y) (P.cong (from ⟨$⟩_) h)) ,
  < from ⟨$⟩_ ,  { x P.refl  right-inverse-of x }) >)

-- A non-infix synonym.

Related : Kind   {ℓ₁ ℓ₂}  Set ℓ₁  Set ℓ₂  Set _
Related k A B = A ∼[ k ] B

-- The bijective equality implies any kind of relatedness.

↔⇒ :  {k x y} {X : Set x} {Y : Set y} 
     X ∼[ bijection ] Y  X ∼[ k ] Y
↔⇒ {implication}         = _⟨$⟩_  Inverse.to
↔⇒ {reverse-implication} = lam ∘′ _⟨$⟩_  Inverse.from
↔⇒ {equivalence}         = Inverse.equivalence
↔⇒ {injection}           = Inverse.injection
↔⇒ {reverse-injection}   = lam ∘′ Inverse.injection  Inv.sym
↔⇒ {left-inverse}        = Inverse.left-inverse
↔⇒ {surjection}          = Inverse.surjection
↔⇒ {bijection}           = id

-- Actual equality also implies any kind of relatedness.

≡⇒ :  {k } {X Y : Set }  X  Y  X ∼[ k ] Y
≡⇒ P.refl = ↔⇒ Inv.id

------------------------------------------------------------------------
-- Special kinds of kinds

-- Kinds whose interpretation is symmetric.

data Symmetric-kind : Set where
  equivalence : Symmetric-kind
  bijection   : Symmetric-kind

-- Forgetful map.

⌊_⌋ : Symmetric-kind  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 Forward-kind : Set where
  implication  : Forward-kind
  equivalence  : Forward-kind
  injection    : Forward-kind
  left-inverse : Forward-kind
  surjection   : Forward-kind
  bijection    : Forward-kind

-- Forgetful map.

⌊_⌋→ : Forward-kind  Kind
 implication  ⌋→ = implication
 equivalence  ⌋→ = equivalence
 injection    ⌋→ = injection
 left-inverse ⌋→ = left-inverse
 surjection   ⌋→ = surjection
 bijection    ⌋→ = bijection

-- The function.

⇒→ :  {k x y} {X : Set x} {Y : Set y}  X ∼[  k ⌋→ ] Y  X  Y
⇒→ {implication}  = id
⇒→ {equivalence}  = _⟨$⟩_  Equivalence.to
⇒→ {injection}    = _⟨$⟩_  Injection.to
⇒→ {left-inverse} = _⟨$⟩_  LeftInverse.to
⇒→ {surjection}   = _⟨$⟩_  Surjection.to
⇒→ {bijection}    = _⟨$⟩_  Inverse.to

-- Kinds whose interpretation include a function which "goes backwards".

data Backward-kind : Set where
  reverse-implication : Backward-kind
  equivalence         : Backward-kind
  reverse-injection   : Backward-kind
  left-inverse        : Backward-kind
  surjection          : Backward-kind
  bijection           : Backward-kind

-- Forgetful map.

⌊_⌋← : Backward-kind  Kind
 reverse-implication ⌋← = reverse-implication
 equivalence         ⌋← = equivalence
 reverse-injection   ⌋← = reverse-injection
 left-inverse        ⌋← = left-inverse
 surjection          ⌋← = surjection
 bijection           ⌋← = bijection

-- The function.

⇒← :  {k x y} {X : Set x} {Y : Set y}  X ∼[  k ⌋← ] Y  Y  X
⇒← {reverse-implication} = app-←
⇒← {equivalence}         = _⟨$⟩_  Equivalence.from
⇒← {reverse-injection}   = _⟨$⟩_  Injection.to  app-↢
⇒← {left-inverse}        = _⟨$⟩_  LeftInverse.from
⇒← {surjection}          = _⟨$⟩_  Surjection.from
⇒← {bijection}           = _⟨$⟩_  Inverse.from

-- Kinds whose interpretation include functions going in both
-- directions.

data Equivalence-kind : Set where
    equivalence  : Equivalence-kind
    left-inverse : Equivalence-kind
    surjection   : Equivalence-kind
    bijection    : Equivalence-kind

-- Forgetful map.

⌊_⌋⇔ : Equivalence-kind  Kind
 equivalence  ⌋⇔ = equivalence
 left-inverse ⌋⇔ = left-inverse
 surjection   ⌋⇔ = surjection
 bijection    ⌋⇔ = bijection

-- The functions.

⇒⇔ :  {k x y} {X : Set x} {Y : Set y} 
     X ∼[  k ⌋⇔ ] Y  X ∼[ equivalence ] Y
⇒⇔ {equivalence}  = id
⇒⇔ {left-inverse} = LeftInverse.equivalence
⇒⇔ {surjection}   = Surjection.equivalence
⇒⇔ {bijection}    = Inverse.equivalence

-- Conversions between special kinds.

⇔⌊_⌋ : Symmetric-kind  Equivalence-kind
⇔⌊ equivalence  = equivalence
⇔⌊ bijection    = bijection

→⌊_⌋ : Equivalence-kind  Forward-kind
→⌊ equivalence   = equivalence
→⌊ left-inverse  = left-inverse
→⌊ surjection    = surjection
→⌊ bijection     = bijection

←⌊_⌋ : Equivalence-kind  Backward-kind
←⌊ equivalence   = equivalence
←⌊ left-inverse  = left-inverse
←⌊ surjection    = surjection
←⌊ bijection     = bijection

------------------------------------------------------------------------
-- Opposites

-- For every kind there is an opposite kind.

_op : Kind  Kind
implication         op = reverse-implication
reverse-implication op = implication
equivalence         op = equivalence
injection           op = reverse-injection
reverse-injection   op = injection
left-inverse        op = surjection
surjection          op = left-inverse
bijection           op = bijection

-- For every morphism there is a corresponding reverse morphism of the
-- opposite kind.

reverse :  {k a b} {A : Set a} {B : Set b} 
          A ∼[ k ] B  B ∼[ k op ] A
reverse {implication}         = lam
reverse {reverse-implication} = app-←
reverse {equivalence}         = Eq.sym
reverse {injection}           = lam
reverse {reverse-injection}   = app-↢
reverse {left-inverse}        = Surj.fromRightInverse
reverse {surjection}          = Surjection.right-inverse
reverse {bijection}           = Inv.sym

------------------------------------------------------------------------
-- For a fixed universe level every kind is a preorder and each
-- symmetric kind is an equivalence

K-refl :  {k }  Reflexive (Related k {})
K-refl {implication}         = id
K-refl {reverse-implication} = lam id
K-refl {equivalence}         = Eq.id
K-refl {injection}           = Inj.id
K-refl {reverse-injection}   = lam Inj.id
K-refl {left-inverse}        = LeftInv.id
K-refl {surjection}          = Surj.id
K-refl {bijection}           = Inv.id

K-reflexive :  {k }  _≡_  Related k {}
K-reflexive P.refl = K-refl

K-trans :  {k ℓ₁ ℓ₂ ℓ₃}  Trans (Related k {ℓ₁} {ℓ₂})
                                (Related k {ℓ₂} {ℓ₃})
                                (Related k {ℓ₁} {ℓ₃})
K-trans {implication}         = flip _∘′_
K-trans {reverse-implication} = λ f g  lam (app-← f  app-← g)
K-trans {equivalence}         = flip Eq._∘_
K-trans {injection}           = flip Inj._∘_
K-trans {reverse-injection}   = λ f g  lam (Inj._∘_ (app-↢ f) (app-↢ g))
K-trans {left-inverse}        = flip LeftInv._∘_
K-trans {surjection}          = flip Surj._∘_
K-trans {bijection}           = flip Inv._∘_

SK-sym :  {k ℓ₁ ℓ₂}  Sym (Related  k  {ℓ₁} {ℓ₂})
                          (Related  k  {ℓ₂} {ℓ₁})
SK-sym {equivalence} = Eq.sym
SK-sym {bijection}   = Inv.sym

SK-isEquivalence :  k   IsEquivalence { = } (Related  k )
SK-isEquivalence k  = record
  { refl  = K-refl
  ; sym   = SK-sym
  ; trans = K-trans
  }

SK-setoid : Symmetric-kind  ( : Level)  Setoid _ _
SK-setoid k  = record { isEquivalence = SK-isEquivalence k  }

K-isPreorder :  k   IsPreorder _↔_ (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 _∼⟨_⟩_ _↔⟨_⟩_ _↔⟨⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_
  infix  1 begin_

  begin_ :  {k x y} {X : Set x} {Y : Set y} 
           X ∼[ k ] Y  X ∼[ k ] Y
  begin_ x∼y = x∼y

  _∼⟨_⟩_ :  {k x y z} (X : Set x) {Y : Set y} {Z : Set z} 
           X ∼[ k ] Y  Y ∼[ k ] Z  X ∼[ k ] Z
  _ ∼⟨ X↝Y  Y↝Z = K-trans X↝Y Y↝Z

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

  _↔⟨_⟩_ :  {k x y z} (X : Set x) {Y : Set y} {Z : Set z} 
           X  Y  Y ∼[ k ] Z  X ∼[ k ] Z
  X ↔⟨ X↔Y  Y⇔Z = X ∼⟨ ↔⇒ X↔Y  Y⇔Z

  _↔⟨⟩_ :  {k x y} (X : Set x) {Y : Set y} 
          X ∼[ k ] Y  X ∼[ k ] Y
  X ↔⟨⟩ X⇔Y = X⇔Y

  _≡˘⟨_⟩_ :  {k  z} (X : Set ) {Y : Set } {Z : Set z} 
            Y  X  Y ∼[ k ] Z  X ∼[ k ] Z
  X ≡˘⟨ Y≡X  Y⇔Z = X ∼⟨ ≡⇒ (P.sym Y≡X)  Y⇔Z

  _≡⟨_⟩_ :  {k  z} (X : Set ) {Y : Set } {Z : Set z} 
           X  Y  Y ∼[ k ] Z  X ∼[ k ] Z
  X ≡⟨ X≡Y  Y⇔Z = X ∼⟨ ≡⇒ X≡Y  Y⇔Z

  _∎ :  {k x} (X : Set x)  X ∼[ k ] X
  X  = 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   {a s} {A : Set a} 
                   (A  Set s)  A  A  Set _
InducedRelation₁ k S = λ x y  S x ∼[ k ] S y

InducedPreorder₁ : Kind   {a s} {A : Set a} 
                   (A  Set s)  Preorder _ _ _
InducedPreorder₁ k S = record
  { _≈_        = _≡_
  ; _∼_        = InducedRelation₁ k S
  ; isPreorder = record
    { isEquivalence = P.isEquivalence
    ; reflexive     = reflexive 
                      K-reflexive 
                      P.cong S
    ; trans         = K-trans
    }
  } where open Preorder (K-preorder _ _)

InducedEquivalence₁ : Symmetric-kind   {a s} {A : Set a} 
                      (A  Set s)  Setoid _ _
InducedEquivalence₁ k S = record
  { _≈_           = InducedRelation₁  k  S
  ; 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   {a b s} {A : Set a} {B : Set b} 
                   (A  B  Set s)  B  B  Set _
InducedRelation₂ k _S_ = λ x y   {z}  (z S x) ∼[ k ] (z S y)

InducedPreorder₂ : Kind   {a b s} {A : Set a} {B : Set b} 
                   (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₂ : Symmetric-kind 
                       {a b s} {A : Set a} {B : Set b} 
                      (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 _ _)