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

Author: andreasabel

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

@@ -152,68 +152,3 @@ separateˡ (z  ∷ʳ τ₁) (z  ∷ʳ τ₂) = z   ∷ₙ-Sep separateˡ τ₁ 
 separateˡ (z  ∷ʳ τ₁) (y≡z ∷ τ₂) = y≡z ∷ᵣ-Sep separateˡ τ₁ τ₂
 separateˡ (x≡z ∷ τ₁) (z  ∷ʳ τ₂) = x≡z ∷ₗ-Sep separateˡ τ₁ τ₂
 separateˡ (x≡z ∷ τ₁) (y≡z ∷ τ₂) = ∷-Sepˡ x≡z y≡z (separateˡ τ₁ τ₂)
-
-------------------------------------------------------------------------
--- 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/Propositional/Disjoint.agda

@@ -2,7 +2,8 @@
 -- The Agda standard library
 --
 -- This module is DEPRECATED.
--- Please use `Data.List.Relation.Binary.Sublist.Propositional` instead.
+-- Please use `Data.List.Relation.Binary.Sublist.Propositional.Slice`
+-- instead.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -12,20 +13,21 @@ module Data.List.Relation.Binary.Sublist.Propositional.Disjoint
 
 {-# WARNING_ON_IMPORT
 "Data.List.Relation.Binary.Sublist.Propositional.Disjoint was deprecated in v2.1.
-Use Data.List.Relation.Binary.Sublist.Propositional instead."
+Use Data.List.Relation.Binary.Sublist.Propositional.Slice instead."
 #-}
 
 open import Data.List.Base using (List)
-import Data.List.Relation.Binary.Sublist.Propositional as SLP
-open SLP using
+open import Data.List.Relation.Binary.Sublist.Propositional using
   ( _⊆_; _∷_; _∷ʳ_
-  ; Disjoint; ⊆-disjoint-union
-  ; ⊆-upper-bound-is-cospan; ⊆-upper-bound-cospan; _∷ₙ_; _∷ₗ_; _∷ᵣ_
+  ; Disjoint; ⊆-disjoint-union; _∷ₙ_; _∷ₗ_; _∷ᵣ_
   )
+import Data.List.Relation.Binary.Sublist.Propositional.Slice as SPSlice
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
+open SPSlice using (⊆-upper-bound-is-cospan; ⊆-upper-bound-cospan)
+
 -- For backward compatibility reexport these:
-open SLP public using ( IsCospan; Cospan )
+open SPSlice public using ( IsCospan; Cospan )
 
 open IsCospan
 open Cospan
@@ -62,10 +64,10 @@ module _
 
 {-# 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` instead."
+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` instead."
+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 τ₁ τ₂
+  }