Sublists: generalize disjoint-union-is-cospan to upper-bound-is-cospan (#2320)

* Sublists: generalize disjoint-union-is-cospan to upper-bound-is-cospan

The disjointness assumption is superfluous.

* Move sublist cospan stuff to new module SubList.Propositional.Slice

* CHANGELOG

Author: andreasabel

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

src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda

@@ -1,34 +1,33 @@
 ------------------------------------------------------------------------
 -- 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 #-}
 
 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."
+#-}

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 τ₁ τ₂
+  }

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 τ σ

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