From 6a15b8e52a92110a5cedd0d44a1a814f91a935c4 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 11 Feb 2024 12:49:37 +0000
Subject: [PATCH 1/2] Qualified import of `Data.Sum.Base as Sum`
---
src/Codata/Sized/Delay.agda | 6 ++--
src/Data/Container/Combinator.agda | 32 +++++++++----------
src/Data/Container/Combinator/Properties.agda | 28 ++++++++--------
3 files changed, 33 insertions(+), 33 deletions(-)
diff --git a/src/Codata/Sized/Delay.agda b/src/Codata/Sized/Delay.agda
index b4549089e7..4219bae341 100644
--- a/src/Codata/Sized/Delay.agda
+++ b/src/Codata/Sized/Delay.agda
@@ -16,9 +16,9 @@ open import Data.Empty
open import Relation.Nullary
open import Data.Nat.Base
open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align)
-open import Data.Product.Base as P hiding (map ; zip)
-open import Data.Sum.Base as S hiding (map)
-open import Data.These.Base as T using (These; this; that; these)
+open import Data.Product.Base hiding (map ; zip)
+open import Data.Sum.Base hiding (map)
+open import Data.These.Base using (These; this; that; these)
open import Function.Base using (id)
------------------------------------------------------------------------
diff --git a/src/Data/Container/Combinator.agda b/src/Data/Container/Combinator.agda
index 01e102cd5c..3d73977470 100644
--- a/src/Data/Container/Combinator.agda
+++ b/src/Data/Container/Combinator.agda
@@ -10,8 +10,8 @@ module Data.Container.Combinator where
open import Level using (Level; _⊔_; lower)
open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
-open import Data.Product.Base as P using (_,_; <_,_>; proj₁; proj₂; ∃)
-open import Data.Sum.Base as S using ([_,_]′)
+open import Data.Product.Base as Product using (_,_; <_,_>; proj₁; proj₂; ∃)
+open import Data.Sum.Base as Sum using ([_,_]′)
open import Data.Unit.Polymorphic.Base using (⊤)
import Function.Base as F
@@ -58,10 +58,10 @@ module _ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s
_∘_ .Position = ◇ C₁ (Position C₂)
to-∘ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) → ⟦ _∘_ ⟧ A
- to-∘ (s , f) = ((s , proj₁ F.∘ f) , P.uncurry (proj₂ F.∘ f) F.∘′ ◇.proof)
+ to-∘ (s , f) = ((s , proj₁ F.∘ f) , Product.uncurry (proj₂ F.∘ f) F.∘′ ◇.proof)
from-∘ : ∀ {a} {A : Set a} → ⟦ _∘_ ⟧ A → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A)
- from-∘ ((s , f) , g) = (s , < f , P.curry (g F.∘′ any) >)
+ from-∘ ((s , f) , g) = (s , < f , Product.curry (g F.∘′ any) >)
-- Product. (Note that, up to isomorphism, this is a special case of
-- indexed product.)
@@ -69,14 +69,14 @@ module _ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s
infixr 2 _×_
_×_ : Container (s₁ ⊔ s₂) (p₁ ⊔ p₂)
- _×_ .Shape = Shape C₁ P.× Shape C₂
- _×_ .Position = P.uncurry λ s₁ s₂ → (Position C₁ s₁) S.⊎ (Position C₂ s₂)
+ _×_ .Shape = Shape C₁ Product.× Shape C₂
+ _×_ .Position = Product.uncurry λ s₁ s₂ → (Position C₁ s₁) Sum.⊎ (Position C₂ s₂)
- to-× : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A → ⟦ _×_ ⟧ A
+ to-× : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A → ⟦ _×_ ⟧ A
to-× ((s₁ , f₁) , (s₂ , f₂)) = ((s₁ , s₂) , [ f₁ , f₂ ]′)
- from-× : ∀ {a} {A : Set a} → ⟦ _×_ ⟧ A → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A
- from-× ((s₁ , s₂) , f) = ((s₁ , f F.∘ S.inj₁) , (s₂ , f F.∘ S.inj₂))
+ from-× : ∀ {a} {A : Set a} → ⟦ _×_ ⟧ A → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A
+ from-× ((s₁ , s₂) , f) = ((s₁ , f F.∘ Sum.inj₁) , (s₂ , f F.∘ Sum.inj₂))
-- Indexed product.
@@ -87,7 +87,7 @@ module _ {i s p} (I : Set i) (Cᵢ : I → Container s p) where
Π .Position = λ s → ∃ λ i → Position (Cᵢ i) (s i)
to-Π : ∀ {a} {A : Set a} → (∀ i → ⟦ Cᵢ i ⟧ A) → ⟦ Π ⟧ A
- to-Π f = (proj₁ F.∘ f , P.uncurry (proj₂ F.∘ f))
+ to-Π f = (proj₁ F.∘ f , Product.uncurry (proj₂ F.∘ f))
from-Π : ∀ {a} {A : Set a} → ⟦ Π ⟧ A → ∀ i → ⟦ Cᵢ i ⟧ A
from-Π (s , f) = λ i → (s i , λ p → f (i , p))
@@ -108,15 +108,15 @@ module _ {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where
infixr 1 _⊎_
_⊎_ : Container (s₁ ⊔ s₂) p
- _⊎_ .Shape = (Shape C₁ S.⊎ Shape C₂)
+ _⊎_ .Shape = (Shape C₁ Sum.⊎ Shape C₂)
_⊎_ .Position = [ Position C₁ , Position C₂ ]′
- to-⊎ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A → ⟦ _⊎_ ⟧ A
- to-⊎ = [ P.map S.inj₁ F.id , P.map S.inj₂ F.id ]′
+ to-⊎ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A → ⟦ _⊎_ ⟧ A
+ to-⊎ = [ Product.map Sum.inj₁ F.id , Product.map Sum.inj₂ F.id ]′
- from-⊎ : ∀ {a} {A : Set a} → ⟦ _⊎_ ⟧ A → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A
- from-⊎ (S.inj₁ s₁ , f) = S.inj₁ (s₁ , f)
- from-⊎ (S.inj₂ s₂ , f) = S.inj₂ (s₂ , f)
+ from-⊎ : ∀ {a} {A : Set a} → ⟦ _⊎_ ⟧ A → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A
+ from-⊎ (Sum.inj₁ s₁ , f) = Sum.inj₁ (s₁ , f)
+ from-⊎ (Sum.inj₂ s₂ , f) = Sum.inj₂ (s₂ , f)
-- Indexed sum.
diff --git a/src/Data/Container/Combinator/Properties.agda b/src/Data/Container/Combinator/Properties.agda
index 6f7c83e993..188bc398c6 100644
--- a/src/Data/Container/Combinator/Properties.agda
+++ b/src/Data/Container/Combinator/Properties.agda
@@ -13,12 +13,12 @@ open import Data.Container.Core
open import Data.Container.Combinator
open import Data.Container.Relation.Unary.Any
open import Data.Empty using (⊥-elim)
-open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
+open import Data.Product.Base as P using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_])
open import Function.Base as F using (_∘′_)
open import Function.Bundles
open import Level using (_⊔_; lower)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
-- I have proved some of the correctness statements under the
-- assumption of functional extensionality. I could have reformulated
@@ -27,35 +27,35 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
module Identity where
correct : ∀ {s p x} {X : Set x} → ⟦ id {s} {p} ⟧ X ↔ F.id X
- correct {X = X} = mk↔ₛ′ from-id to-id (λ _ → P.refl) (λ _ → P.refl)
+ correct {X = X} = mk↔ₛ′ from-id to-id (λ _ → ≡.refl) (λ _ → ≡.refl)
module Constant (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′) where
correct : ∀ {x p y} (X : Set x) {Y : Set y} → ⟦ const {x} {p ⊔ y} X ⟧ Y ↔ F.const X Y
- correct {x} {y} X {Y} = mk↔ₛ′ (from-const X) (to-const X) (λ _ → P.refl) from∘to
+ correct {x} {y} X {Y} = mk↔ₛ′ (from-const X) (to-const X) (λ _ → ≡.refl) from∘to
where
from∘to : (x : ⟦ const X ⟧ Y) → to-const X (proj₁ x) ≡ x
- from∘to xs = P.cong (proj₁ xs ,_) (ext (λ x → ⊥-elim (lower x)))
+ from∘to xs = ≡.cong (proj₁ xs ,_) (ext (λ x → ⊥-elim (lower x)))
module Composition {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
correct : ∀ {x} {X : Set x} → ⟦ C₁ ∘ C₂ ⟧ X ↔ (⟦ C₁ ⟧ F.∘ ⟦ C₂ ⟧) X
- correct {X = X} = mk↔ₛ′ (from-∘ C₁ C₂) (to-∘ C₁ C₂) (λ _ → P.refl) (λ _ → P.refl)
+ correct {X = X} = mk↔ₛ′ (from-∘ C₁ C₂) (to-∘ C₁ C₂) (λ _ → ≡.refl) (λ _ → ≡.refl)
module Product (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′)
{s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
- correct : ∀ {x} {X : Set x} → ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X Prod.× ⟦ C₂ ⟧ X)
- correct {X = X} = mk↔ₛ′ (from-× C₁ C₂) (to-× C₁ C₂) (λ _ → P.refl) from∘to
+ correct : ∀ {x} {X : Set x} → ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X P.× ⟦ C₂ ⟧ X)
+ correct {X = X} = mk↔ₛ′ (from-× C₁ C₂) (to-× C₁ C₂) (λ _ → ≡.refl) from∘to
where
from∘to : (to-× C₁ C₂) F.∘ (from-× C₁ C₂) ≗ F.id
from∘to (s , f) =
- P.cong (s ,_) (ext [ (λ _ → P.refl) , (λ _ → P.refl) ])
+ ≡.cong (s ,_) (ext [ (λ _ → ≡.refl) , (λ _ → ≡.refl) ])
module IndexedProduct {i s p} {I : Set i} (Cᵢ : I → Container s p) where
correct : ∀ {x} {X : Set x} → ⟦ Π I Cᵢ ⟧ X ↔ (∀ i → ⟦ Cᵢ i ⟧ X)
- correct {X = X} = mk↔ₛ′ (from-Π I Cᵢ) (to-Π I Cᵢ) (λ _ → P.refl) (λ _ → P.refl)
+ correct {X = X} = mk↔ₛ′ (from-Π I Cᵢ) (to-Π I Cᵢ) (λ _ → ≡.refl) (λ _ → ≡.refl)
module Sum {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where
@@ -63,16 +63,16 @@ module Sum {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) whe
correct {X = X} = mk↔ₛ′ (from-⊎ C₁ C₂) (to-⊎ C₁ C₂) to∘from from∘to
where
from∘to : (to-⊎ C₁ C₂) F.∘ (from-⊎ C₁ C₂) ≗ F.id
- from∘to (inj₁ s₁ , f) = P.refl
- from∘to (inj₂ s₂ , f) = P.refl
+ from∘to (inj₁ s₁ , f) = ≡.refl
+ from∘to (inj₂ s₂ , f) = ≡.refl
to∘from : (from-⊎ C₁ C₂) F.∘ (to-⊎ C₁ C₂) ≗ F.id
- to∘from = [ (λ _ → P.refl) , (λ _ → P.refl) ]
+ to∘from = [ (λ _ → ≡.refl) , (λ _ → ≡.refl) ]
module IndexedSum {i s p} {I : Set i} (C : I → Container s p) where
correct : ∀ {x} {X : Set x} → ⟦ Σ I C ⟧ X ↔ (∃ λ i → ⟦ C i ⟧ X)
- correct {X = X} = mk↔ₛ′ (from-Σ I C) (to-Σ I C) (λ _ → P.refl) (λ _ → P.refl)
+ correct {X = X} = mk↔ₛ′ (from-Σ I C) (to-Σ I C) (λ _ → ≡.refl) (λ _ → ≡.refl)
module ConstantExponentiation {i s p} {I : Set i} (C : Container s p) where
From 2dc1cd13f25d20c5fc808839aeccc3c094237158 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 25 Feb 2024 09:40:16 +0000
Subject: [PATCH 2/2] resolve merge conflict in favour of #2293
---
src/Data/Container/Combinator/Properties.agda | 24 +++++++++----------
1 file changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/Data/Container/Combinator/Properties.agda b/src/Data/Container/Combinator/Properties.agda
index 188bc398c6..13823bef75 100644
--- a/src/Data/Container/Combinator/Properties.agda
+++ b/src/Data/Container/Combinator/Properties.agda
@@ -18,7 +18,7 @@ open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_])
open import Function.Base as F using (_∘′_)
open import Function.Bundles
open import Level using (_⊔_; lower)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong)
-- I have proved some of the correctness statements under the
-- assumption of functional extensionality. I could have reformulated
@@ -27,35 +27,35 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
module Identity where
correct : ∀ {s p x} {X : Set x} → ⟦ id {s} {p} ⟧ X ↔ F.id X
- correct {X = X} = mk↔ₛ′ from-id to-id (λ _ → ≡.refl) (λ _ → ≡.refl)
+ correct {X = X} = mk↔ₛ′ from-id to-id (λ _ → refl) (λ _ → refl)
module Constant (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′) where
correct : ∀ {x p y} (X : Set x) {Y : Set y} → ⟦ const {x} {p ⊔ y} X ⟧ Y ↔ F.const X Y
- correct {x} {y} X {Y} = mk↔ₛ′ (from-const X) (to-const X) (λ _ → ≡.refl) from∘to
+ correct {x} {y} X {Y} = mk↔ₛ′ (from-const X) (to-const X) (λ _ → refl) from∘to
where
from∘to : (x : ⟦ const X ⟧ Y) → to-const X (proj₁ x) ≡ x
- from∘to xs = ≡.cong (proj₁ xs ,_) (ext (λ x → ⊥-elim (lower x)))
+ from∘to xs = cong (proj₁ xs ,_) (ext (λ x → ⊥-elim (lower x)))
module Composition {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
correct : ∀ {x} {X : Set x} → ⟦ C₁ ∘ C₂ ⟧ X ↔ (⟦ C₁ ⟧ F.∘ ⟦ C₂ ⟧) X
- correct {X = X} = mk↔ₛ′ (from-∘ C₁ C₂) (to-∘ C₁ C₂) (λ _ → ≡.refl) (λ _ → ≡.refl)
+ correct {X = X} = mk↔ₛ′ (from-∘ C₁ C₂) (to-∘ C₁ C₂) (λ _ → refl) (λ _ → refl)
module Product (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′)
{s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
correct : ∀ {x} {X : Set x} → ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X P.× ⟦ C₂ ⟧ X)
- correct {X = X} = mk↔ₛ′ (from-× C₁ C₂) (to-× C₁ C₂) (λ _ → ≡.refl) from∘to
+ correct {X = X} = mk↔ₛ′ (from-× C₁ C₂) (to-× C₁ C₂) (λ _ → refl) from∘to
where
from∘to : (to-× C₁ C₂) F.∘ (from-× C₁ C₂) ≗ F.id
from∘to (s , f) =
- ≡.cong (s ,_) (ext [ (λ _ → ≡.refl) , (λ _ → ≡.refl) ])
+ cong (s ,_) (ext [ (λ _ → refl) , (λ _ → refl) ])
module IndexedProduct {i s p} {I : Set i} (Cᵢ : I → Container s p) where
correct : ∀ {x} {X : Set x} → ⟦ Π I Cᵢ ⟧ X ↔ (∀ i → ⟦ Cᵢ i ⟧ X)
- correct {X = X} = mk↔ₛ′ (from-Π I Cᵢ) (to-Π I Cᵢ) (λ _ → ≡.refl) (λ _ → ≡.refl)
+ correct {X = X} = mk↔ₛ′ (from-Π I Cᵢ) (to-Π I Cᵢ) (λ _ → refl) (λ _ → refl)
module Sum {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where
@@ -63,16 +63,16 @@ module Sum {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) whe
correct {X = X} = mk↔ₛ′ (from-⊎ C₁ C₂) (to-⊎ C₁ C₂) to∘from from∘to
where
from∘to : (to-⊎ C₁ C₂) F.∘ (from-⊎ C₁ C₂) ≗ F.id
- from∘to (inj₁ s₁ , f) = ≡.refl
- from∘to (inj₂ s₂ , f) = ≡.refl
+ from∘to (inj₁ s₁ , f) = refl
+ from∘to (inj₂ s₂ , f) = refl
to∘from : (from-⊎ C₁ C₂) F.∘ (to-⊎ C₁ C₂) ≗ F.id
- to∘from = [ (λ _ → ≡.refl) , (λ _ → ≡.refl) ]
+ to∘from = [ (λ _ → refl) , (λ _ → refl) ]
module IndexedSum {i s p} {I : Set i} (C : I → Container s p) where
correct : ∀ {x} {X : Set x} → ⟦ Σ I C ⟧ X ↔ (∃ λ i → ⟦ C i ⟧ X)
- correct {X = X} = mk↔ₛ′ (from-Σ I C) (to-Σ I C) (λ _ → ≡.refl) (λ _ → ≡.refl)
+ correct {X = X} = mk↔ₛ′ (from-Σ I C) (to-Σ I C) (λ _ → refl) (λ _ → refl)
module ConstantExponentiation {i s p} {I : Set i} (C : Container s p) where