[ fixed #1452 ] more universe-polymorphic combinators for indexed containers (#1458)

Author: andreasabel

CHANGELOG.md

@@ -35,6 +35,10 @@ Bug-fixes
   `Relation.Binary.Reasoning.Base.Partial`, they will need to adjust their additional
   combinators to use the new `singleStep`/`multiStep` constructors of `_IsRelatedTo_`.
 
+* The sum operator `_⊎_` in `Data.Container.Indexed.Combinator` was not as universe 
+  polymorphic as it should have been. This has been fixed. The old, less universe
+  polymorphic variant is still available under the new name `_⊎′_`.
+  
 * The proof `isEquivalence` in `Function.Properties.(Equivalence/Inverse)` used to be 
   defined in an anonymous module that took two unneccessary `Setoid` arguments:
   ```agda
@@ -178,6 +182,11 @@ New modules
   Data.List.Relation.Binary.Pointwise.Properties
   ```
 
+* Heterogeneous `All` predicate for disjoint sums:
+  ```
+  Data.Sum.Relation.Unary.All
+  ```
+
 * Broke up `Codata.Musical.Colist` into a multitude of modules:
   ```
   Codata.Musical.Colist.Base

src/Data/Container/Indexed/Combinator.agda

@@ -14,6 +14,7 @@ open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
 open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
+open import Data.Sum.Relation.Unary.All as All using (All)
 open import Function as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
 open import Function.Inverse using (_↔̇_; inverse)
 open import Level
@@ -22,51 +23,30 @@ open import Relation.Unary using (Pred; _⊆_; _∪_; _∩_; ⋃; ⋂)
 open import Relation.Binary.PropositionalEquality as P
   using (_≗_; refl)
 
+private
+  variable
+    ℓ ℓ₁ ℓ₂ i j k o c c₁ c₂ r r₁ r₂ x z : Level
+    I J K O X Z : Set _
+
 ------------------------------------------------------------------------
 -- Combinators
 
 
 -- Identity.
 
-id : ∀ {o c r} {O : Set o} → Container O O c r
+id : Container O O c r
 id = F.const ⊤ ◃ F.const ⊤ / (λ {o} _ _ → o)
 
 -- Constant.
 
-const : ∀ {i o c r} {I : Set i} {O : Set o} →
-        Pred O c → Container I O c r
+const : Pred O c → Container I O c r
 const X = X ◃ F.const ⊥ / F.const ⊥-elim
 
--- Duality.
-
-_^⊥ : ∀ {i o c r} {I : Set i} {O : Set o} →
-      Container I O c r → Container I O (c ⊔ r) c
-(C ◃ R / n) ^⊥ = record
-  { Command  = λ o → (c : C o) → R c
-  ; Response = λ {o} _ → C o
-  ; next     = λ f c → n c (f c)
-  }
-
--- Strength.
-
-infixl 3 _⋊_
-
-_⋊_ : ∀ {i o c r z} {I : Set i} {O : Set o} (C : Container I O c r)
-      (Z : Set z) → Container (I ⟨×⟩ Z) (O ⟨×⟩ Z) c r
-C ◃ R / n ⋊ Z = C ⟨∘⟩ proj₁ ◃ R / λ {oz} c r → n c r , proj₂ oz
-
-infixr 3 _⋉_
-
-_⋉_ : ∀ {i o z c r} {I : Set i} {O : Set o} (Z : Set z)
-      (C : Container I O c r) → Container (Z ⟨×⟩ I) (Z ⟨×⟩ O) c r
-Z ⋉ C ◃ R / n = C ⟨∘⟩ proj₂ ◃ R / λ {zo} c r → proj₁ zo , n c r
-
 -- Composition.
 
 infixr 9 _∘_
 
-_∘_ : ∀ {i j k c r} {I : Set i} {J : Set j} {K : Set k} →
-      Container J K c r → Container I J c r → Container I K _ _
+_∘_ : Container J K c₁ r₁ → Container I J c₂ r₂ → Container I K _ _
 C₁ ∘ C₂ = C ◃ R / n
   where
   C : ∀ k → Set _
@@ -78,13 +58,37 @@ C₁ ∘ C₂ = C ◃ R / n
   n : ∀ {k} (c : ⟦ C₁ ⟧ (Command C₂) k) → R c → _
   n (_ , f) (r₁ , r₂) = next C₂ (f r₁) r₂
 
--- Product. (Note that, up to isomorphism, this is a special case of
--- indexed product.)
+-- Duality.
+
+_^⊥ : Container I O c r → Container I O (c ⊔ r) c
+(C ^⊥) .Command  o     = (c : C .Command o) → C .Response c
+(C ^⊥) .Response {o} _ = C .Command o
+(C ^⊥) .next     f c   = C .next c (f c)
+
+-- Strength.
+
+infixl 3 _⋊_
+
+_⋊_ : Container I O c r → (Z : Set z) → Container (I ⟨×⟩ Z) (O ⟨×⟩ Z) c r
+(C ⋊ Z) .Command  (o , z)     = C .Command o
+(C ⋊ Z) .Response             = C .Response
+(C ⋊ Z) .next     {o , z} c r = C .next c r , z
+
+infixr 3 _⋉_
+
+_⋉_ : (Z : Set z) → Container I O c r → Container (Z ⟨×⟩ I) (Z ⟨×⟩ O) c r
+(Z ⋉ C) .Command  (z , o)     = C .Command o
+(Z ⋉ C) .Response             = C .Response
+(Z ⋉ C) .next     {z , o} c r = z , C .next c r
+
+
+
+-- Product. (Note that, up to isomorphism, and ignoring universe level
+-- issues, this is a special case of indexed product.)
 
 infixr 2 _×_
 
-_×_ : ∀ {i o c r} {I : Set i} {O : Set o} →
-      Container I O c r → Container I O c r → Container I O c r
+_×_ : Container I O c₁ r₁ → Container I O c₂ r₂ → Container I O _ _
 (C₁ ◃ R₁ / n₁) × (C₂ ◃ R₂ / n₂) = record
   { Command  = C₁ ∩ C₂
   ; Response = R₁ ⟪⊙⟫ R₂
@@ -93,31 +97,35 @@ _×_ : ∀ {i o c r} {I : Set i} {O : Set o} →
 
 -- Indexed product.
 
-Π : ∀ {x i o c r} {X : Set x} {I : Set i} {O : Set o} →
-    (X → Container I O c r) → Container I O _ _
+Π : (X → Container I O c r) → Container I O _ _
 Π {X = X} C = record
   { Command  = ⋂ X (Command ⟨∘⟩ C)
   ; Response = ⋃[ x ∶ X ] λ c → Response (C x) (c x)
   ; next     = λ { c (x , r) → next (C x) (c x) r }
   }
 
--- Sum. (Note that, up to isomorphism, this is a special case of
--- indexed sum.)
+-- Sum. (Note that, up to isomorphism, and ignoring universe level
+-- issues, this is a special case of indexed sum.)
+
+infixr 1  _⊎_ _⊎′_
 
-infixr 1 _⊎_
+_⊎_ : Container I O c₁ r₁ → Container I O c₂ r₂ → Container I O _ _
+(C₁ ⊎ C₂) .Command  = C₁ .Command ∪ C₂ .Command
+(C₁ ⊎ C₂) .Response = All (C₁ .Response) (C₂ .Response)
+(C₁ ⊎ C₂) .next     = All.[ C₁ .next , C₂ .next ]
 
-_⊎_ : ∀ {i o c r} {I : Set i} {O : Set o} →
-      Container I O c r → Container I O c r → Container I O _ _
-(C₁ ◃ R₁ / n₁) ⊎ (C₂ ◃ R₂ / n₂) = record
+-- A simplified version for responses at the same level r:
+
+_⊎′_ : Container I O c₁ r → Container I O c₂ r → Container I O _ r
+(C₁ ◃ R₁ / n₁) ⊎′ (C₂ ◃ R₂ / n₂) = record
   { Command  = C₁ ∪ C₂
-  ; Response = R₁ ⟪⊎⟫ R₂
+  ; Response = [ R₁ , R₂ ]
   ; next     = [ n₁ , n₂ ]
   }
 
 -- Indexed sum.
 
-Σ : ∀ {x i o c r} {X : Set x} {I : Set i} {O : Set o} →
-    (X → Container I O c r) → Container I O _ r
+Σ : (X → Container I O c r) → Container I O _ r
 Σ {X = X} C = record
   { Command  = ⋃ X (Command ⟨∘⟩ C)
   ; Response = λ { (x , c) → Response (C x) c }
@@ -129,17 +137,15 @@ _⊎_ : ∀ {i o c r} {I : Set i} {O : Set o} →
 
 infix 0 const[_]⟶_
 
-const[_]⟶_ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} →
-             Set ℓ → Container I O c r → Container I O _ _
+const[_]⟶_ : (X : Set ℓ) → Container I O c r → Container I O _ _
 const[ X ]⟶ C = Π {X = X} (F.const C)
 
 ------------------------------------------------------------------------
 -- Correctness proofs
 
 module Identity where
 
-  correct : ∀ {o ℓ c r} {O : Set o} {X : Pred O ℓ} →
-            ⟦ id {c = c}{r} ⟧ X ↔̇ F.id X
+  correct : {X : Pred O ℓ} → ⟦ id {c = c}{r} ⟧ X ↔̇ F.id X
   correct {X = X} = inverse to from (λ _ → refl) (λ _ → refl)
     where
     to : ∀ {x} → ⟦ id ⟧ X x → F.id X x
@@ -150,8 +156,7 @@ module Identity where
 
 module Constant (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
 
-  correct : ∀ {i o ℓ₁ ℓ₂} {I : Set i} {O : Set o} (X : Pred O ℓ₁)
-            {Y : Pred O ℓ₂} → ⟦ const X ⟧ Y ↔̇ F.const X Y
+  correct : (X : Pred O ℓ₁) {Y : Pred O ℓ₂} → ⟦ const X ⟧ Y ↔̇ F.const X Y
   correct X {Y} = record
     { to         = P.→-to-⟶ to
     ; from       = P.→-to-⟶ from
@@ -172,16 +177,14 @@ module Constant (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
 
 module Duality where
 
-  correct : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
-              (C : Container I O c r) (X : Pred I ℓ) →
+  correct : (C : Container I O c r) (X : Pred I ℓ) →
             ⟦ C ^⊥ ⟧ X ↔̇ (λ o → (c : Command C o) → ∃ λ r → X (next C c r))
   correct C X = inverse (λ { (f , g) → < f , g > }) (λ f → proj₁ ⟨∘⟩ f , proj₂ ⟨∘⟩ f)
                         (λ _ → refl) (λ _ → refl)
 
 module Composition where
 
-  correct : ∀ {i j k ℓ c r} {I : Set i} {J : Set j} {K : Set k}
-              (C₁ : Container J K c r) (C₂ : Container I J c r) →
+  correct : (C₁ : Container J K c r) (C₂ : Container I J c r) →
             {X : Pred I ℓ} → ⟦ C₁ ∘ C₂ ⟧ X ↔̇ (⟦ C₁ ⟧ ⟨∘⟩ ⟦ C₂ ⟧) X
   correct C₁ C₂ {X} = inverse to from (λ _ → refl) (λ _ → refl)
     where
@@ -193,8 +196,7 @@ module Composition where
 
 module Product (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
 
-  correct : ∀ {i o c r} {I : Set i} {O : Set o}
-              (C₁ C₂ : Container I O c r) {X} →
+  correct : (C₁ C₂ : Container I O c r) {X : Pred I _} →
             ⟦ C₁ × C₂ ⟧ X ↔̇ (⟦ C₁ ⟧ X ∩ ⟦ C₂ ⟧ X)
   correct C₁ C₂ {X} = inverse to from from∘to (λ _ → refl)
     where
@@ -210,8 +212,7 @@ module Product (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
 
 module IndexedProduct where
 
-  correct : ∀ {x i o c r ℓ} {X : Set x} {I : Set i} {O : Set o}
-              (C : X → Container I O c r) {Y : Pred I ℓ} →
+  correct : (C : X → Container I O c r) {Y : Pred I ℓ} →
             ⟦ Π C ⟧ Y ↔̇ ⋂[ x ∶ X ] ⟦ C x ⟧ Y
   correct {X = X} C {Y} = inverse to from (λ _ → refl) (λ _ → refl)
     where
@@ -221,18 +222,38 @@ module IndexedProduct where
     from : ⋂[ x ∶ X ] ⟦ C x ⟧ Y ⊆ ⟦ Π C ⟧ Y
     from f = (proj₁ ⟨∘⟩ f , uncurry (proj₂ ⟨∘⟩ f))
 
-module Sum where
+module Sum (ext : ∀ {ℓ₁ ℓ₂} → Extensionality ℓ₁ ℓ₂) where
 
-  correct : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
-              (C₁ C₂ : Container I O c r) {X : Pred I ℓ} →
+  correct : (C₁ C₂ : Container I O c r) {X : Pred I ℓ} →
             ⟦ C₁ ⊎ C₂ ⟧ X ↔̇ (⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X)
   correct C₁ C₂ {X} = inverse to from from∘to to∘from
     where
     to : ⟦ C₁ ⊎ C₂ ⟧ X ⊆ ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X
+    to (inj₁ c₁ , k) = inj₁ (c₁ , λ r → k (All.inj₁ r))
+    to (inj₂ c₂ , k) = inj₂ (c₂ , λ r → k (All.inj₂ r))
+
+    from : ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X ⊆ ⟦ C₁ ⊎ C₂ ⟧ X
+    from (inj₁ (c , f)) = inj₁ c , λ{ (All.inj₁ r) → f r}
+    from (inj₂ (c , f)) = inj₂ c , λ{ (All.inj₂ r) → f r}
+
+    from∘to : from ⟨∘⟩ to ≗ F.id
+    from∘to (inj₁ _ , _) = P.cong (inj₁ _ ,_) (ext λ{ (All.inj₁ r) → refl})
+    from∘to (inj₂ _ , _) = P.cong (inj₂ _ ,_) (ext λ{ (All.inj₂ r) → refl})
+
+    to∘from : to ⟨∘⟩ from ≗ F.id
+    to∘from =  [ (λ _ → refl) , (λ _ → refl) ]
+
+module Sum′ where
+
+  correct : (C₁ C₂ : Container I O c r) {X : Pred I ℓ} →
+            ⟦ C₁ ⊎′ C₂ ⟧ X ↔̇ (⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X)
+  correct C₁ C₂ {X} = inverse to from from∘to to∘from
+    where
+    to : ⟦ C₁ ⊎′ C₂ ⟧ X ⊆ ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X
     to (inj₁ c₁ , k) = inj₁ (c₁ , k)
     to (inj₂ c₂ , k) = inj₂ (c₂ , k)
 
-    from : ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X ⊆ ⟦ C₁ ⊎ C₂ ⟧ X
+    from : ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X ⊆ ⟦ C₁ ⊎′ C₂ ⟧ X
     from = [ Prod.map inj₁ F.id , Prod.map inj₂ F.id ]
 
     from∘to : from ⟨∘⟩ to ≗ F.id
@@ -244,8 +265,7 @@ module Sum where
 
 module IndexedSum where
 
-  correct : ∀ {x i o c r ℓ} {X : Set x} {I : Set i} {O : Set o}
-              (C : X → Container I O c r) {Y : Pred I ℓ} →
+  correct : (C : X → Container I O c r) {Y : Pred I ℓ} →
             ⟦ Σ C ⟧ Y ↔̇ ⋃[ x ∶ X ] ⟦ C x ⟧ Y
   correct {X = X} C {Y} = inverse to from (λ _ → refl) (λ _ → refl)
     where
@@ -257,7 +277,6 @@ module IndexedSum where
 
 module ConstantExponentiation where
 
-  correct : ∀ {x i o c r ℓ} {X : Set x} {I : Set i} {O : Set o}
-              (C : Container I O c r) {Y : Pred I ℓ} →
+  correct : (C : Container I O c r) {Y : Pred I ℓ} →
             ⟦ const[ X ]⟶ C ⟧ Y ↔̇ (⋂ X (F.const (⟦ C ⟧ Y)))
   correct C {Y} = IndexedProduct.correct (F.const C) {Y}

src/Data/Container/Indexed/FreeMonad.agda

@@ -28,7 +28,7 @@ infix  9 _⋆_
 
 _⋆C_ : ∀ {i o c r} {I : Set i} {O : Set o} →
        Container I O c r → Pred O c → Container I O _ _
-C ⋆C X = const X ⊎ C
+C ⋆C X = const X ⊎′ C
 
 _⋆_ : ∀ {ℓ} {O : Set ℓ} → Container O O ℓ ℓ → Pt O ℓ
 C ⋆ X = μ (C ⋆C X)

src/Data/Sum/Relation/Unary/All.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Heterogeneous `All` predicate for disjoint sums
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Sum.Relation.Unary.All where
+
+open import Data.Sum.Base  using (_⊎_; inj₁; inj₂)
+open import Level          using (Level; _⊔_)
+open import Relation.Unary using (Pred)
+
+private
+  variable
+    a b c p q : Level
+    A B : Set _
+    P Q : Pred A p
+
+------------------------------------------------------------------------
+-- Definition
+
+data All {A : Set a} {B : Set b} (P : Pred A p) (Q : Pred B q)
+         : Pred (A ⊎ B) (a ⊔ b ⊔ p ⊔ q) where
+  inj₁ : ∀ {a} → P a → All P Q (inj₁ a)
+  inj₂ : ∀ {b} → Q b → All P Q (inj₂ b)
+
+------------------------------------------------------------------------
+-- Operations
+
+-- Elimination
+
+[_,_] : ∀ {C : (x : A ⊎ B) → All P Q x → Set c} →
+        ((x : A) (y : P x) → C (inj₁ x) (inj₁ y)) →
+        ((x : B) (y : Q x) → C (inj₂ x) (inj₂ y)) →
+        (x : A ⊎ B) (y : All P Q x) → C x y
+[ f , g ] (inj₁ x) (inj₁ y) = f x y
+[ f , g ] (inj₂ x) (inj₂ y) = g x y