    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Syntax for the building blocks of equational reasoning modules
    ------------------------------------------------------------------------

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

    -- List of `Reasoning` modules that do not use this framework and so
    -- need to be updated manually if the syntax changes.
    --
    --   Data/Vec/Relation/Binary/Equality/Cast
    --   Relation/Binary/HeterogeneousEquality
    --   Effect/Monad/Partiality
    --   Effect/Monad/Partiality/All
    --   Codata/Guarded/Stream/Relation/Binary/Pointwise
    --   Function/Reasoning

    module Relation.Binary.Reasoning.Syntax where

    open import Level using (Level; _⊔_; suc)
    open import Relation.Nullary.Decidable.Core
      using (Dec; True; toWitness)
    open import Relation.Nullary.Negation.Core using (contradiction)
    open import Relation.Binary.Core using (Rel; REL; _⇒_)
    open import Relation.Binary.Definitions
      using (_Respectsʳ_; Asymmetric; Trans; Sym; Reflexive)
    open import Relation.Binary.PropositionalEquality.Core as ≡
      using (_≡_)

    private
      variable
        a ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
        A B C : Set a
        x y z : A

    ------------------------------------------------------------------------
    -- Syntax for beginning a reasoning chain
    ------------------------------------------------------------------------

    ------------------------------------------------------------------------
    -- Basic begin syntax

    module begin-syntax
      (R : REL A B ℓ₁)
      {S : REL A B ℓ₂}
      (reflexive : R ⇒ S)
      where

      infix 1 begin_

      begin_ : R x y → S x y
      begin_ = reflexive

    ------------------------------------------------------------------------
    -- Begin subrelation syntax

    -- Sometimes we want to support sub-relations with the
    -- same reasoning operators as the main relations (e.g. perform equality
    -- proofs with non-strict reasoning operators). This record bundles all
    -- the parts needed to extract the sub-relation proofs.
    record SubRelation {A : Set a} (R : Rel A ℓ₁) ℓ₂ ℓ₃ : Set (a ⊔ ℓ₁ ⊔ suc ℓ₂ ⊔ suc ℓ₃) where
      field
        S : Rel A ℓ₂
        IsS : R x y → Set ℓ₃
        IsS? : ∀ (xRy : R x y) → Dec (IsS xRy)
        extract : ∀ {xRy : R x y} → IsS xRy → S x y

    module begin-subrelation-syntax
      (R : Rel A ℓ₁)
      (sub : SubRelation R ℓ₂ ℓ₃)
      where
      open SubRelation sub

      infix 1 begin_

      begin_ : ∀ {x y} (xRy : R x y) → {s : True (IsS? xRy)} → S x y
      begin_ r {s} = extract (toWitness s)

    -- Begin equality syntax
    module begin-equality-syntax
      (R : Rel A ℓ₁)
      (sub : SubRelation R ℓ₂ ℓ₃) where

      open begin-subrelation-syntax R sub public
        renaming (begin_ to begin-equality_)

    -- Begin apartness syntax
    module begin-apartness-syntax
      (R : Rel A ℓ₁)
      (sub : SubRelation R ℓ₂ ℓ₃) where

      open begin-subrelation-syntax R sub public
        renaming (begin_ to begin-apartness_)

    -- Begin strict syntax
    module begin-strict-syntax
      (R : Rel A ℓ₁)
      (sub : SubRelation R ℓ₂ ℓ₃) where

      open begin-subrelation-syntax R sub public
        renaming (begin_ to begin-strict_)

    ------------------------------------------------------------------------
    -- Begin membership syntax

    module begin-membership-syntax
      (R : Rel A ℓ₁)
      (_∈_ : REL B A ℓ₂)
      (resp : _∈_ Respectsʳ R) where

      infix  1 step-∈

      step-∈ : ∀ (x : B) {xs ys} → R xs ys → x ∈ xs → x ∈ ys
      step-∈ x = resp

      syntax step-∈ x  xs⊆ys x∈xs  = x ∈⟨ x∈xs ⟩ xs⊆ys

    ------------------------------------------------------------------------
    -- Begin contradiction syntax

    -- Used with asymmetric subrelations to derive a contradiction from a
    -- proof that an element is related to itself.
    module begin-contradiction-syntax
      (R : Rel A ℓ₁)
      (sub : SubRelation R ℓ₂ ℓ₃)
      (asym : Asymmetric (SubRelation.S sub))
      where

      open SubRelation sub

      infix 1 begin-contradiction_

      begin-contradiction_ : ∀ (xRx : R x x) {s : True (IsS? xRx)} →
                             ∀ {b} {B : Set b} → B
      begin-contradiction_ {x} r {s} = contradiction x<x (asym x<x)
        where
        x<x : S x x
        x<x = extract (toWitness s)

    ------------------------------------------------------------------------
    -- Syntax for continuing a chain of reasoning steps
    ------------------------------------------------------------------------

    -- Note that the arguments to the `step`s are not provided in their
    -- "natural" order and syntax declarations are later used to re-order
    -- them. This is because the `step` ordering allows the type-checker to
    -- better infer the middle argument `y` from the `_IsRelatedTo_`
    -- argument (see issue 622).
    --
    -- This has two practical benefits. First it speeds up type-checking by
    -- approximately a factor of 5. Secondly it allows the combinators to be
    -- used with macros that use reflection, e.g. `Tactic.RingSolver`, where
    -- they need to be able to extract `y` using reflection.

    ------------------------------------------------------------------------
    -- Syntax for unidirectional relations

    -- See https://github.com/agda/agda-stdlib/issues/2150 for a possible
    -- simplification.

    module _
      {R : REL A B ℓ₂}
      (S : REL B C ℓ₁)
      (T : REL A C ℓ₃)
      (step : Trans R S T)
      where

      forward : ∀ (x : A) {y z} → S y z → R x y → T x z
      forward x yRz x∼y = step {x} x∼y yRz

      -- Arbitrary relation syntax
      module ∼-syntax where
        infixr 2 step-∼
        step-∼ = forward
        syntax step-∼ x yRz x∼y = x ∼⟨ x∼y ⟩ yRz

      -- Preorder syntax
      module ≲-syntax where
        infixr 2 step-≲
        step-≲ = forward
        syntax step-≲ x yRz x≲y = x ≲⟨ x≲y ⟩ yRz

      -- Partial order syntax
      module ≤-syntax where
        infixr 2 step-≤
        step-≤ = forward
        syntax step-≤ x yRz x≤y = x ≤⟨ x≤y ⟩ yRz

      -- Strict partial order syntax
      module <-syntax where
        infixr 2 step-<
        step-< = forward
        syntax step-< x yRz x<y = x <⟨ x<y ⟩ yRz

      -- Subset order syntax
      module ⊆-syntax where
        infixr 2 step-⊆
        step-⊆ = forward
        syntax step-⊆ x yRz x⊆y = x ⊆⟨ x⊆y ⟩ yRz

      -- Strict subset order syntax
      module ⊂-syntax where
        infixr 2 step-⊂
        step-⊂ = forward
        syntax step-⊂ x yRz x⊂y = x ⊂⟨ x⊂y ⟩ yRz

      -- Square subset order syntax
      module ⊑-syntax where
        infixr 2 step-⊑
        step-⊑ = forward
        syntax step-⊑ x yRz x⊑y = x ⊑⟨ x⊑y ⟩ yRz

      -- Strict square subset order syntax
      module ⊏-syntax where
        infixr 2 step-⊏
        step-⊏ = forward
        syntax step-⊏ x yRz x⊏y = x ⊏⟨ x⊏y ⟩ yRz

      -- Divisibility syntax
      module ∣-syntax where
        infixr 2 step-∣
        step-∣ = forward
        syntax step-∣ x yRz x∣y = x ∣⟨ x∣y ⟩ yRz

      -- Single-step syntax
      module ⟶-syntax where
        infixr 2 step-⟶
        step-⟶ = forward
        syntax step-⟶ x yRz x∣y = x ⟶⟨ x∣y ⟩ yRz

      -- Multi-step syntax
      module ⟶*-syntax where
        infixr 2 step-⟶*
        step-⟶* = forward
        syntax step-⟶* x yRz x∣y = x ⟶*⟨ x∣y ⟩ yRz

    ------------------------------------------------------------------------
    -- Syntax for bidirectional relations

      module _
        {U : REL B A ℓ₄}
        (sym : Sym U R)
        where

        backward : ∀ x {y z} → S y z → U y x → T x z
        backward x yRz x≈y = forward x yRz (sym x≈y)

        -- Setoid equality syntax
        module ≈-syntax where
          infixr 2 step-≈-⟩ step-≈-⟨
          step-≈-⟩ = forward
          step-≈-⟨ = backward
          syntax step-≈-⟩ x yRz x≈y = x ≈⟨ x≈y ⟩ yRz
          syntax step-≈-⟨ x yRz y≈x = x ≈⟨ y≈x ⟨ yRz

          -- Deprecated
          infixr 2 step-≈ step-≈˘
          step-≈ = step-≈-⟩
          {-# WARNING_ON_USAGE step-≈
          "Warning: step-≈ was deprecated in v2.0.
          Please use step-≈-⟩ instead."
          #-}
          step-≈˘ = step-≈-⟨
          {-# WARNING_ON_USAGE step-≈˘
          "Warning: step-≈˘ and _≈˘⟨_⟩_ was deprecated in v2.0.
          Please use step-≈-⟨ and _≈⟨_⟨_ instead."
          #-}
          syntax step-≈˘ x yRz y≈x = x ≈˘⟨ y≈x ⟩ yRz

        -- Container equality syntax
        module ≋-syntax where
          infixr 2 step-≋-⟩ step-≋-⟨
          step-≋-⟩ = forward
          step-≋-⟨ = backward
          syntax step-≋-⟩ x yRz x≋y = x ≋⟨ x≋y ⟩ yRz
          syntax step-≋-⟨ x yRz y≋x = x ≋⟨ y≋x ⟨ yRz

          -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
          infixr 2 step-≋ step-≋˘
          step-≋ = step-≋-⟩
          {-# WARNING_ON_USAGE step-≋
          "Warning: step-≋ was deprecated in v2.0.
          Please use step-≋-⟩ instead."
          #-}
          step-≋˘ = step-≋-⟨
          {-# WARNING_ON_USAGE step-≋˘
          "Warning: step-≋˘ and _≋˘⟨_⟩_ was deprecated in v2.0.
          Please use step-≋-⟨ and _≋⟨_⟨_ instead."
          #-}
          syntax step-≋˘ x yRz y≋x = x ≋˘⟨ y≋x ⟩ yRz

        -- Other equality syntax
        module ≃-syntax where
          infixr 2 step-≃-⟩ step-≃-⟨
          step-≃-⟩ = forward
          step-≃-⟨ = backward
          syntax step-≃-⟩ x yRz x≃y = x ≃⟨ x≃y ⟩ yRz
          syntax step-≃-⟨ x yRz y≃x = x ≃⟨ y≃x ⟨ yRz

        -- Apartness relation syntax
        module #-syntax where
          infixr 2 step-#-⟩ step-#-⟨
          step-#-⟩ = forward
          step-#-⟨ = backward
          syntax step-#-⟩ x yRz x#y = x #⟨ x#y ⟩ yRz
          syntax step-#-⟨ x yRz y#x = x #⟨ y#x ⟨ yRz

          -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
          infixr 2 step-# step-#˘
          step-# = step-#-⟩
          {-# WARNING_ON_USAGE step-#
          "Warning: step-# was deprecated in v2.0.
          Please use step-#-⟩ instead."
          #-}
          step-#˘ = step-#-⟨
          {-# WARNING_ON_USAGE step-#˘
          "Warning: step-#˘ and _#˘⟨_⟩_ was deprecated in v2.0.
          Please use step-#-⟨ and _#⟨_⟨_ instead."
          #-}
          syntax step-#˘ x yRz y#x = x #˘⟨ y#x ⟩ yRz

        -- Bijection syntax
        module ⤖-syntax where
          infixr 2 step-⤖ step-⬻
          step-⤖ = forward
          step-⬻ = backward
          syntax step-⤖ x yRz x⤖y = x ⤖⟨ x⤖y ⟩ yRz
          syntax step-⬻ x yRz y⤖x = x ⬻⟨ y⤖x ⟩ yRz

        -- Inverse syntax
        module ↔-syntax where
          infixr 2 step-↔-⟩ step-↔-⟨
          step-↔-⟩ = forward
          step-↔-⟨ = backward
          syntax step-↔-⟩ x yRz x↔y = x ↔⟨ x↔y ⟩ yRz
          syntax step-↔-⟨ x yRz y↔x = x ↔⟨ y↔x ⟨ yRz

        -- Inverse syntax
        module ↭-syntax where
          infixr 2 step-↭-⟩ step-↭-⟨
          step-↭-⟩ = forward
          step-↭-⟨ = backward
          syntax step-↭-⟩ x yRz x↭y = x ↭⟨ x↭y ⟩ yRz
          syntax step-↭-⟨ x yRz y↭x = x ↭⟨ y↭x ⟨ yRz

          -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
          infixr 2 step-↭ step-↭˘
          step-↭ = forward
          {-# WARNING_ON_USAGE step-↭
          "Warning: step-↭ was deprecated in v2.0.
          Please use step-↭-⟩ instead."
          #-}
          step-↭˘ = backward
          {-# WARNING_ON_USAGE step-↭˘
          "Warning: step-↭˘ and _↭˘⟨_⟩_ was deprecated in v2.0.
          Please use step-↭-⟨ and _↭⟨_⟨_ instead."
          #-}
          syntax step-↭˘ x yRz y↭x = x ↭˘⟨ y↭x ⟩ yRz

    ------------------------------------------------------------------------
    -- Propositional equality

    -- Crucially often the step function cannot just be `subst` or pattern
    -- match on `refl` as we often want to compute which constructor the
    -- relation begins with, in order for the implicit subrelation
    -- arguments to resolve. See `≡-noncomputable-syntax` below if this
    -- is not required.
    module ≡-syntax
      (R : REL A B ℓ₁)
      (step : Trans _≡_ R R)
      where

      infixr 2 step-≡-⟩  step-≡-∣ step-≡-⟨
      step-≡-⟩ = forward R R step

      step-≡-∣ : ∀ x {y} → R x y → R x y
      step-≡-∣ x xRy = xRy

      step-≡-⟨ = backward R R step ≡.sym

      syntax step-≡-⟩ x yRz x≡y = x ≡⟨ x≡y ⟩ yRz
      syntax step-≡-∣ x xRy     = x ≡⟨⟩ xRy
      syntax step-≡-⟨ x yRz y≡x = x ≡⟨ y≡x ⟨ yRz

      -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
      infixr 2 step-≡ step-≡˘
      step-≡ = step-≡-⟩
      {-# WARNING_ON_USAGE step-≡
      "Warning: step-≡ was deprecated in v2.0.
      Please use step-≡-⟩ instead."
      #-}
      step-≡˘ = step-≡-⟨
      {-# WARNING_ON_USAGE step-≡˘
      "Warning: step-≡˘ and _≡˘⟨_⟩_ was deprecated in v2.0.
      Please use step-≡-⟨ and _≡⟨_⟨_ instead."
      #-}
      syntax step-≡˘ x yRz y≡x = x ≡˘⟨ y≡x ⟩ yRz

    -- Unlike ≡-syntax above, chains of reasoning using this syntax will not
    -- reduce when proofs of propositional equality which are not definitionally
    -- equal to `refl` are passed.
    module ≡-noncomputing-syntax (R : REL A B ℓ₁) where

      private
        step : Trans _≡_ R R
        step ≡.refl xRy = xRy

      open ≡-syntax R step public

    ------------------------------------------------------------------------
    -- Syntax for ending a chain of reasoning
    ------------------------------------------------------------------------

    module end-syntax
      (R : Rel A ℓ₁)
      (reflexive : Reflexive R)
      where

      infix 3 _∎

      _∎ : ∀ x → R x x
      x ∎ = reflexive