n-ary decidable equality transformer

CHANGELOG.md

@@ -94,6 +94,7 @@ New modules
 
   Data.Product.Nary.NonDependent
   Function.Nary.NonDependent
+  Function.Nary.NonDependent.Base
   Relation.Nary
 
   Data.Sign.Base
@@ -675,14 +676,6 @@ Other minor additions
   been generalised so that the types of the two equal elements need not
   be at the same universe level.
 
-* Added new proof to `Relation.Binary.PropositionalEquality`:
-  ```
-  Congₙ  : ∀ n (f g : Arrows n as b) → Set _
-  congₙ  : ∀ n (f : Arrows n as b) → Congₙ n f f
-  Substₙ : ∀ n (f g : Arrows n as (Set r)) → Set _
-  substₙ : (f : Arrows n as (Set r)) → Substₙ n f f
-  ```
-
 * Added new proof to `Relation.Binary.PropositionalEquality.Core`:
   ```agda
   ≢-sym : Symmetric _≢_

src/Data/Product/Nary/NonDependent.agda

@@ -16,14 +16,18 @@ module Data.Product.Nary.NonDependent where
 
 open import Level as L using (Level; _⊔_; Lift; 0ℓ)
 open import Agda.Builtin.Unit
-open import Data.Product
+open import Data.Product as Prod
+import Data.Product.Properties as Prodₚ
 open import Data.Sum using (_⊎_)
 open import Data.Nat.Base using (ℕ; zero; suc; pred)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Function
 open import Relation.Nullary
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)
 
-open import Function.Nary.NonDependent
+open import Function.Nary.NonDependent.Base
 
 -- Provided n Levels and a corresponding "vector" of `n` Sets, we can build a big
 -- right-nested product type packing a value for each one of these Sets.
@@ -42,6 +46,17 @@ Product 0       _        = ⊤
 Product 1       (a , _)  = a
 Product (suc n) (a , as) = a × Product n as
 
+-- Pointwise lifting of a relation on products
+
+Allₙ : (∀ {a} {A : Set a} → Rel A a) →
+        ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
+Allₙ R 0               l       r       = _
+Allₙ R 1               a       b       = R a b , _
+Allₙ R (suc n@(suc _)) (a , l) (b , r) = R a b , Allₙ R n l r
+
+Equalₙ : ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
+Equalₙ = Allₙ _≡_
+
 ------------------------------------------------------------------------
 -- Generic Programs
 
@@ -91,11 +106,40 @@ uncurryₙ (suc n@(suc _)) f = uncurry (uncurryₙ n ∘′ f)
 
 curry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
           (Product⊤ n as → b) → as ⇉ b
-curry⊤ₙ n f = curryₙ n (f ∘ toProduct⊤ n)
+curry⊤ₙ zero    f = f _
+curry⊤ₙ (suc n) f = curry⊤ₙ n ∘′ curry f
 
 uncurry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
             as ⇉ b → (Product⊤ n as → b)
-uncurry⊤ₙ n f = uncurryₙ n f ∘ toProduct n
+uncurry⊤ₙ zero    f = const f
+uncurry⊤ₙ (suc n) f = uncurry (uncurry⊤ₙ n ∘′ f)
+
+------------------------------------------------------------------------
+-- decidability
+
+Product⊤-dec : ∀ n {ls} {as : Sets n ls} → Product⊤ n (Dec <$> as) → Dec (Product⊤ n as)
+Product⊤-dec zero    _          = yes _
+Product⊤-dec (suc n) (p? , ps?) = p? ×-dec Product⊤-dec n ps?
+
+Product-dec : ∀ n {ls} {as : Sets n ls} → Product n (Dec <$> as) → Dec (Product n as)
+Product-dec 0               _          = yes _
+Product-dec 1               p?         = p?
+Product-dec (suc n@(suc _)) (p? , ps?) = p? ×-dec Product-dec n ps?
+
+------------------------------------------------------------------------
+-- pointwise liftings
+
+toEqualₙ : ∀ n {ls} {as : Sets n ls} {l r : Product n as} →
+           l ≡ r → Product n (Equalₙ n l r)
+toEqualₙ 0               eq = _
+toEqualₙ 1               eq = eq
+toEqualₙ (suc n@(suc _)) eq = Prod.map₂ (toEqualₙ n) (Prodₚ.,-injective eq)
+
+fromEqualₙ : ∀ n {ls} {as : Sets n ls} {l r : Product n as} →
+             Product n (Equalₙ n l r) → l ≡ r
+fromEqualₙ 0               eq = refl
+fromEqualₙ 1               eq = eq
+fromEqualₙ (suc n@(suc _)) eq = uncurry (cong₂ _,_) (Prod.map₂ (fromEqualₙ n) eq)
 
 ------------------------------------------------------------------------
 -- projection of the k-th component

src/Function/Nary/NonDependent.agda

@@ -18,78 +18,22 @@ open import Level using (Level; 0ℓ; _⊔_; Lift)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Product using (_×_; _,_)
-open import Data.Unit.Base
+open import Data.Product.Nary.NonDependent
 open import Function using (_∘′_; _$′_; const; flip)
 open import Relation.Unary using (IUniversal)
+open import Relation.Binary.PropositionalEquality
 
 private
   variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
+    r : Level
 
 ------------------------------------------------------------------------
--- Type Definitions
-
--- We want to define n-ary function spaces and generic n-ary operations on
--- them such as (un)currying, zipWith, alignWith, etc.
-
--- We want users to be able to use these seamlessly whenever n is concrete.
-
--- In other words, we want Agda to infer the sets `A₁, ⋯, Aₙ` when we write
--- `uncurryₙ n f` where `f` has type `A₁ → ⋯ → Aₙ → B`. For this to happen,
--- we need the structure in which these Sets are stored to effectively
--- η-expand to `A₁, ⋯, Aₙ` when the parameter `n` is known.
-
--- Hence the following definitions:
-------------------------------------------------------------------------
-
--- First, a "vector" of `n` Levels (defined by induction on n so that it
--- may be built by η-expansion and unification). Each Level will be that
--- of one of the Sets we want to take the n-ary product of.
-
-Levels : ℕ → Set
-Levels zero    = ⊤
-Levels (suc n) = Level × Levels n
-
--- The overall Level of a `n` Sets of respective levels `l₁, ⋯, lₙ` will
--- be the least upper bound `l₁ ⊔ ⋯ ⊔ lₙ` of all of the Levels involved.
--- Hence the following definition of n-ary least upper bound:
-
-⨆ : ∀ n → Levels n → Level
-⨆ zero    _        = Level.zero
-⨆ (suc n) (l , ls) = l ⊔ (⨆ n ls)
-
--- Second, a "vector" of `n` Sets whose respective Levels are determined
--- by the `Levels n` input.
-
-Sets : ∀ n (ls : Levels n) → Set (Level.suc (⨆ n ls))
-Sets zero    _        = Lift _ ⊤
-Sets (suc n) (l , ls) = Set l × Sets n ls
-
--- Third, a function type whose domains are given by a "vector" of `n` Sets
--- `A₁, ⋯, Aₙ` and whose codomain is `B`. `Arrows` forms such a type of
--- shape `A₁ → ⋯ → Aₙ → B` by induction on `n`.
-
-Arrows : ∀ n {r ls} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
-Arrows zero    _        b = b
-Arrows (suc n) (a , as) b = a → Arrows n as b
-
--- We introduce a notation for this definition
-
-infixr 0 _⇉_
-_⇉_ : ∀ {n ls r} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
-_⇉_ = Arrows _
-
+-- Re-exporting the basic operations
 
+open import Function.Nary.NonDependent.Base public
 
 ------------------------------------------------------------------------
--- Operations on Levels
-
-lmap : (Level → Level) → ∀ n → Levels n → Levels n
-lmap f zero    ls       = _
-lmap f (suc n) (l , ls) = f l , lmap f n ls
+-- Additional operations on Levels
 
 ltabulate : ∀ n → (Fin n → Level) → Levels n
 ltabulate zero    f = _
@@ -101,55 +45,33 @@ lreplicate n ℓ = ltabulate n (const ℓ)
 0ℓs : ∀[ Levels ]
 0ℓs = lreplicate _ 0ℓ
 
-
 ------------------------------------------------------------------------
--- Operations on Sets
+-- Congruence
 
-_<$>_ : (∀ {l} → Set l → Set l) →
-        ∀ {n ls} → Sets n ls → Sets n ls
-_<$>_ f {zero}   as        = _
-_<$>_ f {suc n}  (a , as)  = f a , f <$> as
+module _ n {ls} {as : Sets n ls} {R : Set r} (f : as ⇉ R) where
 
--- generalised map
+-- Congruentₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
+--                   a₁₁ ≡ a₁₂ → ⋯ → aₙ₁ ≡ aₙ₂ →
+--                   f a₁₁ ⋯ aₙ₁ ≡ f a₁₂ ⋯ aₙ₂
 
-smap : ∀ f → (∀ {l} → Set l → Set (f l)) →
-       ∀ n {ls} → Sets n ls → Sets n (lmap f n ls)
-smap f F zero    as       = _
-smap f F (suc n) (a , as) = F a , smap f F n as
+  Congruentₙ : Set (r Level.⊔ ⨆ n ls)
+  Congruentₙ = ∀ {l r} → Equalₙ n l r ⇉ (uncurryₙ n f l ≡ uncurryₙ n f r)
 
+  congₙ : Congruentₙ
+  congₙ = curryₙ n (cong (uncurryₙ n f) ∘′ fromEqualₙ n)
 
 ------------------------------------------------------------------------
--- Operations on Functions
-
--- mapping under n arguments
-
-mapₙ : ∀ n {ls} {as : Sets n ls} → (B → C) → as ⇉ B → as ⇉ C
-mapₙ zero    f v = f v
-mapₙ (suc n) f g = mapₙ n f ∘′ g
-
--- compose function at the n-th position
-
-_%=_⊢_ : ∀ n {ls} {as : Sets n ls} → (A → B) → as ⇉ (B → C) → as ⇉ (A → C)
-n %= f ⊢ g = mapₙ n (_∘′ f) g
-
--- partially apply function at the n-th position
-
-_∷=_⊢_ : ∀ n {ls} {as : Sets n ls} → A → as ⇉ (A → B) → as ⇉ B
-n ∷= x ⊢ g = mapₙ n (_$′ x) g
-
--- hole at the n-th position
-
-holeₙ : ∀ n {ls} {as : Sets n ls} → (A → as ⇉ B) → as ⇉ (A → B)
-holeₙ zero    f = f
-holeₙ (suc n) f = holeₙ n ∘′ flip f
+-- Injectivitiy
 
--- function constant in its n first arguments
+module _ n {ls} {as : Sets n ls} {R : Set r} (con : as ⇉ R) where
 
--- Note that its type will only be inferred if it is used in a context
--- specifying what the type of the function ought to be. Just like the
--- usual const: there is no way to infer its domain from its argument.
+-- Injectiveₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
+--                   con a₁₁ ⋯ aₙ₁ ≡ con a₁₂ ⋯ aₙ₂ →
+--                   a₁₁ ≡ a₁₂ × ⋯ × aₙ₁ ≡ aₙ₂
 
-constₙ : ∀ n {ls r} {as : Sets n ls} {b : Set r} → b → as ⇉ b
-constₙ zero    v = v
-constₙ (suc n) v = const (constₙ n v)
+  Injectiveₙ : Set (r Level.⊔ ⨆ n ls)
+  Injectiveₙ = ∀ {l r} → uncurryₙ n con l ≡ uncurryₙ n con r → Product n (Equalₙ n l r)
 
+  injectiveₙ : (∀ {l r} → uncurryₙ n con l ≡ uncurryₙ n con r → l ≡ r) →
+               Injectiveₙ
+  injectiveₙ con-inj eq = toEqualₙ n (con-inj eq)