    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some functional properties are symmetric
    ------------------------------------------------------------------------

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

    module Function.Construct.Symmetry where

    open import Data.Product.Base using (_,_; swap; proj₁; proj₂)
    open import Function.Base using (_∘_)
    open import Function.Definitions
      using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ
            ; Congruent)
    open import Function.Structures
      using (IsBijection; IsCongruent; IsRightInverse; IsLeftInverse; IsInverse)
    open import Function.Bundles
      using (Bijection; Equivalence; LeftInverse; RightInverse; Inverse
            ; _⤖_; _⇔_; _↩_; _↪_; _↔_)
    open import Level using (Level)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
    open import Relation.Binary.PropositionalEquality.Properties using (setoid)

    private
      variable
        a b c ℓ₁ ℓ₂ ℓ₃ : Level
        A B C : Set a

    ------------------------------------------------------------------------
    -- Properties

    module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B}
             ((inj , surj) : Bijective ≈₁ ≈₂ f)
             where

      private
        f⁻¹      = proj₁ ∘ surj
        f∘f⁻¹≡id = proj₂ ∘ surj

      injective : Reflexive ≈₁ → Symmetric ≈₂ → Transitive ≈₂ →
                  Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ f⁻¹
      injective refl sym trans cong gx≈gy =
        trans (trans (sym (f∘f⁻¹≡id _ refl)) (cong gx≈gy)) (f∘f⁻¹≡id _ refl)

      surjective : Reflexive ≈₁ → Transitive ≈₂ → Surjective ≈₂ ≈₁ f⁻¹
      surjective refl trans x = f x , inj ∘ trans (f∘f⁻¹≡id _ refl)

      bijective : Reflexive ≈₁ → Symmetric ≈₂ → Transitive ≈₂ →
                  Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
      bijective refl sym trans cong = injective refl sym trans cong , surjective refl trans

    module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f : A → B} {f⁻¹ : B → A} where

      inverseʳ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₁ f⁻¹ f
      inverseʳ inv = inv

      inverseˡ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₁ f⁻¹ f
      inverseˡ inv = inv

      inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₁ f⁻¹ f
      inverseᵇ (invˡ , invʳ) = (invʳ , invˡ)

    ------------------------------------------------------------------------
    -- Structures

    module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
             {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f)
             where

      private
        module IB = IsBijection isBij
        f⁻¹       = proj₁ ∘ IB.surjective

      -- We can only flip a bijection if the witness produced by the
      -- surjection proof respects the equality on the codomain.
      isBijection : Congruent ≈₂ ≈₁ f⁻¹ → IsBijection ≈₂ ≈₁ f⁻¹
      isBijection f⁻¹-cong = record
        { isInjection = record
          { isCongruent = record
            { cong           = f⁻¹-cong
            ; isEquivalence₁ = IB.Eq₂.isEquivalence
            ; isEquivalence₂ = IB.Eq₁.isEquivalence
            }
          ; injective = injective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong
          }
        ; surjective = surjective IB.bijective IB.Eq₁.refl IB.Eq₂.trans
        }

    module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ f) where

      -- We can always flip a bijection if using the equality over the
      -- codomain is propositional equality.
      isBijection-≡ : IsBijection _≡_ ≈₁ _
      isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong _)
        where module IB = IsBijection isBij

    module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : B → A} where

      isCongruent : IsCongruent ≈₁ ≈₂ f → Congruent ≈₂ ≈₁ f⁻¹ → IsCongruent ≈₂ ≈₁ f⁻¹
      isCongruent ic cg = record
        { cong           = cg
        ; isEquivalence₁ = F.isEquivalence₂
        ; isEquivalence₂ = F.isEquivalence₁
        } where module F = IsCongruent ic

      isLeftInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsLeftInverse ≈₂ ≈₁ f⁻¹ f
      isLeftInverse inv = record
        { isCongruent = isCongruent F.isCongruent F.from-cong
        ; from-cong   = F.to-cong
        ; inverseˡ    = inverseˡ ≈₁ ≈₂ F.inverseʳ
        } where module F = IsRightInverse inv

      isRightInverse : IsLeftInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₁ f⁻¹ f
      isRightInverse inv = record
        { isCongruent = isCongruent F.isCongruent F.from-cong
        ; from-cong   = F.to-cong
        ; inverseʳ    = inverseʳ ≈₁ ≈₂ F.inverseˡ
        } where module F = IsLeftInverse inv

      isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₁ f⁻¹ f
      isInverse f-inv = record
        { isLeftInverse = isLeftInverse F.isRightInverse
        ; inverseʳ      = inverseʳ ≈₁ ≈₂ F.inverseˡ
        } where module F = IsInverse f-inv

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

    module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where

      private
        module IB = Bijection bij
        from      = proj₁ ∘ IB.surjective

      -- We can only flip a bijection if the witness produced by the
      -- surjection proof respects the equality on the codomain.
      bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ from → Bijection S R
      bijection cong = record
        { to        = from
        ; cong      = cong
        ; bijective = bijective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong
        }

    -- We can always flip a bijection if using the equality over the
    -- codomain is propositional equality.
    bijection-≡ : {R : Setoid a ℓ₁} {B : Set b} →
                  Bijection R (setoid B) → Bijection (setoid B) R
    bijection-≡ bij = bijection bij (B.Eq₁.reflexive ∘ cong _)
     where module B = Bijection bij

    module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where

      equivalence : Equivalence R S → Equivalence S R
      equivalence equiv = record
        { to        = E.from
        ; from      = E.to
        ; to-cong   = E.from-cong
        ; from-cong = E.to-cong
        } where module E = Equivalence equiv

      rightInverse : LeftInverse R S → RightInverse S R
      rightInverse left = record
        { to         = L.from
        ; from       = L.to
        ; to-cong    = L.from-cong
        ; from-cong  = L.to-cong
        ; inverseʳ   = L.inverseˡ
        } where module L = LeftInverse left

      leftInverse : RightInverse R S → LeftInverse S R
      leftInverse right = record
        { to        = R.from
        ; from      = R.to
        ; to-cong   = R.from-cong
        ; from-cong = R.to-cong
        ; inverseˡ  = R.inverseʳ
        } where module R = RightInverse right

      inverse : Inverse R S → Inverse S R
      inverse inv = record
        { to        = I.from
        ; from      = I.to
        ; to-cong   = I.from-cong
        ; from-cong = I.to-cong
        ; inverse   = swap I.inverse
        } where module I = Inverse inv

    ------------------------------------------------------------------------
    -- Propositional bundles

    ⤖-sym : A ⤖ B → B ⤖ A
    ⤖-sym b = bijection b (cong _)

    ⇔-sym : A ⇔ B → B ⇔ A
    ⇔-sym = equivalence

    ↩-sym : A ↩ B → B ↪ A
    ↩-sym = rightInverse

    ↪-sym : A ↪ B → B ↩ A
    ↪-sym = leftInverse

    ↔-sym : A ↔ B → B ↔ A
    ↔-sym = inverse

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version v2.0

    sym-⤖ = ⤖-sym
    {-# WARNING_ON_USAGE sym-⤖
    "Warning: sym-⤖ was deprecated in v2.0.
    Please use ⤖-sym instead."
    #-}

    sym-⇔ = ⇔-sym
    {-# WARNING_ON_USAGE sym-⇔
    "Warning: sym-⇔ was deprecated in v2.0.
    Please use ⇔-sym instead."
    #-}

    sym-↩ = ↩-sym
    {-# WARNING_ON_USAGE sym-↩
    "Warning: sym-↩ was deprecated in v2.0.
    Please use ↩-sym instead."
    #-}

    sym-↪ = ↪-sym
    {-# WARNING_ON_USAGE sym-↪
    "Warning: sym-↪ was deprecated in v2.0.
    Please use ↪-sym instead."
    #-}

    sym-↔ = ↔-sym
    {-# WARNING_ON_USAGE sym-↔
    "Warning: sym-↔ was deprecated in v2.0.
    Please use ↔-sym instead."
    #-}