------------------------------------------------------------------------
-- 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
 using (_⊆_; UpperBound; ⊆-trans; ∷ₙ-ub; _∷ʳ_; _∷ₗ-ub_; _∷_; _∷ᵣ-ub_;
        _,_∷-ub_; ⊆-upper-bound; [])
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) ≡ τ₂

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