Decidablity of dependent products (#1211)

Author: alexarice

CHANGELOG/v1.4.md

@@ -41,3 +41,5 @@ Other minor additions
 ---------------------
 
 * Added the decidablitity functions `_<‴?_`, `_≤‴?_`, `_≥‴?_`, and `_>‴?_` for deciding `≤‴` in `Data.Nat.Properties`.
+
+* Moved `≡-dec` from `Data.Product.Properties.WithK` to `Data.Product.Properties`. The proof has been changed so that is uses that decidability implies UIP and no longer uses axiom K. Functions `injectiveʳ-≡` and `injectiveʳ-UIP` have also been added to `Data.Product.Properties`. Aliases have been added to `Data.Product.Properties.WithK` though there could be clashes in code which imports both modules.

src/Data/Product/Properties.agda

@@ -8,12 +8,14 @@
 
 module Data.Product.Properties where
 
+open import Axiom.UniquenessOfIdentityProofs
 open import Data.Product
-open import Function using (_∘_)
-open import Relation.Binary using (Decidable)
+open import Function using (_∘_;_∋_)
+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)
 
 ------------------------------------------------------------------------
 -- Equality (dependent)
@@ -23,7 +25,17 @@ module _ {a b} {A : Set a} {B : A → Set b} where
   ,-injectiveˡ : ∀ {a c} {b : B a} {d : B c} → (a , b) ≡ (c , d) → a ≡ c
   ,-injectiveˡ refl = refl
 
-  -- See also Data.Product.Properties.WithK.,-injectiveʳ.
+  ,-injectiveʳ-≡ : ∀ {a b} {c : B a} {d : B b} → UIP A → (a , c) ≡ (b , d) → (q : a ≡ b) → subst B q c ≡ d
+  ,-injectiveʳ-≡ {c = c} u refl q = cong (λ x → subst B x c) (u q refl)
+
+  ,-injectiveʳ-UIP : ∀ {a} {b c : B a} → UIP A → (Σ A B ∋ (a , b)) ≡ (a , c) → b ≡ c
+  ,-injectiveʳ-UIP u p = ,-injectiveʳ-≡ u p refl
+
+  ≡-dec : DecidableEquality A → (∀ {a} → DecidableEquality (B a)) →
+          DecidableEquality (Σ A B)
+  ≡-dec dec₁ dec₂ (a , x) (b , y) with dec₁ a b
+  ... | no [a≢b] = no ([a≢b] ∘ ,-injectiveˡ)
+  ... | yes refl = Dec.map′ (cong (a ,_)) (,-injectiveʳ-UIP (Decidable⇒UIP.≡-irrelevant dec₁)) (dec₂ x y)
 
 ------------------------------------------------------------------------
 -- Equality (non-dependent)
@@ -35,8 +47,3 @@ module _ {a b} {A : Set a} {B : Set b} where
 
   ,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
   ,-injective refl = refl , refl
-
-  ≡-dec : Decidable {A = A} _≡_ → Decidable {A = B} _≡_ →
-          Decidable {A = A × B} _≡_
-  ≡-dec dec₁ dec₂ (a , b) (c , d) =
-    Dec.map′ (uncurry (cong₂ _,_)) ,-injective (dec₁ a c ×-dec dec₂ b d)

src/Data/Product/Properties/WithK.agda

@@ -8,33 +8,17 @@
 
 module Data.Product.Properties.WithK where
 
-open import Data.Bool.Base
 open import Data.Product
-open import Data.Product.Properties using (,-injectiveˡ)
 open import Function
-open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Reflects
-open import Relation.Nullary using (Dec; _because_; yes; no)
-open import Relation.Nullary.Decidable using (map′)
 
 ------------------------------------------------------------------------
 -- Equality
 
-module _ {a b} {A : Set a} {B : Set b} where
-
-  ,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
-  ,-injective refl = refl , refl
+-- These exports are deprecated from v1.4
+open import Data.Product.Properties using (,-injective; ≡-dec) public
 
 module _ {a b} {A : Set a} {B : A → Set b} where
 
   ,-injectiveʳ : ∀ {a} {b c : B a} → (Σ A B ∋ (a , b)) ≡ (a , c) → b ≡ c
   ,-injectiveʳ refl = refl
-
-  -- Note: this is not an instance of `_×-dec_`, because we need `x` and `y`
-  -- to have the same type before we can test them for equality.
-  ≡-dec : Decidable _≡_ → (∀ {a} → Decidable {A = B a} _≡_) →
-          Decidable {A = Σ A B} _≡_
-  ≡-dec dec₁ dec₂ (a , x) (b , y) with dec₁ a b
-  ... | false because [a≢b] = no (invert [a≢b] ∘ ,-injectiveˡ)
-  ... | yes refl = map′ (cong (a ,_)) ,-injectiveʳ (dec₂ x y)