------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles for types of functions
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

-- Note that these bundles differ from those found elsewhere in other
-- library hierarchies as they take Setoids as parameters. This is
-- because a function is of no use without knowing what its domain and
-- codomain is, as well which equalities are being considered over them.
-- One consequence of this is that they are not built from the
-- definitions found in `Function.Structures` as is usually the case in
-- other library hierarchies, as this would duplicate the equality
-- axioms.

{-# OPTIONS --without-K --safe #-}

module Function.Bundles where

import Function.Definitions as FunctionDefinitions
import Function.Structures as FunctionStructures
open import Level using (Level; _⊔_; suc)
open import Data.Product using (_,_; proj₁; proj₂)
open import Relation.Binary hiding (_⇔_)
open import Relation.Binary.PropositionalEquality as ≡
  using (_≡_)
open Setoid using (isEquivalence)

private
  variable
    a b ℓ₁ ℓ₂ : Level

------------------------------------------------------------------------
-- Setoid bundles
------------------------------------------------------------------------

module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where

  open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_)
  open Setoid To   using () renaming (Carrier to B; _≈_ to _≈₂_)
  open FunctionDefinitions _≈₁_ _≈₂_
  open FunctionStructures  _≈₁_ _≈₂_

------------------------------------------------------------------------
-- Bundles with one element

  -- Called `Func` rather than `Function` in order to avoid clashing
  -- with the top-level module.
  record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f    : A → B
      cong : f Preserves _≈₁_ ⟶ _≈₂_

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    open IsCongruent isCongruent public
      using (module Eq₁; module Eq₂)


  record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f           : A → B
      cong        : f Preserves _≈₁_ ⟶ _≈₂_
      injective   : Injective f

    function : Func
    function = record
      { f    = f
      ; cong = cong
      }

    open Func function public
      hiding (f; cong)

    isInjection : IsInjection f
    isInjection = record
      { isCongruent = isCongruent
      ; injective   = injective
      }


  record Surjection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f          : A → B
      cong       : f Preserves _≈₁_ ⟶ _≈₂_
      surjective : Surjective f

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)

    isSurjection : IsSurjection f
    isSurjection = record
      { isCongruent = isCongruent
      ; surjective  = surjective
      }


  record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      cong      : f Preserves _≈₁_ ⟶ _≈₂_
      bijective : Bijective f

    injective : Injective f
    injective = proj₁ bijective

    surjective : Surjective f
    surjective = proj₂ bijective

    injection : Injection
    injection = record
      { cong      = cong
      ; injective = injective
      }

    surjection : Surjection
    surjection = record
      { cong       = cong
      ; surjective = surjective
      }

    open Injection  injection  public using (isInjection)
    open Surjection surjection public using (isSurjection)

    isBijection : IsBijection f
    isBijection = record
      { isInjection = isInjection
      ; surjective  = surjective
      }

    open IsBijection isBijection public using (module Eq₁; module Eq₂)


------------------------------------------------------------------------
-- Bundles with two elements

  record Equivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f     : A → B
      g     : B → A
      cong₁ : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂ : g Preserves _≈₂_ ⟶ _≈₁_


  record LeftInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      g         : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : g Preserves _≈₂_ ⟶ _≈₁_
      inverseˡ  : Inverseˡ f g

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong₁
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)

    isLeftInverse : IsLeftInverse f g
    isLeftInverse = record
      { isCongruent = isCongruent
      ; cong₂       = cong₂
      ; inverseˡ    = inverseˡ
      }

    equivalence : Equivalence
    equivalence = record
      { cong₁ = cong₁
      ; cong₂ = cong₂
      }


  record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      g         : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : g Preserves _≈₂_ ⟶ _≈₁_
      inverseʳ  : Inverseʳ f g

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong₁
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    isRightInverse : IsRightInverse f g
    isRightInverse = record
      { isCongruent = isCongruent
      ; cong₂       = cong₂
      ; inverseʳ    = inverseʳ
      }

    equivalence : Equivalence
    equivalence = record
      { cong₁ = cong₁
      ; cong₂ = cong₂
      }


  record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      f⁻¹       : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : f⁻¹ Preserves _≈₂_ ⟶ _≈₁_
      inverse   : Inverseᵇ f f⁻¹

    inverseˡ : Inverseˡ f f⁻¹
    inverseˡ = proj₁ inverse

    inverseʳ : Inverseʳ f f⁻¹
    inverseʳ = proj₂ inverse

    leftInverse : LeftInverse
    leftInverse = record
      { cong₁    = cong₁
      ; cong₂    = cong₂
      ; inverseˡ = inverseˡ
      }

    rightInverse : RightInverse
    rightInverse = record
      { cong₁    = cong₁
      ; cong₂    = cong₂
      ; inverseʳ = inverseʳ
      }

    open LeftInverse leftInverse   public using (isLeftInverse)
    open RightInverse rightInverse public using (isRightInverse)

    isInverse : IsInverse f f⁻¹
    isInverse = record
      { isLeftInverse = isLeftInverse
      ; inverseʳ      = inverseʳ
      }

    open IsInverse isInverse public using (module Eq₁; module Eq₂)


