Add some type relations and isomorphisms

CHANGELOG.md

@@ -312,6 +312,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 lemma in `Data.Vec.Properties`:
   ```agda
   map-concat : map f (concat xss) ≡ concat (map (map f) xss)
@@ -322,6 +327,15 @@ Additions to existing modules
   _≡?_ : DecidableEquality (Vec A n)
   ```
 
+* In `Function.Related.TypeIsomorphisms`:
+  ```agda
+  Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} → (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q)
+  Σ-distribʳ-⊎ : {P : Set a} {Q : Set b} {R : P ⊎ Q → Set c} → (Σ (P ⊎ Q) R) ↔ (Σ P (R ∘ inj₁) ⊎ Σ Q (R ∘ 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.Construct.Interior.Symmetric`:
   ```agda
   decidable         : Decidable R → Decidable (SymInterior R)

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 _)

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,24 +106,44 @@ 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 : Set a} {Q : Set b} {R : P ⊎ Q → Set c} →
+  (Σ (P ⊎ Q) R) ↔ (Σ P (R ∘ inj₁) ⊎ Σ Q (R ∘ inj₂))
+Σ-distribʳ-⊎ = mk↔ₛ′
+  (uncurry [ curry inj₁ , curry inj₂ ])
+  [ Product.dmap inj₁ id , Product.dmap inj₂ id ]
   [ (λ _ → refl) , (λ _ → refl) ]
   (uncurry [ (λ _ _ → refl) , (λ _ _ → refl) ])
 
+------------------------------------------------------------------------
+-- Properties of × and ⊎
+
+-- × distributes over ⊎
+-- primed variants are more 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ʳ-⊎ ℓ
 
@@ -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)