Port old TypeIsomorphisms over to the new Function hierarchy. (#1203)

Author: JacquesCarette

CHANGELOG.md

@@ -170,6 +170,18 @@ New modules
   Data.Vec.Functional.Properties
   ```
 
+* Modules replacing `Function.Related.TypeIsomorphisms` using the new
+  `Inverse` definitions.
+  ```
+  Data.Sum.Algebra
+  Data.Product.Algebra
+  ```
+
+* Basic properties of the function type `A → B`:
+  ```agda
+  Function.Properties
+  ```
+
 * Symmetry for various functional properties
   ```agda
   Function.Construct.Symmetry
@@ -205,6 +217,7 @@ New modules
 * Indexed nullary relations/sets:
   ```
   Relation.Nullary.Indexed
+  Relation.Nullary.Indexed.Negation
   ```
 
 * Symmetric transitive closures of binary relations:
@@ -433,8 +446,15 @@ Other minor additions
   recompute       : .(Coprime n d) → Coprime n d
   ```
 
-* Added new functions to `Data.Product`:
+* Add new functions to `Data.Product`:
   ```agda
+  assocʳ-curried : Σ (Σ A B) C → Σ A (λ a → Σ (B a) (curry C a))
+  assocˡ-curried : Σ A (λ a → Σ (B a) (curry C a)) → Σ (Σ A B) C
+  assocʳ         : Σ (Σ A B) (uncurry C) → Σ A (λ a → Σ (B a) (C a))
+  assocˡ         : Σ A (λ a → Σ (B a) (C a)) → Σ (Σ A B) (uncurry C)
+  assocʳ′        : (A × B) × C → A × (B × C)
+  assocˡ′        : A × (B × C) → (A × B) × C
+
   dmap : (f : (a : A) → B a) → (∀ {a} (p : P a) → Q p (f a)) →
          (ap : Σ A P) → Σ (B (proj₁ ap)) (Q (proj₂ ap))
   dmap : ((a : A) → X a) → ((b : B) → Y b) →
@@ -443,6 +463,19 @@ Other minor additions
           ((a , b) : A × B) → X a × Y b
   ```
 
+* Added new proofs to `Data.Product.Properties`:
+  ```agda
+  Σ-≡,≡↔≡ : {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : Σ A B} → (∃ λ (p : a₁ ≡ a₂) → subst B p b₁ ≡ b₂) ↔ (p₁ ≡ p₂)
+  ×-≡,≡↔≡ : {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} → (a₁ ≡ a₂ × b₁ ≡ b₂) ↔ p₁ ≡ p₂
+  ∃∃↔∃∃   : (R : A → B → Set ℓ) → (∃₂ λ x y → R x y) ↔ (∃₂ λ y x → R x y)
+  ```
+
+* Add new functions to `Data.Sum.Base`:
+  ```agda
+  assocʳ : (A ⊎ B) ⊎ C → A ⊎ B ⊎ C
+  assocˡ : A ⊎ B ⊎ C → (A ⊎ B) ⊎ C
+  ```
+
 * Made first argument of `[,]-∘-distr` in `Data.Sum.Properties` explicit
 
 * Added new proofs to `Data.Sum.Properties`:
@@ -583,6 +616,11 @@ Other minor additions
   _on₂_   : (C → C → D) → (A → B → C) → (A → B → D)
   ```
 
+* Added new function in `Function.Bundles`:
+  ```agda
+  mk↔′ : ∀ (f : A → B) (f⁻¹ : B → A) → Inverseˡ f f⁻¹ → Inverseʳ f f⁻¹ → A ↔ B
+  ```
+
 * Added new operator to `Relation.Binary`:
   ```agda
   _⇔_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _
@@ -604,6 +642,11 @@ Other minor additions
   icong′ : {f : A → B} x → f x ≡ f x
   ```
 
+* Added new proof to `Relation.Nullary.Decidable`:
+  ```agda
+  True-↔ : (dec : Dec P) → Irrelevant P → True dec ↔ P
+  ```
+
 * Added new proofs to `Relation.Binary.Construct.NonStrictToStrict`:
   ```agda
   <-isDecStrictPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecStrictPartialOrder _≈_ _<_

src/Data/Product.agda

@@ -136,6 +136,25 @@ uncurry : ∀ {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
           ((p : Σ A B) → C p)
 uncurry f (x , y) = f x y
 
+-- Rewriting dependent products
+assocʳ : {B : A → Set b} {C : (a : A) → B a → Set c} →
+          Σ (Σ A B) (uncurry C) → Σ A (λ a → Σ (B a) (C a))
+assocʳ ((a , b) , c) = (a , (b , c))
+
+assocˡ : {B : A → Set b} {C : (a : A) → B a → Set c} →
+          Σ A (λ a → Σ (B a) (C a)) → Σ (Σ A B) (uncurry C)
+assocˡ (a , (b , c)) = ((a , b) , c)
+
+-- Alternate form of associativity for dependent products
+-- where the C parameter is uncurried.
+assocʳ-curried : {B : A → Set b} {C : Σ A B → Set c} →
+                 Σ (Σ A B) C → Σ A (λ a → Σ (B a) (curry C a))
+assocʳ-curried ((a , b) , c) = (a , (b , c))
+
+assocˡ-curried : {B : A → Set b} {C : Σ A B → Set c} →
+          Σ A (λ a → Σ (B a) (curry C a)) → Σ (Σ A B) C
+assocˡ-curried (a , (b , c)) = ((a , b) , c)
+
 ------------------------------------------------------------------------
 -- Operations for non-dependent products
 
@@ -174,3 +193,10 @@ f -×- g = f -⟪ _×_ ⟫- g
 
 _-,-_ : (A → B → C) → (A → B → D) → (A → B → C × D)
 f -,- g = f -⟪ _,_ ⟫- g
+
+-- Rewriting non-dependent products
+assocʳ′ : (A × B) × C → A × (B × C)
+assocʳ′ ((a , b) , c) = (a , (b , c))
+
+assocˡ′ : A × (B × C) → (A × B) × C
+assocˡ′ (a , (b , c)) = ((a , b) , c)

src/Data/Product/Algebra.agda

@@ -0,0 +1,184 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Algebraic properties of products
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Product.Algebra where
+
+open import Algebra
+open import Data.Bool.Base using (true; false)
+open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
+open import Data.Product
+open import Data.Product.Properties
+open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
+open import Data.Sum.Algebra
+open import Data.Unit.Polymorphic using (⊤; tt)
+open import Function.Base using (_∘′_)
+open import Function.Bundles using (_↔_; Inverse; mk↔′)
+open import Function.Properties.Inverse using (↔-isEquivalence)
+open import Level using (Level; suc)
+open import Relation.Binary.PropositionalEquality.Core
+
+import Function.Definitions as FuncDef
+
+------------------------------------------------------------------------
+
+private
+  variable
+    a b c d p : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+
+  module _ {A : Set a} {B : Set b} where
+    open FuncDef {A = A} {B} _≡_ _≡_
+
+------------------------------------------------------------------------
+-- Properties of Σ
+
+-- Σ is associative
+Σ-assoc : {B : A → Set b} {C : (a : A) → B a → Set c} →
+          Σ (Σ A B) (uncurry C) ↔ Σ A (λ a → Σ (B a) (C a))
+Σ-assoc = mk↔′ assocʳ assocˡ cong′ cong′
+
+-- Σ is associative, alternate formulation
+Σ-assoc-alt : {B : A → Set b} {C : Σ A B → Set c} →
+          Σ (Σ A B) C ↔ Σ A (λ a → Σ (B a) (curry C a))
+Σ-assoc-alt = mk↔′ assocʳ-curried assocˡ-curried cong′ cong′
+
+------------------------------------------------------------------------
+-- Algebraic properties
+
+-- × is a congruence
+×-cong : A ↔ B → C ↔ D → (A × C) ↔ (B × D)
+×-cong i j = mk↔′ (map I.f J.f) (map I.f⁻¹ J.f⁻¹)
+  (λ {(a , b) → cong₂ _,_ (I.inverseˡ a) (J.inverseˡ b)})
+  (λ {(a , b) → cong₂ _,_ (I.inverseʳ a) (J.inverseʳ b)})
+  where module I = Inverse i; module J = Inverse j
+
+-- × is commutative.
+-- (we don't use Commutative because it isn't polymorphic enough)
+×-comm : (A : Set a) (B : Set b) → (A × B) ↔ (B × A)
+×-comm _ _ = mk↔′ swap swap swap-involutive swap-involutive
+
+module _ (ℓ : Level) where
+
+  -- × is associative
+  ×-assoc : Associative {ℓ = ℓ} _↔_ _×_
+  ×-assoc _ _ _ = mk↔′ assocʳ′ assocˡ′ cong′ cong′
+
+  -- ⊤ is the identity for ×
+  ×-identityˡ : LeftIdentity {ℓ = ℓ} _↔_ ⊤ _×_
+  ×-identityˡ _ = mk↔′ proj₂ (tt ,_) cong′ cong′
+
+  ×-identityʳ : RightIdentity {ℓ = ℓ} _↔_ ⊤ _×_
+  ×-identityʳ _ = mk↔′ proj₁ (_, tt) cong′ cong′
+
+  ×-identity : Identity _↔_ ⊤ _×_
+  ×-identity = ×-identityˡ , ×-identityʳ
+
+  -- ⊥ is the zero for ×
+  ×-zeroˡ : LeftZero {ℓ = ℓ} _↔_ ⊥ _×_
+  ×-zeroˡ A = mk↔′ proj₁ ⊥-elim ⊥-elim λ ()
+
+  ×-zeroʳ : RightZero {ℓ = ℓ} _↔_ ⊥ _×_
+  ×-zeroʳ A = mk↔′ proj₂ ⊥-elim ⊥-elim λ ()
+
+  ×-zero : Zero _↔_ ⊥ _×_
+  ×-zero = ×-zeroˡ , ×-zeroʳ
+
+  -- × distributes over ⊎
+  ×-distribˡ-⊎ : _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_
+  ×-distribˡ-⊎ _ _ _ = mk↔′
+    (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
+    [ map₂ inj₁ , map₂ inj₂ ]′
+    Sum.[ cong′ , cong′ ]
+    (uncurry λ _ → Sum.[ cong′ , cong′ ])
+
+  ×-distribʳ-⊎ : _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_
+  ×-distribʳ-⊎ _ _ _ = mk↔′
+    (uncurry [ curry inj₁ , curry inj₂ ]′)
+    [ map₁ inj₁ , map₁ inj₂ ]′
+    Sum.[ cong′ , cong′ ]
+    (uncurry Sum.[ (λ _ → cong′) , (λ _ → cong′) ])
+
+  ×-distrib-⊎ : _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_
+  ×-distrib-⊎ = ×-distribˡ-⊎ , ×-distribʳ-⊎
+
+------------------------------------------------------------------------
+-- Algebraic structures
+
+  ×-isMagma : IsMagma {ℓ = ℓ} _↔_ _×_
+  ×-isMagma = record
+    { isEquivalence = ↔-isEquivalence
+    ; ∙-cong        = ×-cong
+    }
+
+  ×-isSemigroup : IsSemigroup _↔_ _×_
+  ×-isSemigroup = record
+    { isMagma = ×-isMagma
+    ; assoc   = λ _ _ _ → Σ-assoc
+    }
+
+  ×-isMonoid : IsMonoid _↔_ _×_ ⊤
+  ×-isMonoid = record
+    { isSemigroup = ×-isSemigroup
+    ; identity    = ×-identityˡ , ×-identityʳ
+    }
+
+  ×-isCommutativeMonoid : IsCommutativeMonoid _↔_ _×_ ⊤
+  ×-isCommutativeMonoid = record
+    { isMonoid = ×-isMonoid
+    ; comm     = ×-comm
+    }
+
+  ⊎-×-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _↔_ _⊎_ _×_ ⊥ ⊤
+  ⊎-×-isSemiringWithoutAnnihilatingZero = record
+    { +-isCommutativeMonoid = ⊎-isCommutativeMonoid ℓ
+    ; *-isMonoid            = ×-isMonoid
+    ; distrib               = ×-distrib-⊎
+    }
+
+  ⊎-×-isSemiring : IsSemiring _↔_ _⊎_ _×_ ⊥ ⊤
+  ⊎-×-isSemiring = record
+    { isSemiringWithoutAnnihilatingZero = ⊎-×-isSemiringWithoutAnnihilatingZero
+    ; zero                              = ×-zero
+    }
+
+  ⊎-×-isCommutativeSemiring : IsCommutativeSemiring _↔_ _⊎_ _×_ ⊥ ⊤
+  ⊎-×-isCommutativeSemiring = record
+    { isSemiring = ⊎-×-isSemiring
+    ; *-comm     = ×-comm
+    }
+------------------------------------------------------------------------
+-- Algebraic bundles
+
+  ×-magma : Magma (suc ℓ) ℓ
+  ×-magma = record
+    { isMagma = ×-isMagma
+    }
+
+  ×-semigroup : Semigroup (suc ℓ) ℓ
+  ×-semigroup = record
+    { isSemigroup = ×-isSemigroup
+    }
+
+  ×-monoid : Monoid (suc ℓ) ℓ
+  ×-monoid = record
+    { isMonoid = ×-isMonoid
+    }
+
+  ×-commutativeMonoid : CommutativeMonoid (suc ℓ) ℓ
+  ×-commutativeMonoid = record
+    { isCommutativeMonoid = ×-isCommutativeMonoid
+    }
+
+  ×-⊎-commutativeSemiring : CommutativeSemiring (suc ℓ) ℓ
+  ×-⊎-commutativeSemiring = record
+    { isCommutativeSemiring = ⊎-×-isCommutativeSemiring
+    }
+

src/Data/Product/Properties.agda

@@ -10,17 +10,24 @@ module Data.Product.Properties where
 
 open import Axiom.UniquenessOfIdentityProofs
 open import Data.Product
-open import Function using (_∘_;_∋_)
+open import Function
+open import Level using (Level)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Product
 import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary using (Dec; yes; no)
 
+private
+  variable
+    a b ℓ : Level
+    A : Set a
+    B : Set b
+
 ------------------------------------------------------------------------
 -- Equality (dependent)
 
-module _ {a b} {A : Set a} {B : A → Set b} where
+module _ {B : A → Set b} where
 
   ,-injectiveˡ : ∀ {a c} {b : B a} {d : B c} → (a , b) ≡ (c , d) → a ≡ c
   ,-injectiveˡ refl = refl
@@ -40,10 +47,57 @@ module _ {a b} {A : Set a} {B : A → Set b} where
 ------------------------------------------------------------------------
 -- Equality (non-dependent)
 
-module _ {a b} {A : Set a} {B : Set b} where
+,-injectiveʳ : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → b ≡ d
+,-injectiveʳ refl = refl
+
+,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
+,-injective refl = refl , refl
+
+-- The following properties are definitionally true (because of η)
+-- but for symmetry with ⊎ it is convenient to define and name them.
+
+swap-involutive : swap {A = A} {B = B} ∘ swap ≗ id
+swap-involutive _ = refl
+
+------------------------------------------------------------------------
+-- Equality between pairs can be expressed as a pair of equalities
+
+Σ-≡,≡↔≡ : {A : Set a} {B : A → Set b} {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : Σ A B} →
+          (∃ λ (p : a₁ ≡ a₂) → subst B p b₁ ≡ b₂) ↔ (p₁ ≡ p₂)
+Σ-≡,≡↔≡ {A = A} {B = B} = mk↔ {f = to} (right-inverse-of , left-inverse-of)
+  where
+  to : {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : Σ A B} →
+       Σ (a₁ ≡ a₂) (λ p → subst B p b₁ ≡ b₂) → p₁ ≡ p₂
+  to (refl , refl) = refl
+
+  from : {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : Σ A B} →
+         p₁ ≡ p₂ → Σ (a₁ ≡ a₂) (λ p → subst B p b₁ ≡ b₂)
+  from refl = refl , refl
+
+  left-inverse-of : {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : Σ A B} →
+                    (p : Σ (a₁ ≡ a₂) (λ x → subst B x b₁ ≡ b₂)) →
+                    from (to p) ≡ p
+  left-inverse-of (refl , refl) = refl
+
+  right-inverse-of : {p₁ p₂ : Σ A B} (p : p₁ ≡ p₂) → to (from p) ≡ p
+  right-inverse-of refl = refl
+
+-- the non-dependent case. Proofs are exactly as above, and straightforward.
+×-≡,≡↔≡ : {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} → (a₁ ≡ a₂ × b₁ ≡ b₂) ↔ p₁ ≡ p₂
+×-≡,≡↔≡ = mk↔′
+  (λ {(refl , refl) → refl})
+  (λ { refl         → refl , refl})
+  (λ {refl → refl})
+  (λ {(refl , refl) → refl})
+
+------------------------------------------------------------------------
+-- The order of ∃₂ can be swapped
 
-  ,-injectiveʳ : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → b ≡ d
-  ,-injectiveʳ refl = refl
+∃∃↔∃∃ : (R : A → B → Set ℓ) → (∃₂ λ x y → R x y) ↔ (∃₂ λ y x → R x y)
+∃∃↔∃∃ R = mk↔′ to from cong′ cong′
+  where
+  to : (∃₂ λ x y → R x y) → (∃₂ λ y x → R x y)
+  to (x , y , Rxy) = (y , x , Rxy)
 
-  ,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
-  ,-injective refl = refl , refl
+  from : (∃₂ λ y x → R x y) → (∃₂ λ x y → R x y)
+  from (y , x , Rxy) = (x , y , Rxy)