diff --git a/CHANGELOG.md b/CHANGELOG.md index 186fe9d051..2b9d357511 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ Version 2.1-dev =============== -The library has been tested using Agda 2.6.4 and 2.6.4.1. +The library has been tested using Agda 2.6.4, 2.6.4.1, and 2.6.4.3. Highlights ---------- @@ -33,6 +33,9 @@ Other major improvements Deprecated modules ------------------ +* `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of + `Data.List.Relation.Binary.Sublist.Propositional.Slice`. + Deprecated names ---------------- @@ -80,6 +83,12 @@ New modules Algebra.Module.Construct.Idealization ``` +* `Data.List.Relation.Binary.Sublist.Propositional.Slice` + replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*) + and adding new functions: + - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*) + - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*) + * `Data.Vec.Functional.Relation.Binary.Permutation`, defining: ```agda _↭_ : IRel (Vector A) _ @@ -170,7 +179,7 @@ Additions to existing modules quasigroup : Quasigroup _ _ isLoop : IsLoop _∙_ _\\_ _//_ ε loop : Loop _ _ - + \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ \\-leftDivides : LeftDivides _∙_ _\\_ @@ -189,7 +198,7 @@ Additions to existing modules identityʳ-unique : x ∙ y ≈ x → y ≈ ε identity-unique : Identity x _∙_ → x ≈ ε ``` - + * In `Algebra.Construct.Terminal`: ```agda rawNearSemiring : RawNearSemiring c ℓ @@ -218,7 +227,7 @@ Additions to existing modules _\\_ : Op₂ A x \\ y = (x ⁻¹) ∙ y ``` - + * In `Data.Container.Indexed.Core`: ```agda Subtrees o c = (r : Response c) → X (next c r) @@ -301,6 +310,11 @@ Additions to existing modules pointwise⊆any : Pointwise R (just x) ⊆ Any (R x) ``` +* In `Data.List.Relation.Binary.Sublist.Setoid`: + ```agda + ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ + ``` + * In `Data.Nat.Divisibility`: ```agda quotient≢0 : m ∣ n → .{{NonZero n}} → NonZero quotient @@ -327,7 +341,7 @@ Additions to existing modules pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n ``` - + * Added new proofs to `Data.Nat.Primality`: ```agda rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda index a6a33cc43a..97557891a9 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda @@ -1,7 +1,9 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Sublist-related properties +-- This module is DEPRECATED. +-- Please use `Data.List.Relation.Binary.Sublist.Propositional.Slice` +-- instead. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -9,26 +11,23 @@ module Data.List.Relation.Binary.Sublist.Propositional.Disjoint {a} {A : Set a} where +{-# WARNING_ON_IMPORT +"Data.List.Relation.Binary.Sublist.Propositional.Disjoint was deprecated in v2.1. +Use Data.List.Relation.Binary.Sublist.Propositional.Slice instead." +#-} + open import Data.List.Base using (List) -open import Data.List.Relation.Binary.Sublist.Propositional +open import Data.List.Relation.Binary.Sublist.Propositional using + ( _⊆_; _∷_; _∷ʳ_ + ; Disjoint; ⊆-disjoint-union; _∷ₙ_; _∷ₗ_; _∷ᵣ_ + ) +import Data.List.Relation.Binary.Sublist.Propositional.Slice as SPSlice open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) ------------------------------------------------------------------------- --- A Union where the triangles commute is a --- Cospan in the slice category (_ ⊆ zs). - -record IsCospan {xs ys zs : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} (u : UpperBound τ₁ τ₂) : Set a where - field - tri₁ : ⊆-trans (UpperBound.inj₁ u) (UpperBound.sub u) ≡ τ₁ - tri₂ : ⊆-trans (UpperBound.inj₂ u) (UpperBound.sub u) ≡ τ₂ +open SPSlice using (⊆-upper-bound-is-cospan; ⊆-upper-bound-cospan) -record Cospan {xs ys zs : List A} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) : Set a where - field - upperBound : UpperBound τ₁ τ₂ - isCospan : IsCospan upperBound - - open UpperBound upperBound public - open IsCospan isCospan public +-- For backward compatibility reexport these: +open SPSlice public using ( IsCospan; Cospan ) open IsCospan open Cospan @@ -57,14 +56,18 @@ module _ ⊆-disjoint-union-is-cospan : ∀ {xs ys zs : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} → (d : Disjoint τ₁ τ₂) → IsCospan (⊆-disjoint-union d) -⊆-disjoint-union-is-cospan [] = record { tri₁ = refl ; tri₂ = refl } -⊆-disjoint-union-is-cospan (x ∷ₙ d) = ∷ₙ-cospan d (⊆-disjoint-union-is-cospan d) -⊆-disjoint-union-is-cospan (refl ∷ₗ d) = ∷ₗ-cospan d (⊆-disjoint-union-is-cospan d) -⊆-disjoint-union-is-cospan (refl ∷ᵣ d) = ∷ᵣ-cospan d (⊆-disjoint-union-is-cospan d) +⊆-disjoint-union-is-cospan {τ₁ = τ₁} {τ₂ = τ₂} _ = ⊆-upper-bound-is-cospan τ₁ τ₂ ⊆-disjoint-union-cospan : ∀ {xs ys zs : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} → Disjoint τ₁ τ₂ → Cospan τ₁ τ₂ -⊆-disjoint-union-cospan d = record - { upperBound = ⊆-disjoint-union d - ; isCospan = ⊆-disjoint-union-is-cospan d - } +⊆-disjoint-union-cospan {τ₁ = τ₁} {τ₂ = τ₂} _ = ⊆-upper-bound-cospan τ₁ τ₂ + +{-# WARNING_ON_USAGE ⊆-disjoint-union-is-cospan +"Warning: ⊆-disjoint-union-is-cospan was deprecated in v2.1. +Please use `⊆-upper-bound-is-cospan` from `Data.List.Relation.Binary.Sublist.Propositional.Slice` instead." +#-} + +{-# WARNING_ON_USAGE ⊆-disjoint-union-cospan +"Warning: ⊆-disjoint-union-cospan was deprecated in v2.1. +Please use `⊆-upper-bound-cospan` from `Data.List.Relation.Binary.Sublist.Propositional.Slice` instead." +#-} diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda new file mode 100644 index 0000000000..949fded0ae --- /dev/null +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda @@ -0,0 +1,79 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Slices in the propositional sublist category. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.List.Relation.Binary.Sublist.Propositional.Slice + {a} {A : Set a} where + +open import Data.List.Base using (List) +open import Data.List.Relation.Binary.Sublist.Propositional +open import Relation.Binary.PropositionalEquality + +------------------------------------------------------------------------ +-- A Union where the triangles commute is a +-- Cospan in the slice category (_ ⊆ zs). + +record IsCospan {xs ys zs : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} (u : UpperBound τ₁ τ₂) : Set a where + field + tri₁ : ⊆-trans (UpperBound.inj₁ u) (UpperBound.sub u) ≡ τ₁ + tri₂ : ⊆-trans (UpperBound.inj₂ u) (UpperBound.sub u) ≡ τ₂ + +record Cospan {xs ys zs : List A} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) : Set a where + field + upperBound : UpperBound τ₁ τ₂ + isCospan : IsCospan upperBound + + open UpperBound upperBound public + open IsCospan isCospan public + +open IsCospan +open Cospan + +module _ + {x : A} {xs ys zs : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} + {u : UpperBound τ₁ τ₂} (c : IsCospan u) where + open UpperBound u + open IsCospan c + + ∷ₙ-cospan : IsCospan (∷ₙ-ub u) + ∷ₙ-cospan = record + { tri₁ = cong (x ∷ʳ_) (c .tri₁) + ; tri₂ = cong (x ∷ʳ_) (c .tri₂) + } + + ∷ₗ-cospan : IsCospan (refl {x = x} ∷ₗ-ub u) + ∷ₗ-cospan = record + { tri₁ = cong (refl ∷_) (c .tri₁) + ; tri₂ = cong (x ∷ʳ_) (c .tri₂) + } + + ∷ᵣ-cospan : IsCospan (refl {x = x} ∷ᵣ-ub u) + ∷ᵣ-cospan = record + { tri₁ = cong (x ∷ʳ_) (c .tri₁) + ; tri₂ = cong (refl ∷_) (c .tri₂) + } + + ∷-cospan : IsCospan (refl {x = x} , refl {x = x} ∷-ub u) + ∷-cospan = record + { tri₁ = cong (refl ∷_) (c .tri₁) + ; tri₂ = cong (refl ∷_) (c .tri₂) + } + +⊆-upper-bound-is-cospan : ∀ {xs ys zs : List A} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → + IsCospan (⊆-upper-bound τ₁ τ₂) +⊆-upper-bound-is-cospan [] [] = record { tri₁ = refl ; tri₂ = refl } +⊆-upper-bound-is-cospan (z ∷ʳ τ₁) (.z ∷ʳ τ₂) = ∷ₙ-cospan (⊆-upper-bound-is-cospan τ₁ τ₂) +⊆-upper-bound-is-cospan (z ∷ʳ τ₁) (refl ∷ τ₂) = ∷ᵣ-cospan (⊆-upper-bound-is-cospan τ₁ τ₂) +⊆-upper-bound-is-cospan (refl ∷ τ₁) (z ∷ʳ τ₂) = ∷ₗ-cospan (⊆-upper-bound-is-cospan τ₁ τ₂) +⊆-upper-bound-is-cospan (refl ∷ τ₁) (refl ∷ τ₂) = ∷-cospan (⊆-upper-bound-is-cospan τ₁ τ₂) + +⊆-upper-bound-cospan : ∀ {xs ys zs : List A} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → + Cospan τ₁ τ₂ +⊆-upper-bound-cospan τ₁ τ₂ = record + { upperBound = ⊆-upper-bound τ₁ τ₂ + ; isCospan = ⊆-upper-bound-is-cospan τ₁ τ₂ + } diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid.agda b/src/Data/List/Relation/Binary/Sublist/Setoid.agda index 83a16444d0..2fc0373d67 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid.agda @@ -162,7 +162,7 @@ record RawPushout {xs ys zs : List A} (τ : xs ⊆ ys) (σ : xs ⊆ zs) : Set (c leg₁ : ys ⊆ upperBound leg₂ : zs ⊆ upperBound -open RawPushout +open RawPushout using (leg₁; leg₂) ------------------------------------------------------------------------ -- Extending corners of a raw pushout square @@ -211,13 +211,25 @@ z ∷ʳ₂ rpo = record ⊆-joinˡ : ∀ {xs ys zs : List A} → (τ : xs ⊆ ys) (σ : xs ⊆ zs) → ∃ λ us → xs ⊆ us -⊆-joinˡ τ σ = upperBound rpo , ⊆-trans τ (leg₁ rpo) +⊆-joinˡ τ σ = RawPushout.upperBound rpo , ⊆-trans τ (leg₁ rpo) where rpo = ⊆-pushoutˡ τ σ ------------------------------------------------------------------------ -- Upper bound of two sublists xs,ys ⊆ zs +-- +-- Two sublists τ : xs ⊆ zs and σ : ys ⊆ zs +-- can be joined in a unique way if τ and σ are respected. +-- +-- For instance, if τ : [x] ⊆ [x,y,x] and σ : [y] ⊆ [x,y,x] +-- then the union will be [x,y] or [y,x], depending on whether +-- τ picks the first x or the second one. +-- +-- NB: If the content of τ and σ were ignored then the union would not +-- be unique. Expressing uniqueness would require a notion of equality +-- of sublist proofs, which we do not (yet) have for the setoid case +-- (however, for the propositional case). record UpperBound {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) : Set (c ⊔ ℓ) where field @@ -254,24 +266,26 @@ x≈y ∷ᵣ-ub u = record ; inj₂ = x≈y ∷ u .inj₂ } +_,_∷-ub_ : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x y z} → + (x≈z : x ≈ z) (y≈z : y ≈ z) → UpperBound τ σ → UpperBound (x≈z ∷ τ) (y≈z ∷ σ) +x≈z , y≈z ∷-ub u = record + { sub = refl ∷ u .sub + ; inj₁ = x≈z ∷ u .inj₁ + ; inj₂ = y≈z ∷ u .inj₂ + } + +⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ +⊆-upper-bound [] [] = record { sub = [] ; inj₁ = [] ; inj₂ = [] } +⊆-upper-bound (y ∷ʳ τ) (.y ∷ʳ σ) = ∷ₙ-ub (⊆-upper-bound τ σ) +⊆-upper-bound (y ∷ʳ τ) (x≈y ∷ σ) = x≈y ∷ᵣ-ub ⊆-upper-bound τ σ +⊆-upper-bound (x≈y ∷ τ) (y ∷ʳ σ) = x≈y ∷ₗ-ub ⊆-upper-bound τ σ +⊆-upper-bound (x≈z ∷ τ) (y≈z ∷ σ) = x≈z , y≈z ∷-ub ⊆-upper-bound τ σ + ------------------------------------------------------------------------ -- Disjoint union -- --- Two non-overlapping sublists τ : xs ⊆ zs and σ : ys ⊆ zs --- can be joined in a unique way if τ and σ are respected. --- --- For instance, if τ : [x] ⊆ [x,y,x] and σ : [y] ⊆ [x,y,x] --- then the union will be [x,y] or [y,x], depending on whether --- τ picks the first x or the second one. --- --- NB: If the content of τ and σ were ignored then the union would not --- be unique. Expressing uniqueness would require a notion of equality --- of sublist proofs, which we do not (yet) have for the setoid case --- (however, for the propositional case). +-- Upper bound of two non-overlapping sublists. ⊆-disjoint-union : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} → Disjoint τ σ → UpperBound τ σ -⊆-disjoint-union [] = record { sub = [] ; inj₁ = [] ; inj₂ = [] } -⊆-disjoint-union (x ∷ₙ d) = ∷ₙ-ub (⊆-disjoint-union d) -⊆-disjoint-union (x≈y ∷ₗ d) = x≈y ∷ₗ-ub (⊆-disjoint-union d) -⊆-disjoint-union (x≈y ∷ᵣ d) = x≈y ∷ᵣ-ub (⊆-disjoint-union d) +⊆-disjoint-union {τ = τ} {σ = σ} _ = ⊆-upper-bound τ σ diff --git a/standard-library.agda-lib b/standard-library.agda-lib index ba7ae571b9..cedacd1041 100644 --- a/standard-library.agda-lib +++ b/standard-library.agda-lib @@ -1,4 +1,5 @@ -name: standard-library-2.1 +name: standard-library-tbt include: src flags: --warning=noUnsupportedIndexedMatch +-- --type-based-termination