From 106caef555b821f3caa07eabd7990c7397433209 Mon Sep 17 00:00:00 2001 From: shhyou Date: Tue, 11 Nov 2025 11:07:08 +0800 Subject: [PATCH 1/4] Share Sum and Product type isomorphism proof --- src/Data/Product/Properties.agda | 3 +++ src/Function/Related/TypeIsomorphisms.agda | 15 +++++---------- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda index 0bfa3166df..f14e881c9b 100644 --- a/src/Data/Product/Properties.agda +++ b/src/Data/Product/Properties.agda @@ -64,6 +64,9 @@ map-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) swap-involutive : swap {A = A} {B = B} ∘ swap ≗ id swap-involutive _ = refl +swap-↔ : (A × B) ↔ (B × A) +swap-↔ = mk↔ₛ′ swap swap swap-involutive swap-involutive + ------------------------------------------------------------------------ -- Equality between pairs can be expressed as a pair of equalities diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index b1549ef14d..72bd941cc7 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -24,8 +24,9 @@ open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Data.Product.Base as Product using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃; ∃-syntax) open import Data.Product.Function.NonDependent.Propositional +import Data.Product.Properties as Product open import Data.Sum.Base as Sum -open import Data.Sum.Properties using (swap-involutive) +import Data.Sum.Properties as Sum open import Data.Sum.Function.Propositional using (_⊎-cong_) open import Data.Unit.Polymorphic.Base using (⊤) open import Level using (Level; Lift; 0ℓ; suc) @@ -63,7 +64,7 @@ open import Relation.Nullary.Decidable public -- × is commutative ×-comm : ∀ (A : Set a) (B : Set b) → (A × B) ↔ (B × A) -×-comm _ _ = mk↔ₛ′ Product.swap Product.swap (λ _ → refl) λ _ → refl +×-comm _ _ = Product.swap-↔ -- × has ⊤ as its identity @@ -102,7 +103,7 @@ open import Relation.Nullary.Decidable public -- ⊎ is commutative ⊎-comm : ∀ (A : Set a) (B : Set b) → (A ⊎ B) ↔ (B ⊎ A) -⊎-comm _ _ = mk↔ₛ′ swap swap swap-involutive swap-involutive +⊎-comm _ _ = Sum.swap-↔ -- ⊎ has ⊥ as its identity @@ -279,13 +280,7 @@ open import Relation.Nullary.Decidable public ∃∃↔∃∃ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) → (∃₂ λ x y → P x y) ↔ (∃₂ λ y x → P x y) -∃∃↔∃∃ P = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl) - where - to : (∃₂ λ x y → P x y) → (∃₂ λ y x → P x y) - to (x , y , Pxy) = (y , x , Pxy) - - from : (∃₂ λ y x → P x y) → (∃₂ λ x y → P x y) - from (y , x , Pxy) = (x , y , Pxy) +∃∃↔∃∃ = Product.∃∃↔∃∃ ------------------------------------------------------------------------ -- Implicit and explicit function spaces are isomorphic From 41aa7059c3e997178c830d89e19fe2cdee351596 Mon Sep 17 00:00:00 2001 From: shhyou Date: Tue, 11 Nov 2025 15:37:52 +0800 Subject: [PATCH 2/4] Add pairing of type isomorphism --- src/Data/Product/Properties.agda | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda index f14e881c9b..789ee5a07f 100644 --- a/src/Data/Product/Properties.agda +++ b/src/Data/Product/Properties.agda @@ -9,9 +9,9 @@ module Data.Product.Properties where open import Axiom.UniquenessOfIdentityProofs using (UIP; module Decidable⇒UIP) -open import Data.Product.Base using (_,_; Σ; _×_; map; swap; ∃; ∃₂) +open import Data.Product.Base using (_,_; Σ; _,′_; _×_; map; swap; ∃; ∃₂) open import Function.Base using (_∋_; _∘_; id) -open import Function.Bundles using (_↔_; mk↔ₛ′) +open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse) open import Level using (Level) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core @@ -114,3 +114,14 @@ module _ {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} where from : (∃₂ λ y x → R x y) → (∃₂ λ x y → R x y) from (y , x , Rxy) = (x , y , Rxy) + +------------------------------------------------------------------------ +-- Non-dependent product (_×_) preserves type isomorphism (_↔_) + +infixr 4 _,′-↔_ + +_,′-↔_ : A ↔ C → B ↔ D → (A × B) ↔ (C × D) +i ,′-↔ j = mk↔ₛ′ (map (Inverse.to i) (Inverse.to j)) + (map (Inverse.from i) (Inverse.from j)) + (λ _ → ×-≡,≡→≡ (Inverse.inverseˡ i refl ,′ Inverse.inverseˡ j refl)) + (λ _ → ×-≡,≡→≡ (Inverse.inverseʳ i refl ,′ Inverse.inverseʳ j refl)) From c3d32b1838889323cc0a87d0461eabd7ddf024b0 Mon Sep 17 00:00:00 2001 From: shhyou Date: Tue, 11 Nov 2025 14:27:16 +0800 Subject: [PATCH 3/4] Update CHANGELOG for the new functions --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 040b993eae..7bee0da902 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -190,6 +190,12 @@ Additions to existing modules ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m ``` +* In `Data.Product.Properties`: + ```agda + swap-↔ : (A × B) ↔ (B × A) + _,′-↔_ : A ↔ C → B ↔ D → (A × B) ↔ (C × D) + ``` + * In `Data.Vec.Properties`: ```agda updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) → From 99da9cbbe40fa40b4f778837b3443625c6c7415b Mon Sep 17 00:00:00 2001 From: shhyou Date: Tue, 11 Nov 2025 16:01:21 +0800 Subject: [PATCH 4/4] cosmetic changes: limit Data.Sum.Base imports --- src/Function/Related/TypeIsomorphisms.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 72bd941cc7..2e73ba648e 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -26,6 +26,7 @@ open import Data.Product.Base as Product open import Data.Product.Function.NonDependent.Propositional import Data.Product.Properties as Product open import Data.Sum.Base as Sum + using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) import Data.Sum.Properties as Sum open import Data.Sum.Function.Propositional using (_⊎-cong_) open import Data.Unit.Polymorphic.Base using (⊤)