------------------------------------------------------------------------
-- The Agda standard library
--
-- Order properties of the subset relations _⊆_ and _⊂_
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Relation.Unary.Relation.Binary.Subset where

open import Level using (Level)
import Relation.Binary.Structures as BinaryStructures
open import Relation.Binary.Bundles
open import Relation.Unary
open import Relation.Unary.Properties
open import Relation.Unary.Relation.Binary.Equality using (≐-isEquivalence; ≐′-isEquivalence)

------------------------------------------------------------------------
-- Structures

module _ {a : Level} {A : Set a} {ℓ : Level} where

  open BinaryStructures {A = Pred A ℓ} _≐_

  ⊆-isPreorder : IsPreorder _⊆_
  ⊆-isPreorder = record
    { isEquivalence = ≐-isEquivalence
    ; reflexive = ⊆-reflexive
    ; trans = ⊆-trans
    }

  ⊆-isPartialOrder : IsPartialOrder _⊆_
  ⊆-isPartialOrder = record
    { isPreorder = ⊆-isPreorder
    ; antisym = ⊆-antisym
    }

  ⊂-isStrictPartialOrder : IsStrictPartialOrder _⊂_
  ⊂-isStrictPartialOrder = record
    { isEquivalence = ≐-isEquivalence
    ; irrefl = ⊂-irrefl
    ; trans = ⊂-trans
    ; <-resp-≈ = ⊂-resp-≐
    }

module _ {a : Level} {A : Set a} {ℓ : Level} where

  open BinaryStructures {A = Pred A ℓ} _≐′_

  ⊆′-isPreorder : IsPreorder _⊆′_
  ⊆′-isPreorder = record
    { isEquivalence = ≐′-isEquivalence
    ; reflexive = ⊆′-reflexive
    ; trans = ⊆′-trans
    }

  ⊆′-isPartialOrder : IsPartialOrder _⊆′_
  ⊆′-isPartialOrder = record
    { isPreorder = ⊆′-isPreorder
    ; antisym = ⊆′-antisym
    }

  ⊂′-isStrictPartialOrder : IsStrictPartialOrder _⊂′_
  ⊂′-isStrictPartialOrder = record
    { isEquivalence = ≐′-isEquivalence
    ; irrefl = ⊂′-irrefl
    ; trans = ⊂′-trans
    ; <-resp-≈ = ⊂′-resp-≐′
    }

------------------------------------------------------------------------
-- Bundles

module _ {a : Level} (A : Set a) (ℓ : Level) where

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = record
    { isPreorder = ⊆-isPreorder {A = A} {ℓ}
    }

  ⊆-poset : Poset _ _ _
  ⊆-poset = record
    { isPartialOrder = ⊆-isPartialOrder {A = A} {ℓ}
    }

  ⊂-strictPartialOrder : StrictPartialOrder _ _ _
  ⊂-strictPartialOrder = record
    { isStrictPartialOrder = ⊂-isStrictPartialOrder {A = A} {ℓ}
    }

  ⊆′-preorder : Preorder _ _ _
  ⊆′-preorder = record
    { isPreorder = ⊆′-isPreorder {A = A} {ℓ}
    }

  ⊆′-poset : Poset _ _ _
  ⊆′-poset = record
    { isPartialOrder = ⊆′-isPartialOrder {A = A} {ℓ}
    }

  ⊂′-strictPartialOrder : StrictPartialOrder _ _ _
  ⊂′-strictPartialOrder = record
    { isStrictPartialOrder = ⊂′-isStrictPartialOrder {A = A} {ℓ}
    }