------------------------------------------------------------------------
-- Bundles with three elements

  record BiEquivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f     : A → B
      g₁    : B → A
      g₂    : B → A
      cong₁ : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂ : g₁ Preserves _≈₂_ ⟶ _≈₁_
      cong₃ : g₂ Preserves _≈₂_ ⟶ _≈₁_


  record BiInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      g₁        : B → A
      g₂        : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : g₁ Preserves _≈₂_ ⟶ _≈₁_
      cong₃     : g₂ Preserves _≈₂_ ⟶ _≈₁_
      inverseˡ  : Inverseˡ f g₁
      inverseʳ  : Inverseʳ f g₂

    f-isCongruent : IsCongruent f
    f-isCongruent = record
      { cong           = cong₁
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    isBiInverse : IsBiInverse f g₁ g₂
    isBiInverse = record
      { f-isCongruent = f-isCongruent
      ; cong₂         = cong₂
      ; inverseˡ      = inverseˡ
      ; cong₃         = cong₃
      ; inverseʳ      = inverseʳ
      }

    biEquivalence : BiEquivalence
    biEquivalence = record
      { cong₁ = cong₁
      ; cong₂ = cong₂
      ; cong₃ = cong₃
      }


------------------------------------------------------------------------
-- Bundles specialised for propositional equality
------------------------------------------------------------------------

infix  _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_
_⟶_ : Set a → Set b → Set _
A ⟶ B = Func (≡.setoid A) (≡.setoid B)

_↣_ : Set a → Set b → Set _
A ↣ B = Injection (≡.setoid A) (≡.setoid B)

_↠_ : Set a → Set b → Set _
A ↠ B = Surjection (≡.setoid A) (≡.setoid B)

_⤖_ : Set a → Set b → Set _
A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)

_⇔_ : Set a → Set b → Set _
A ⇔ B = Equivalence (≡.setoid A) (≡.setoid B)

_↩_ : Set a → Set b → Set _
A ↩ B = LeftInverse (≡.setoid A) (≡.setoid B)

_↪_ : Set a → Set b → Set _
A ↪ B = RightInverse (≡.setoid A) (≡.setoid B)

_↩↪_ : Set a → Set b → Set _
A ↩↪ B = BiInverse (≡.setoid A) (≡.setoid B)

_↔_ : Set a → Set b → Set _
A ↔ B = Inverse (≡.setoid A) (≡.setoid B)

-- We now define some constructors for the above that
-- automatically provide the required congruency proofs.

module _ {A : Set a} {B : Set b} where

  open FunctionDefinitions {A = A} {B} _≡_ _≡_

  mk⟶ : (A → B) → A ⟶ B
  mk⟶ f = record
    { f         = f
    ; cong      = ≡.cong f
    }

  mk↣ : ∀ {f : A → B} → Injective f → A ↣ B
  mk↣ {f} inj = record
    { f         = f
    ; cong      = ≡.cong f
    ; injective = inj
    }

  mk↠ : ∀ {f : A → B} → Surjective f → A ↠ B
  mk↠ {f} surj = record
    { f          = f
    ; cong       = ≡.cong f
    ; surjective = surj
    }

  mk⤖ : ∀ {f : A → B} → Bijective f → A ⤖ B
  mk⤖ {f} bij = record
    { f         = f
    ; cong      = ≡.cong f
    ; bijective = bij
    }

  mk⇔ : ∀ (f : A → B) (g : B → A) → A ⇔ B
  mk⇔ f g = record
    { f     = f
    ; g     = g
    ; cong₁ = ≡.cong f
    ; cong₂ = ≡.cong g
    }

  mk↩ : ∀ {f : A → B} {g : B → A} → Inverseˡ f g → A ↩ B
  mk↩ {f} {g} invˡ = record
    { f        = f
    ; g        = g
    ; cong₁    = ≡.cong f
    ; cong₂    = ≡.cong g
    ; inverseˡ = invˡ
    }

  mk↪ : ∀ {f : A → B} {g : B → A} → Inverseʳ f g → A ↪ B
  mk↪ {f} {g} invʳ = record
    { f        = f
    ; g        = g
    ; cong₁    = ≡.cong f
    ; cong₂    = ≡.cong g
    ; inverseʳ = invʳ
    }

  mk↩↪ : ∀ {f : A → B} {g₁ : B → A} {g₂ : B → A} →
         Inverseˡ f g₁ → Inverseʳ f g₂ → A ↩↪ B
  mk↩↪ {f} {g₁} {g₂} invˡ invʳ = record
    { f        = f
    ; g₁       = g₁
    ; g₂       = g₂
    ; cong₁    = ≡.cong f
    ; cong₂    = ≡.cong g₁
    ; cong₃    = ≡.cong g₂
    ; inverseˡ = invˡ
    ; inverseʳ = invʳ
    }

  mk↔ : ∀ {f : A → B} {f⁻¹ : B → A} → Inverseᵇ f f⁻¹ → A ↔ B
  mk↔ {f} {f⁻¹} inv = record
    { f       = f
    ; f⁻¹     = f⁻¹
    ; cong₁   = ≡.cong f
    ; cong₂   = ≡.cong f⁻¹
    ; inverse = inv
    }

  -- Sometimes the implicit arguments above cannot be inferred
  mk↔′ : ∀ (f : A → B) (f⁻¹ : B → A) → Inverseˡ f f⁻¹ → Inverseʳ f f⁻¹ → A ↔ B
  mk↔′ f f⁻¹ invˡ invʳ = mk↔ {f = f} {f⁻¹ = f⁻¹} (invˡ , invʳ)