------------------------------------------------------------------------
-- The Agda standard library
--
-- 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 using
  ( _⊆_; _∷_; _∷ʳ_
  ; 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 SPSlice public using ( IsCospan; Cospan )

open IsCospan
open Cospan

module _
  {x : A} {xs ys zs : List A} {τ₁ : xs  zs} {τ₂ : ys  zs}
  (d : Disjoint τ₁ τ₂) (c : IsCospan (⊆-disjoint-union d)) where

  ∷ₙ-cospan : IsCospan (⊆-disjoint-union (x ∷ₙ d))
  ∷ₙ-cospan = record
    { tri₁ = cong (x ∷ʳ_) (c .tri₁)
    ; tri₂ = cong (x ∷ʳ_) (c .tri₂)
    }

  ∷ₗ-cospan : IsCospan (⊆-disjoint-union (refl {x = x} ∷ₗ d))
  ∷ₗ-cospan = record
    { tri₁ = cong (refl ∷_) (c .tri₁)
    ; tri₂ = cong (x   ∷ʳ_) (c .tri₂)
    }

  ∷ᵣ-cospan : IsCospan (⊆-disjoint-union (refl {x = x} ∷ᵣ d))
  ∷ᵣ-cospan = record
    { tri₁ = cong (x   ∷ʳ_) (c .tri₁)
    ; tri₂ = cong (refl ∷_) (c .tri₂)
    }

⊆-disjoint-union-is-cospan :  {xs ys zs : List A} {τ₁ : xs  zs} {τ₂ : ys  zs} 
  (d : Disjoint τ₁ τ₂)  IsCospan (⊆-disjoint-union 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 {τ₁ = τ₁} {τ₂ = τ₂} _ = ⊆-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."
#-}