diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9874c5593d..c0dd26217b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,8 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
+
 Minor improvements
 ------------------
 
@@ -341,6 +343,11 @@ Additions to existing modules
   m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
   ```
 
+* In `Data.Product.Function.Dependent.Propositional`:
+  ```agda
+  congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
+  ```
+
 * New lemmas in `Data.Rational.Properties`:
   ```agda
   nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q)
@@ -377,6 +384,15 @@ Additions to existing modules
   _≡?_ : DecidableEquality (Vec A n)
   ```
 
+* In `Function.Related.TypeIsomorphisms`:
+  ```agda
+  Σ-distribˡ-⊎ : (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q)
+  Σ-distribʳ-⊎ : (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂))
+  ×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
+  ×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C)
+  ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
+ ```
+
 * In `Relation.Binary.Bundles`:
   ```agda
   record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda
index cb8a8d99a1..4c6f391e2f 100644
--- a/src/Data/Product/Function/Dependent/Propositional.agda
+++ b/src/Data/Product/Function/Dependent/Propositional.agda
@@ -17,7 +17,7 @@ open import Function.Related.Propositional
          implication; reverseImplication; equivalence; injection;
          reverseInjection; leftInverse; surjection; bijection)
 open import Function.Base using (_$_; _∘_; _∘′_)
-open import Function.Properties.Inverse using (↔⇒↠; ↔⇒⟶; ↔⇒⟵; ↔-sym; ↔⇒↩)
+open import Function.Properties.Inverse using (↔⇒↠; ↔⇒⟶; ↔⇒⟵; ↔-sym; ↔⇒↩; refl)
 open import Function.Properties.RightInverse using (↩⇒↪; ↪⇒↩)
 open import Function.Properties.Inverse.HalfAdjointEquivalence
   using (↔⇒≃; _≃_; ≃⇒↔)
@@ -316,3 +316,6 @@ cong {B = B} {k = reverseInjection}   I↔J A↢B = Σ-↣ (↔-sym I↔J) (swap
 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 _)
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
index 3386032654..478ef28a2e 100644
--- a/src/Function/Related/TypeIsomorphisms.agda
+++ b/src/Function/Related/TypeIsomorphisms.agda
@@ -15,7 +15,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (true; false)
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Product.Base as Product
-  using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃)
+  using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃; ∃-syntax)
 open import Data.Product.Function.NonDependent.Propositional
 open import Data.Sum.Base as Sum
 open import Data.Sum.Properties using (swap-involutive)
@@ -106,26 +106,46 @@ private
 ⊎-identity ℓ = ⊎-identityˡ ℓ , ⊎-identityʳ ℓ
 
 ------------------------------------------------------------------------
--- Properties of × and ⊎
+-- Properties of Σ and ⊎
 
--- × distributes over ⊎
+-- Σ distributes over ⊎
 
-×-distribˡ-⊎ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_
-×-distribˡ-⊎ ℓ _ _ _ = mk↔ₛ′
+Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} →
+  (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q)
+Σ-distribˡ-⊎ = mk↔ₛ′
   (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
   [ Product.map₂ inj₁ , Product.map₂ inj₂ ]′
   [ (λ _ → refl) , (λ _ → refl) ]
   (uncurry λ _ → [ (λ _ → refl) , (λ _ → refl) ])
 
-×-distribʳ-⊎ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_
-×-distribʳ-⊎ ℓ _ _ _ = mk↔ₛ′
-  (uncurry [ curry inj₁ , curry inj₂ ]′)
-  [ Product.map₁ inj₁ , Product.map₁ inj₂ ]′
+Σ-distribʳ-⊎ : {P : A ⊎ B → Set c} →
+  (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂))
+Σ-distribʳ-⊎ = mk↔ₛ′
+  (uncurry [ curry inj₁ , curry inj₂ ])
+  [ Product.dmap inj₁ id , Product.dmap inj₂ id ]
   [ (λ _ → refl) , (λ _ → refl) ]
   (uncurry [ (λ _ _ → refl) , (λ _ _ → refl) ])
 
-×-distrib-⊎ : ∀ ℓ → _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_
-×-distrib-⊎ ℓ = ×-distribˡ-⊎ ℓ , ×-distribʳ-⊎ ℓ
+------------------------------------------------------------------------
+-- Properties of × and ⊎
+
+-- × distributes over ⊎
+-- primed variants are less level polymorphic
+
+×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
+×-distribˡ-⊎ = Σ-distribˡ-⊎
+
+×-distribˡ-⊎′ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_
+×-distribˡ-⊎′ ℓ _ _ _ = ×-distribˡ-⊎
+
+×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C)
+×-distribʳ-⊎ = Σ-distribʳ-⊎
+
+×-distribʳ-⊎′ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_
+×-distribʳ-⊎′ ℓ _ _ _ = ×-distribʳ-⊎
+
+×-distrib-⊎′ : ∀ ℓ → _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_
+×-distrib-⊎′ ℓ = ×-distribˡ-⊎′ ℓ , ×-distribʳ-⊎′ ℓ
 
 ------------------------------------------------------------------------
 -- ⊥, ⊤, _×_ and _⊎_ form a commutative semiring
@@ -228,7 +248,7 @@ private
 ×-⊎-isCommutativeSemiring k ℓ = isCommutativeSemiringˡ record
   { +-isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ
   ; *-isCommutativeMonoid = ×-isCommutativeMonoid k ℓ
-  ; distribʳ              = λ A B C → ↔⇒ (×-distribʳ-⊎ ℓ A B C)
+  ; distribʳ              = λ _ _ _ → ↔⇒ ×-distribʳ-⊎
   ; zeroˡ                 = ↔⇒ ∘ ×-zeroˡ ℓ
   }
 
@@ -332,3 +352,11 @@ True↔ ( true because  [p]) irr =
   mk↔ₛ′ (λ _ → invert [p]) (λ _ → _) (irr _) (λ _ → refl)
 True↔ (false because ofⁿ ¬p) _ =
   mk↔ₛ′ (λ()) (invert (ofⁿ ¬p)) (λ x → flip contradiction ¬p x) (λ ())
+
+------------------------------------------------------------------------
+-- Relating a predicate to an existentially quantified one with the
+-- restriction that the quantified variable is equal to the given one
+
+∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
+∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py)
+  (λ where (_ , refl , _) → refl) (λ where _ → refl)