    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Closures of a unary relation with respect to a binary one.
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Core using (Rel)

    module Relation.Unary.Closure.Base {a b} {A : Set a} (R : Rel A b) where

    open import Level using (_⊔_)
    open import Data.Product.Base using (Σ-syntax; _×_; _,_; -,_)
    open import Function.Base using (flip)
    open import Relation.Binary.Definitions using (Reflexive; Transitive)
    open import Relation.Unary using (Pred)

    ------------------------------------------------------------------------
    -- Definitions

    -- Box

    -- We start with the definition of □ ("box") which is named after the
    -- box modality in modal logic. `□ T x` states that all the elements one
    -- step away from `x` with respect to the relation R satisfy `T`.

    □ : ∀ {t} → Pred A t → Pred A (a ⊔ b ⊔ t)
    □ T x = ∀ {y} → R x y → T y

    -- Use cases of □ include:
    -- * The definition of the accessibility predicate corresponding to R:
    --   data Acc (x : A) : Set (a ⊔ b) where
    --     step : □ Acc x → Acc x

    -- * The characterization of stability under weakening: picking R to be
    --   `Data.List.Relation.Sublist.Inductive`, `∀ {Γ} → Tm Γ → □ T Γ`
    --   corresponds to the fact that we have a notion of weakening for `Tm`.

    -- Diamond

    -- We then have the definition of ◇ ("diamond") which is named after the
    -- diamond modality in modal logic. In modal logic, `◇ T x` states that
    -- there exists an element one step away from x with respect to the
    -- relation R that satisfies T. It is worth noting that the modal logic
    -- metaphor breaks down here: this only is a closure operator if the
    -- step we take is *backwards* with respect to R.

    ◇ : ∀ {t} → Pred A t → Pred A (a ⊔ b ⊔ t)
    ◇ T x = Σ[ support ∈ A ] (R support x × T support)

    -- Use cases of ◇ include:
    -- * The characterization of strengthening: picking R to be
    --   `Data.List.Relation.Sublist.Inductive`, `∀ {Γ} → Tm Γ → ◇ Tm Γ`
    --   is the type of a function strengthening a term to its support:
    --   all the unused variables are discarded early on by the `related`
    --   proof.
    -- Cf. Conor McBride's "Everybody's got to be somewhere" for a more
    -- detailed treatment of such an example.

    -- Closed

    -- Whenever we have a value in one context, we can get one in any
    -- related context.

    record Closed {t} (T : Pred A t) : Set (a ⊔ b ⊔ t) where
      field next : ∀ {x} → T x → □ T x

    ------------------------------------------------------------------------
    -- Basic functions relating □ and ◇

    module _ {t p} {T : Pred A t} {P : Pred A p} where

      curry : (∀ {x} → ◇ T x → P x) → (∀ {x} → T x → □ P x)
      curry f tx x∼y = f (-, x∼y , tx)

      uncurry : (∀ {x} → T x → □ P x) → (∀ {x} → ◇ T x → P x)
      uncurry f (_ , y∼x , ty) = f ty y∼x

    ------------------------------------------------------------------------
    -- Properties

    module □ {t} {T : Pred A t} where

      reindex : Transitive R → ∀ {x y} → R x y → □ T x → □ T y
      reindex trans x∼y □Tx y∼z = □Tx (trans x∼y y∼z)

      -- Provided that R is reflexive and Transitive, □ is a comonad
      map : ∀ {u} {U : Pred A u} {x} → (∀ {x} → T x → U x) → □ T x → □ U x
      map f □Tx x~y = f (□Tx x~y)

      extract : Reflexive R → ∀ {x} → □ T x → T x
      extract refl □Tx = □Tx refl

      duplicate : Transitive R → ∀ {x} → □ T x → □ (□ T) x
      duplicate trans □Tx x∼y y∼z = □Tx (trans x∼y y∼z)

      -- Provided that R is transitive, □ is a closure operator
      -- i.e. for any `T`, `□ T` is closed.
      closed : Transitive R → Closed (□ T)
      closed trans = record { next = duplicate trans }

    module ◇ {t} {T : Pred A t} where

      reindex : Transitive R → ∀ {x y} → R x y → ◇ T x → ◇ T y
      reindex trans x∼y (z , z∼x , tz) = z , trans z∼x x∼y , tz

      -- Provided that R is reflexive and Transitive, ◇ is a monad
      map : ∀ {u} {U : Pred A u} {x} → (∀ {x} → T x → U x) → ◇ T x → ◇ U x
      map f (y , y∼x , ty) = y , y∼x , f ty

      pure : Reflexive R → ∀ {x} → T x → ◇ T x
      pure refl tx = -, refl , tx

      join : Transitive R → ∀ {x} → ◇ (◇ T) x → ◇ T x
      join trans (_ , y∼x , _ , z∼y , tz) = _ , trans z∼y y∼x , tz

      -- Provided that R is transitive, ◇ is a closure operator
      -- i.e. for any `T`, `◇ T` is closed.
      closed : Transitive R → Closed (◇ T)
      closed trans = record { next = λ ◇Tx x∼y → reindex trans x∼y ◇Tx }

      run : Closed T → ∀ {x} → ◇ T x → T x
      run closed (_ , y∼x , ty) = Closed.next closed ty y∼x