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

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

    module Data.Product.Function.Dependent.Propositional where

    open import Data.Product.Base as Product using (Σ; map; proj₂; _,_)
    open import Data.Product.Properties using (Σ-≡,≡→≡; Σ-≡,≡↔≡; Σ-≡,≡←≡)
    open import Level using (Level; 0ℓ)
    open import Function.Related.Propositional
      using (_∼[_]_; module EquationalReasoning; K-reflexive;
             implication; reverseImplication; equivalence; injection;
             reverseInjection; leftInverse; surjection; bijection)
    open import Function.Base using (_$_; _∘_; _∘′_)
    open import Function.Properties.Inverse using (↔⇒↠; ↔⇒⟶; ↔⇒⟵; ↔-sym; ↔⇒↩; refl)
    open import Function.Properties.RightInverse using (↩⇒↪; ↪⇒↩)
    open import Function.Properties.Inverse.HalfAdjointEquivalence
      using (↔⇒≃; _≃_; ≃⇒↔)
    open import Function.Consequences.Propositional
      using (inverseʳ⇒injective; strictlySurjective⇒surjective)
    open import Function.Definitions using (Inverseˡ; Inverseʳ; Injective; StrictlySurjective)
    open import Function.Bundles
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
    open import Relation.Binary.PropositionalEquality.Properties as ≡
      using (module ≡-Reasoning)
    open import Function.Construct.Symmetry using (↩-sym; ↪-sym)

    private
      variable
        i a b c d : Level
        I J : Set i
        A B : I → Set a

    ------------------------------------------------------------------------
    -- Functions

    module _ where
      open Func

      Σ-⟶ : (I⟶J : I ⟶ J) →
             (∀ {i} → A i ⟶ B (to I⟶J i)) →
             Σ I A ⟶ Σ J B
      Σ-⟶ I⟶J A⟶B = mk⟶ $ Product.map (to I⟶J) (to A⟶B)

    ------------------------------------------------------------------------
    -- Equivalences

    module _ where
      open Surjection

      Σ-⇔ : (I↠J : I ↠ J) →
             (∀ {i} → A i ⇔ B (to I↠J i)) →
             Σ I A ⇔ Σ J B
      Σ-⇔ {B = B} I↠J A⇔B = mk⇔
        (map (to  I↠J) (Equivalence.to A⇔B))
        (map (to⁻ I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl))))

      -- See also Data.Product.Relation.Binary.Pointwise.Dependent.WithK.↣.

    ------------------------------------------------------------------------
    -- Injections

    module _ where

      Σ-↣ : (I↔J : I ↔ J) →
             (∀ {i} → A i ↣ B (Inverse.to I↔J i)) →
             Σ I A ↣ Σ J B
      Σ-↣ {I = I} {J = J} {A = A} {B = B} I↔J A↣B = mk↣ to-injective
        where
        open ≡.≡-Reasoning

        I≃J = ↔⇒≃ I↔J

        subst-application′ :
          let open _≃_ I≃J in
          {x₁ x₂ : I} {y : A (from (to x₁))}
          (g : ∀ x → A (from (to x)) → B (to x))
          (eq : to x₁ ≡ to x₂) →
          ≡.subst B eq (g x₁ y) ≡ g x₂ (≡.subst A (≡.cong from eq) y)
        subst-application′ {x₁} {x₂} {y} g eq =
          ≡.subst B eq (g x₁ y)                      ≡⟨ ≡.cong (≡.subst B eq) (≡.sym (g′-lemma _ _)) ⟩
          ≡.subst B eq (g′ (to x₁) y)                ≡⟨ ≡.subst-application A g′ eq ⟩
          g′ (to x₂) (≡.subst A (≡.cong from eq) y)  ≡⟨ g′-lemma _ _ ⟩
          g x₂ (≡.subst A (≡.cong from eq) y)        ∎
          where
          open _≃_ I≃J

          g′ : ∀ x → A (from x) → B x
          g′ x =
            ≡.subst B (right-inverse-of x) ∘
            g (from x) ∘
            ≡.subst A (≡.sym (≡.cong from (right-inverse-of x)))

          g′-lemma : ∀ x y → g′ (to x) y ≡ g x y
          g′-lemma x y =
            ≡.subst B (right-inverse-of (to x))
              (g (from (to x)) $
               ≡.subst A (≡.sym (≡.cong from (right-inverse-of (to x)))) y)  ≡⟨ ≡.cong (λ p → ≡.subst B p (g (from (to x))
                                                                                                               (≡.subst A (≡.sym (≡.cong from p)) y)))
                                                                                   (≡.sym (left-right x)) ⟩
            ≡.subst B (≡.cong to (left-inverse-of x))
              (g (from (to x)) $
               ≡.subst A
                 (≡.sym (≡.cong from (≡.cong to (left-inverse-of x))))
                 y)                                                           ≡⟨ lemma _ ⟩

            g x y                                                             ∎
            where
            lemma : ∀ {x′} eq {y : A (from (to x′))} →
                      ≡.subst B (≡.cong to eq)
                        (g (from (to x))
                          (≡.subst A (≡.sym (≡.cong from (≡.cong to eq))) y)) ≡
                      g x′ y
            lemma ≡.refl = ≡.refl

        open Injection

        to′ : Σ I A → Σ J B
        to′ = Product.map (_≃_.to I≃J) (to A↣B)

        to-injective : Injective _≡_ _≡_ to′
        to-injective {(x₁ , x₂)} {(y₁ , y₂)} =

          Σ-≡,≡→≡ ∘′

          map (_≃_.injective I≃J) (λ {eq₁} eq₂ → injective A↣B (
                  to A↣B (≡.subst A (_≃_.injective I≃J eq₁) x₂)             ≡⟨⟩

                  (let eq =
                          ≡.trans (≡.sym (_≃_.left-inverse-of I≃J x₁))
                            (≡.trans (≡.cong (_≃_.from I≃J) eq₁)
                              (≡.trans (_≃_.left-inverse-of I≃J y₁)
                                ≡.refl)) in
                  to A↣B (≡.subst A eq x₂))                                   ≡⟨ ≡.cong (λ p → to A↣B
                                                                                                 (≡.subst A
                                                                                                   (≡.trans (≡.sym (_≃_.left-inverse-of I≃J _))
                                                                                                      (≡.trans (≡.cong (_≃_.from I≃J) eq₁) p))
                                                                                                   x₂))
                                                                                   (≡.trans-reflʳ _) ⟩

                  (let eq = ≡.trans (≡.sym (_≃_.left-inverse-of I≃J x₁))
                              (≡.trans (≡.cong (_≃_.from I≃J) eq₁)
                                (_≃_.left-inverse-of I≃J y₁)) in
                  to A↣B (≡.subst A eq x₂))                                  ≡⟨ ≡.cong (to A↣B)
                                                                                   (≡.sym (≡.subst-subst (≡.sym (_≃_.left-inverse-of I≃J _)))) ⟩

                  to A↣B ((≡.subst A (≡.trans (≡.cong (_≃_.from I≃J) eq₁)
                                 (_≃_.left-inverse-of I≃J y₁)) $
                   ≡.subst A (≡.sym (_≃_.left-inverse-of I≃J x₁)) x₂))      ≡⟨ ≡.cong (to A↣B)
                                                                                   (≡.sym (≡.subst-subst (≡.cong (_≃_.from I≃J) eq₁))) ⟩
                  to A↣B (
                  (≡.subst A (_≃_.left-inverse-of I≃J y₁) $
                   ≡.subst A (≡.cong (_≃_.from I≃J) eq₁) $
                   ≡.subst A (≡.sym (_≃_.left-inverse-of I≃J x₁)) x₂))      ≡⟨ ≡.sym (subst-application′
                                                                                          (λ x y → to A↣B
                                                                                                     (≡.subst A (_≃_.left-inverse-of I≃J x) y))
                                                                                          eq₁) ⟩
                  ≡.subst B eq₁ (to A↣B $
                     (≡.subst A (_≃_.left-inverse-of I≃J x₁) $
                      ≡.subst A (≡.sym (_≃_.left-inverse-of I≃J x₁)) x₂))  ≡⟨ ≡.cong (≡.subst B eq₁ ∘ to A↣B)
                                                                                   (≡.subst-subst (≡.sym (_≃_.left-inverse-of I≃J _))) ⟩

                  (let eq = ≡.trans (≡.sym (_≃_.left-inverse-of I≃J x₁))
                              (_≃_.left-inverse-of I≃J x₁) in
                  ≡.subst B eq₁ (to A↣B (≡.subst A eq x₂)))                  ≡⟨ ≡.cong (λ p → ≡.subst B eq₁ (to A↣B (≡.subst A p x₂)))
                                                                                  (≡.trans-symˡ (_≃_.left-inverse-of I≃J _)) ⟩
                  ≡.subst B eq₁ (to A↣B (≡.subst A ≡.refl x₂))               ≡⟨⟩

                  ≡.subst B eq₁ (to A↣B x₂)                                  ≡⟨ eq₂ ⟩

                  to A↣B y₂                                                  ∎

            )) ∘

          Σ-≡,≡←≡

    ------------------------------------------------------------------------
    -- Surjections

    module _ where
      open Surjection

      Σ-↠ : (I↠J : I ↠ J) →
           (∀ {x} → A x ↠ B (to I↠J x)) →
           Σ I A ↠ Σ J B
      Σ-↠ {I = I} {J = J} {A = A} {B = B} I↠J A↠B =
        mk↠ₛ strictlySurjective′
        where
        to′ : Σ I A → Σ J B
        to′ = map (to I↠J) (to A↠B)

        backcast : ∀ {i} → B i → B (to I↠J (to⁻ I↠J i))
        backcast = ≡.subst B (≡.sym (to∘to⁻ I↠J _))

        to⁻′ : Σ J B → Σ I A
        to⁻′ = map (to⁻ I↠J) (Surjection.to⁻ A↠B ∘ backcast)

        strictlySurjective′ : StrictlySurjective _≡_ to′
        strictlySurjective′ (x , y) = to⁻′ (x , y) , Σ-≡,≡→≡
          ( to∘to⁻ I↠J x
          , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (to⁻ A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩
             ≡.subst B (to∘to⁻ I↠J x) (backcast y)                      ≡⟨ ≡.subst-subst-sym (to∘to⁻ I↠J x) ⟩
             y                                                          ∎)
          ) where open ≡.≡-Reasoning

    ------------------------------------------------------------------------
    -- Left inverses

    module _ where
      open LeftInverse

      Σ-↩ : (I↩J : I ↩ J) →
             (∀ {i} → A i ↩ B (to I↩J i)) →
             Σ I A ↩ Σ J B
      Σ-↩ {I = I} {J = J} {A = A} {B = B} I↩J A↩B = mk↩ {to = to′ } {from = from′} inv
        where
        to′ : Σ I A → Σ J B
        to′ = map (to I↩J) (to A↩B)

        backcast : ∀ {j} → B j → B (to I↩J (from I↩J j))
        backcast = ≡.subst B (≡.sym (inverseˡ I↩J ≡.refl))

        from′ : Σ J B → Σ I A
        from′ = map (from I↩J) (from A↩B ∘ backcast)

        inv : Inverseˡ _≡_ _≡_ to′ from′
        inv {j , b} ≡.refl = Σ-≡,≡→≡ (strictlyInverseˡ I↩J j  , (
          begin
            ≡.subst B (inverseˡ I↩J ≡.refl) (to A↩B (from A↩B (backcast b))) ≡⟨ ≡.cong (≡.subst B _) (inverseˡ A↩B ≡.refl) ⟩
            ≡.subst B (inverseˡ I↩J ≡.refl) (backcast b)                       ≡⟨ ≡.subst-subst-sym (inverseˡ I↩J _) ⟩
            b                                                                  ∎)) where open ≡.≡-Reasoning

    ------------------------------------------------------------------------
    -- Right inverses

    module _ where
      open RightInverse

      -- the dual to Σ-↩, taking advantage of the proof above by threading
      -- relevant symmetry proofs through it.
      Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B
      Σ-↪ I↪J A↪B = ↩-sym (Σ-↩ (↪-sym I↪J) (↪-sym A↪B))

    ------------------------------------------------------------------------
    -- Inverses

    module _ where
      open Inverse

      Σ-↔ : (I↔J : I ↔ J) →
          (∀ {x} → A x ↔ B (to I↔J x)) →
          Σ I A ↔ Σ J B
      Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′
        (Surjection.to surjection′)
        (Surjection.to⁻ surjection′)
        (Surjection.to∘to⁻ surjection′)
        left-inverse-of
        where
        open ≡.≡-Reasoning

        I≃J = ↔⇒≃ I↔J

        surjection′ : Σ I A ↠ Σ J B
        surjection′ = Σ-↠ (↔⇒↠ (≃⇒↔ I≃J)) (↔⇒↠ A↔B)

        left-inverse-of : ∀ p → Surjection.to⁻ surjection′ (Surjection.to surjection′ p) ≡ p
        left-inverse-of (x , y) = to Σ-≡,≡↔≡
          ( _≃_.left-inverse-of I≃J x
          , (≡.subst A (_≃_.left-inverse-of I≃J x)
               (from A↔B
                  (≡.subst B (≡.sym (_≃_.right-inverse-of I≃J
                                        (_≃_.to I≃J x)))
                     (to A↔B y)))                   ≡⟨ ≡.subst-application B (λ _ → from A↔B) _ ⟩

             from A↔B
               (≡.subst B (≡.cong (_≃_.to I≃J)
                              (_≃_.left-inverse-of I≃J x))
                  (≡.subst B (≡.sym (_≃_.right-inverse-of I≃J
                                        (_≃_.to I≃J x)))
                     (to A↔B y)))                   ≡⟨ ≡.cong (λ eq → from A↔B (≡.subst B eq
                                                                                      (≡.subst B (≡.sym (_≃_.right-inverse-of I≃J _)) _)))
                                                                       (_≃_.left-right I≃J _) ⟩
             from A↔B
               (≡.subst B (_≃_.right-inverse-of I≃J
                              (_≃_.to I≃J x))
                  (≡.subst B (≡.sym (_≃_.right-inverse-of I≃J
                                        (_≃_.to I≃J x)))
                     (to A↔B y)))                   ≡⟨ ≡.cong (from A↔B)
                                                                       (≡.subst-subst-sym (_≃_.right-inverse-of I≃J _)) ⟩

             from A↔B (to A↔B y)      ≡⟨ Inverse.strictlyInverseʳ A↔B _ ⟩

             y                                                    ∎)
          )

    private module _ where
      open Inverse

      swap-coercions : ∀ {k} (B : J → Set b)
        (I↔J : _↔_ I J) →
        (∀ {x} → A x ∼[ k ] B (to I↔J x)) →
        ∀ {x} → A (from I↔J x) ∼[ k ] B x
      swap-coercions {A = A} B I↔J eq {x} =
        A (from I↔J x)           ∼⟨ eq ⟩
        B (to I↔J (from I↔J x)) ↔⟨ K-reflexive (≡.cong B $ strictlyInverseˡ I↔J x) ⟩
        B x                       ∎
        where open EquationalReasoning

    cong : ∀ {k} (I↔J : I ↔ J) →
           (∀ {x} → A x ∼[ k ] B (Inverse.to I↔J x)) →
           Σ I A ∼[ k ] Σ J B
    cong {k = implication}                I↔J A⟶B = Σ-⟶ (↔⇒⟶ I↔J) A⟶B
    cong {B = B} {k = reverseImplication} I↔J A⟵B = Σ-⟶ (↔⇒⟵ I↔J) (swap-coercions {k = reverseImplication} B I↔J A⟵B)
    cong {k = equivalence}                I↔J A⇔B = Σ-⇔ (↔⇒↠ I↔J) A⇔B
    cong {k = injection}                  I↔J A↣B = Σ-↣ I↔J A↣B
    cong {B = B} {k = reverseInjection}   I↔J A↢B = Σ-↣ (↔-sym I↔J) (swap-coercions {k = reverseInjection} B I↔J A↢B)
    cong {B = B} {k = leftInverse}        I↔J A↩B = ↩⇒↪ (Σ-↩ (↔⇒↩ (↔-sym I↔J)) (↪⇒↩ (swap-coercions {k = leftInverse} B I↔J A↩B)))
    cong {k = surjection}                 I↔J A↠B = Σ-↠ (↔⇒↠ I↔J) A↠B
    cong {k = bijection}                  I↔J A↔B = Σ-↔ I↔J A↔B

    congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
    congˡ = cong (refl _)