    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Non-dependent product combinators for propositional equality
    -- preserving functions
    ------------------------------------------------------------------------

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

    module Data.Product.Function.NonDependent.Propositional where

    open import Data.Product.Base using (_×_; map)
    open import Data.Product.Function.NonDependent.Setoid
    open import Data.Product.Relation.Binary.Pointwise.NonDependent
      using (_×ₛ_; Pointwise-≡↔≡)
    open import Function.Base using (id)
    open import Function.Bundles
      using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _⤖_; _↩_; _↪_; _↔_)
    open import Function.Properties.Inverse as Inv
      using (Inverse⇒Equivalence; Inverse⇒Injection; Inverse⇒Surjection;
             Inverse⇒Bijection)
    open import Function.Related.Propositional
      using (_∼[_]_; implication; reverseImplication; equivalence; injection;
             reverseInjection; leftInverse; surjection; bijection)
    import Function.Construct.Composition as Compose
    open import Level using (Level; _⊔_)
    open import Relation.Binary hiding (_⇔_)
    open import Relation.Binary.PropositionalEquality.Properties using (setoid)

    private
      variable
        a b c d : Level
        A B C D : Set a

    ------------------------------------------------------------------------
    -- Helper lemma

    private
      liftViaInverse : {R : ∀ {a b ℓ₁ ℓ₂} → REL (Setoid a ℓ₁) (Setoid b ℓ₂) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)} →
                       (∀ {a b c ℓ₁ ℓ₂ ℓ₃} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} {U : Setoid c ℓ₃} → R S T → R T U → R S U) →
                       (∀ {a b ℓ₁ ℓ₂} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} → Inverse S T → R S T) →
                       (R (setoid A) (setoid C) → R (setoid B) (setoid D) → R (setoid A ×ₛ setoid B) (setoid C ×ₛ setoid D)) →
                       R (setoid A) (setoid C) → R (setoid B) (setoid D) →
                       R (setoid (A × B)) (setoid (C × D))
      liftViaInverse trans inv⇒R lift RAC RBD =
        Inv.transportVia trans inv⇒R (Inv.sym Pointwise-≡↔≡) (lift RAC RBD) Pointwise-≡↔≡

    ------------------------------------------------------------------------
    -- Combinators for various function types

    infixr 2 _×-⟶_ _×-⇔_ _×-↣_ _×-↠_ _×-⤖_ _×-↩_ _×-↪_ _×-↔_

    _×-⟶_ : A ⟶ B → C ⟶ D → (A × C) ⟶ (B × D)
    _×-⟶_ = liftViaInverse Compose.function Inv.toFunction _×-function_

    _×-⇔_ : A ⇔ B → C ⇔ D → (A × C) ⇔ (B × D)
    _×-⇔_ = liftViaInverse Compose.equivalence Inverse⇒Equivalence _×-equivalence_

    _×-↣_ : A ↣ B → C ↣ D → (A × C) ↣ (B × D)
    _×-↣_ = liftViaInverse Compose.injection Inverse⇒Injection _×-injection_

    _×-↠_ : A ↠ B → C ↠ D → (A × C) ↠ (B × D)
    _×-↠_ = liftViaInverse Compose.surjection Inverse⇒Surjection _×-surjection_

    _×-⤖_ : A ⤖ B → C ⤖ D → (A × C) ⤖ (B × D)
    _×-⤖_ = liftViaInverse Compose.bijection Inverse⇒Bijection _×-bijection_

    _×-↩_ : A ↩ B → C ↩ D → (A × C) ↩ (B × D)
    _×-↩_ = liftViaInverse Compose.leftInverse Inverse.leftInverse _×-leftInverse_

    _×-↪_ : A ↪ B → C ↪ D → (A × C) ↪ (B × D)
    _×-↪_ = liftViaInverse Compose.rightInverse Inverse.rightInverse _×-rightInverse_

    _×-↔_ : A ↔ B → C ↔ D → (A × C) ↔ (B × D)
    _×-↔_ = liftViaInverse Compose.inverse id _×-inverse_

    infixr 2 _×-cong_

    _×-cong_ : ∀ {k} → A ∼[ k ] B → C ∼[ k ] D → (A × C) ∼[ k ] (B × D)
    _×-cong_ {k = implication}         = _×-⟶_
    _×-cong_ {k = reverseImplication}  = _×-⟶_
    _×-cong_ {k = equivalence}         = _×-⇔_
    _×-cong_ {k = injection}           = _×-↣_
    _×-cong_ {k = reverseInjection}    = _×-↣_
    _×-cong_ {k = leftInverse}         = _×-↪_
    _×-cong_ {k = surjection}          = _×-↠_
    _×-cong_ {k = bijection}           = _×-↔_