{-# 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)
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."
#-}