------------------------------------------------------------------------
-- A variant of Definition.Typed.Reasoning.Reduction with fewer
-- dependencies
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.Typed.Reasoning.Reduction.Primitive
  {β„“} {M : Set β„“}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  where

open import Definition.Typed R
open import Definition.Typed.RedSteps R
open import Definition.Untyped M

open import Tools.Function
import Tools.PropositionalEquality as PE

private variable
  A B t u v : Term _
  Ξ“         : Con Term _

------------------------------------------------------------------------
-- Combinators for left-to-right reductions

infix  -1 finally-β‡’* finally-β‡’
infixr -2 step-β‡’ step-β‡’* finally-β‡’*≑ finally-⇒≑

-- A single step.

step-β‡’ : βˆ€ t β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-β‡’ _ = flip _⇨_

syntax step-β‡’ t uβ‡’v tβ‡’u = t β‡’βŸ¨ tβ‡’u ⟩ uβ‡’v

{-# INLINE step-β‡’ #-}

-- Multiple steps.

step-β‡’* : βˆ€ t β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-β‡’* _ = flip _β‡¨βˆ·*_

syntax step-β‡’* t uβ‡’v tβ‡’u = t β‡’*⟨ tβ‡’u ⟩ uβ‡’v

{-# INLINE step-β‡’* #-}

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

finally-β‡’* : βˆ€ t u β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-⇒* _ _ t⇒u = t⇒u

syntax finally-β‡’* t u tβ‡’u = t β‡’*⟨ tβ‡’u ⟩∎ u ∎

{-# INLINE finally-β‡’* #-}

-- A variant of finally-β‡’*.

finally-β‡’ : βˆ€ t u β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-β‡’ _ _ tβ‡’u ⊒u = tβ‡’u ⇨ id ⊒u

syntax finally-β‡’ t u tβ‡’u ⊒u = t β‡’βŸ¨ tβ‡’u , ⊒u ⟩∎ u ∎

{-# INLINE finally-β‡’ #-}

-- A variant of finally-β‡’* that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∎⟨_βŸ©β‡’.

finally-β‡’*≑ : βˆ€ t β†’ u PE.≑ v β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
finally-β‡’*≑ _ PE.refl tβ‡’u = tβ‡’u

syntax finally-β‡’*≑ t u≑v tβ‡’u = t β‡’*⟨ tβ‡’u βŸ©βˆŽβ‰‘ u≑v

-- A variant of finally-β‡’*≑.

finally-⇒≑ : βˆ€ t β†’ u PE.≑ v β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
finally-⇒≑ _ PE.refl = finally-β‡’ _ _

syntax finally-⇒≑ t u≑v tβ‡’u = t β‡’βŸ¨ tβ‡’u βŸ©βˆŽβ‰‘ u≑v

------------------------------------------------------------------------
-- Combinators for right-to-left reductions

infix  -1 finally-⇐* finally-⇐
infixr -2 step-⇐ step-⇐* finally-⇐*≑ finally-⇐≑

opaque

  -- A single step.

  step-⇐ :
    βˆ€ v β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ u β‡’ v ∷ A β†’ Ξ“ ⊒ v ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
  step-⇐ _ tβ‡’u uβ‡’v ⊒v = tβ‡’u β‡¨βˆ·* (uβ‡’v ⇨ id ⊒v)

  syntax step-⇐ v tβ‡’u uβ‡’v ⊒v = v β‡βŸ¨ uβ‡’v , ⊒v ⟩ tβ‡’u

-- Multiple steps.

step-⇐* : βˆ€ v β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-⇐* _ = _β‡¨βˆ·*_

syntax step-⇐* v tβ‡’u uβ‡’v = v ⇐*⟨ uβ‡’v ⟩ tβ‡’u

{-# INLINE step-⇐* #-}

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

finally-⇐* : βˆ€ u t β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-⇐* _ _ tβ‡’u = tβ‡’u

syntax finally-⇐* u t tβ‡’u = u ⇐*⟨ tβ‡’u ⟩∎ t ∎

{-# INLINE finally-⇐* #-}

-- A variant of finally-⇐*.

finally-⇐ : βˆ€ u t β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-⇐ _ _ tβ‡’u ⊒u = tβ‡’u ⇨ id ⊒u

syntax finally-⇐ u t tβ‡’u ⊒u = u β‡βŸ¨ tβ‡’u , ⊒u ⟩∎ t ∎

{-# INLINE finally-⇐ #-}

-- A variant of finally-⇐* that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∎⟨_βŸ©β‡’.

finally-⇐*≑ : βˆ€ v β†’ u PE.≑ t β†’ Ξ“ ⊒ v β‡’* u ∷ A β†’ Ξ“ ⊒ v β‡’* t ∷ A
finally-⇐*≑ _ PE.refl vβ‡’u = vβ‡’u

syntax finally-⇐*≑ v u≑t vβ‡’u = v ⇐*⟨ vβ‡’u βŸ©βˆŽβ‰‘ u≑t

-- A variant of finally-⇐*≑.

finally-⇐≑ : βˆ€ v β†’ u PE.≑ t β†’ Ξ“ ⊒ v β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ v β‡’* t ∷ A
finally-⇐≑ _ PE.refl = finally-⇐ _ _

syntax finally-⇐≑ v u≑t vβ‡’u ⊒u = v β‡βŸ¨ vβ‡’u , ⊒u βŸ©βˆŽβ‰‘ u≑t

------------------------------------------------------------------------
-- Combinators for left-to-right or right-to-left reductions

infix  -1 _∎⟨_βŸ©β‡’
infixr -2 step-≑ step-β‰‘Λ˜ _β‰‘βŸ¨βŸ©β‡’_

-- A reasoning step that uses propositional equality.

step-≑ : βˆ€ t β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ t PE.≑ u β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-≑ _ uβ‡’v PE.refl = uβ‡’v

syntax step-≑ t uβ‡’v t≑u = t β‰‘βŸ¨ t≑u βŸ©β‡’ uβ‡’v

-- A reasoning step that uses propositional equality, combined with
-- symmetry.

step-β‰‘Λ˜ : βˆ€ t β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ u PE.≑ t β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-β‰‘Λ˜ _ uβ‡’v PE.refl = uβ‡’v

syntax step-β‰‘Λ˜ t uβ‡’v u≑t = t β‰‘Λ˜βŸ¨ u≑t βŸ©β‡’ uβ‡’v

-- A reasoning step that uses (Agda's) definitional equality.

_β‰‘βŸ¨βŸ©β‡’_ : βˆ€ t β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
_ β‰‘βŸ¨βŸ©β‡’ tβ‡’u = tβ‡’u

{-# INLINE _β‰‘βŸ¨βŸ©β‡’_ #-}

-- Reflexivity.

_∎⟨_βŸ©β‡’ : βˆ€ t β†’ Ξ“ ⊒ t ∷ A β†’ Ξ“ ⊒ t β‡’* t ∷ A
_ ∎⟨ ⊒t βŸ©β‡’ = id ⊒t

{-# INLINE _∎⟨_βŸ©β‡’ #-}

------------------------------------------------------------------------
-- Combinators for left-to-right reductions with explicit types

infix -1
  finally-β‡’*∷ finally-β‡’βˆ·
infixr -2
  step-β‡’βˆ· step-β‡’*∷ step-β‡’*βˆ·β‰‘ step-β‡’*βˆ·β‰‘Λ˜ _∷_β‰‘βŸ¨βŸ©β‡’βˆ·_ finally-β‡’*βˆ·β‰‘
  finally-β‡’βˆ·β‰‘

-- A single step.

step-β‡’βˆ· : βˆ€ t A β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-β‡’βˆ· _ _ = flip _⇨_

syntax step-β‡’βˆ· t A uβ‡’v tβ‡’u = t ∷ A β‡’βŸ¨ tβ‡’u ⟩∷ uβ‡’v

{-# INLINE step-β‡’βˆ· #-}

-- Multiple steps.

step-β‡’*∷ : βˆ€ t A β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-β‡’*∷ _ _ = flip _β‡¨βˆ·*_

syntax step-β‡’*∷ t A uβ‡’v tβ‡’u = t ∷ A β‡’*⟨ tβ‡’u ⟩∷ uβ‡’v

{-# INLINE step-β‡’*∷ #-}

-- A reasoning step that uses propositional equality.

step-β‡’*βˆ·β‰‘ : βˆ€ t A β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ t PE.≑ u β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-β‡’*βˆ·β‰‘ _ _ uβ‡’v PE.refl = uβ‡’v

syntax step-β‡’*βˆ·β‰‘ t A uβ‡’v t≑u = t ∷ A β‰‘βŸ¨ t≑u βŸ©β‡’βˆ· uβ‡’v

-- A reasoning step that uses propositional equality, combined with
-- symmetry.

step-β‡’*βˆ·β‰‘Λ˜ : βˆ€ t A β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ u PE.≑ t β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-β‡’*βˆ·β‰‘Λ˜ _ _ uβ‡’v PE.refl = uβ‡’v

syntax step-β‡’*βˆ·β‰‘Λ˜ t A uβ‡’v u≑t = t ∷ A β‰‘Λ˜βŸ¨ u≑t βŸ©β‡’βˆ· uβ‡’v

-- A reasoning step that uses (Agda's) definitional equality.

_∷_β‰‘βŸ¨βŸ©β‡’βˆ·_ : βˆ€ t A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
_ ∷ _ β‰‘βŸ¨βŸ©β‡’βˆ· tβ‡’u = tβ‡’u

{-# INLINE _∷_β‰‘βŸ¨βŸ©β‡’βˆ·_ #-}

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

finally-β‡’*∷ : βˆ€ t A u β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-β‡’*∷ _ _ _ tβ‡’u = tβ‡’u

syntax finally-β‡’*∷ t A u tβ‡’u = t ∷ A β‡’*⟨ tβ‡’u ⟩∎∷ u ∎

{-# INLINE finally-β‡’*∷ #-}

-- A variant of finally-β‡’*∷.

finally-β‡’βˆ· : βˆ€ t A u β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-β‡’βˆ· _ _ _ tβ‡’u ⊒u = tβ‡’u ⇨ id ⊒u

syntax finally-β‡’βˆ· t A u tβ‡’u ⊒u = t ∷ A β‡’βŸ¨ tβ‡’u , ⊒u ⟩∎∷ u ∎

{-# INLINE finally-β‡’βˆ· #-}

-- A variant of finally-β‡’*∷ that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∷_∎⟨_βŸ©β‡’.

finally-β‡’*βˆ·β‰‘ : βˆ€ t A β†’ u PE.≑ v β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
finally-β‡’*βˆ·β‰‘ _ _ PE.refl tβ‡’u = tβ‡’u

syntax finally-β‡’*βˆ·β‰‘ t A u≑v tβ‡’u = t ∷ A β‡’*⟨ tβ‡’u βŸ©βˆŽβˆ·β‰‘ u≑v

-- A variant of finally-β‡’*βˆ·β‰‘.

finally-β‡’βˆ·β‰‘ :
  βˆ€ t A β†’ u PE.≑ v β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
finally-β‡’βˆ·β‰‘ _ _ PE.refl = finally-β‡’ _ _

syntax finally-β‡’βˆ·β‰‘ t A u≑v tβ‡’u = t ∷ A β‡’βŸ¨ tβ‡’u βŸ©βˆŽβˆ·β‰‘ u≑v

------------------------------------------------------------------------
-- Combinators for right-to-left reductions with explicit types

infix -1
  finally-⇐*∷ finally-β‡βˆ·
infixr -2
  step-β‡βˆ· step-⇐*∷ step-⇐*βˆ·β‰‘ step-⇐*βˆ·β‰‘Λ˜ _∷_β‰‘βŸ¨βŸ©β‡βˆ·_ finally-⇐*βˆ·β‰‘
  finally-β‡βˆ·β‰‘

opaque

  -- A single step.

  step-β‡βˆ· :
    βˆ€ v A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ u β‡’ v ∷ A β†’ Ξ“ ⊒ v ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
  step-β‡βˆ· _ _ tβ‡’u uβ‡’v ⊒v = tβ‡’u β‡¨βˆ·* (uβ‡’v ⇨ id ⊒v)

  syntax step-β‡βˆ· v A tβ‡’u uβ‡’v ⊒v = v ∷ A β‡βŸ¨ uβ‡’v , ⊒v ⟩∷ tβ‡’u

-- Multiple steps.

step-⇐*∷ : βˆ€ v A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ u β‡’* v ∷ A β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-⇐*∷ _ _ = _β‡¨βˆ·*_

syntax step-⇐*∷ v A tβ‡’u uβ‡’v = v ∷ A ⇐*⟨ uβ‡’v ⟩∷ tβ‡’u

{-# INLINE step-⇐*∷ #-}

-- A reasoning step that uses propositional equality.

step-⇐*βˆ·β‰‘ : βˆ€ v A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ v PE.≑ u β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-⇐*βˆ·β‰‘ _ _ tβ‡’u PE.refl = tβ‡’u

syntax step-⇐*βˆ·β‰‘ v A tβ‡’u v≑u = v ∷ A β‰‘βŸ¨ v≑u βŸ©β‡βˆ· tβ‡’u

-- A reasoning step that uses propositional equality, combined with
-- symmetry.

step-⇐*βˆ·β‰‘Λ˜ : βˆ€ v A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ u PE.≑ v β†’ Ξ“ ⊒ t β‡’* v ∷ A
step-⇐*βˆ·β‰‘Λ˜ _ _ tβ‡’u PE.refl = tβ‡’u

syntax step-⇐*βˆ·β‰‘Λ˜ v A tβ‡’u u≑v = v ∷ A β‰‘Λ˜βŸ¨ u≑v βŸ©β‡βˆ· tβ‡’u

-- A reasoning step that uses (Agda's) definitional equality.

_∷_β‰‘βŸ¨βŸ©β‡βˆ·_ : βˆ€ u A β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
_ ∷ _ β‰‘βŸ¨βŸ©β‡βˆ· tβ‡’u = tβ‡’u

{-# INLINE _∷_β‰‘βŸ¨βŸ©β‡βˆ·_ #-}

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

finally-⇐*∷ : βˆ€ u A t β†’ Ξ“ ⊒ t β‡’* u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-⇐*∷ _ _ _ tβ‡’u = tβ‡’u

syntax finally-⇐*∷ u A t tβ‡’u = u ∷ A ⇐*⟨ tβ‡’u ⟩∎∷ t ∎

{-# INLINE finally-⇐*∷ #-}

-- A variant of finally-⇐*∷.

finally-β‡βˆ· : βˆ€ u A t β†’ Ξ“ ⊒ t β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
finally-β‡βˆ· _ _ _ tβ‡’u ⊒u = tβ‡’u ⇨ id ⊒u

syntax finally-β‡βˆ· u A t tβ‡’u ⊒u = u ∷ A β‡βŸ¨ tβ‡’u , ⊒u ⟩∎∷ t ∎

{-# INLINE finally-β‡βˆ· #-}

-- A variant of finally-⇐*∷ that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∷_∎⟨_βŸ©β‡’.

finally-⇐*βˆ·β‰‘ : βˆ€ v A β†’ u PE.≑ t β†’ Ξ“ ⊒ v β‡’* u ∷ A β†’ Ξ“ ⊒ v β‡’* t ∷ A
finally-⇐*βˆ·β‰‘ _ _ PE.refl vβ‡’u = vβ‡’u

syntax finally-⇐*βˆ·β‰‘ v A u≑t vβ‡’u = v ∷ A ⇐*⟨ vβ‡’u βŸ©βˆŽβˆ·β‰‘ u≑t

-- A variant of finally-⇐*βˆ·β‰‘.

finally-β‡βˆ·β‰‘ :
  βˆ€ v A β†’ u PE.≑ t β†’ Ξ“ ⊒ v β‡’ u ∷ A β†’ Ξ“ ⊒ u ∷ A β†’ Ξ“ ⊒ v β‡’* t ∷ A
finally-β‡βˆ·β‰‘ _ _ PE.refl = finally-⇐ _ _

syntax finally-β‡βˆ·β‰‘ v A u≑t vβ‡’u ⊒u = v ∷ A β‡βŸ¨ vβ‡’u , ⊒u βŸ©βˆŽβˆ·β‰‘ u≑t

------------------------------------------------------------------------
-- A combinator for left-to-right or right-to-left reductions with
-- explicit types

infix -1 _∷_∎⟨_βŸ©β‡’

-- Reflexivity.

_∷_∎⟨_βŸ©β‡’ : βˆ€ t A β†’ Ξ“ ⊒ t ∷ A β†’ Ξ“ ⊒ t β‡’* t ∷ A
_ ∷ _ ∎⟨ ⊒t βŸ©β‡’ = id ⊒t

{-# INLINE _∷_∎⟨_βŸ©β‡’ #-}

------------------------------------------------------------------------
-- Conversion combinators

infix -2 step-β‡’*-conv step-β‡’*-conv˘ step-β‡’*-conv-≑ step-β‡’*-conv-β‰‘Λ˜

opaque

  -- Conversion.

  step-β‡’*-conv : Ξ“ ⊒ t β‡’* u ∷ B β†’ Ξ“ ⊒ A ≑ B β†’ Ξ“ ⊒ t β‡’* u ∷ A
  step-β‡’*-conv tβ‡’u A≑B = conv* tβ‡’u (sym A≑B)

  syntax step-β‡’*-conv tβ‡’u A≑B = ⟨ A≑B βŸ©β‡’ tβ‡’u

opaque

  -- Conversion.

  step-β‡’*-conv˘ : Ξ“ ⊒ t β‡’* u ∷ B β†’ Ξ“ ⊒ B ≑ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
  step-β‡’*-conv˘ tβ‡’u B≑A = conv* tβ‡’u B≑A

  syntax step-β‡’*-conv˘ tβ‡’u B≑A = ˘⟨ B≑A βŸ©β‡’ tβ‡’u

-- Conversion using propositional equality.

step-β‡’*-conv-≑ : Ξ“ ⊒ t β‡’* u ∷ B β†’ A PE.≑ B β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-β‡’*-conv-≑ tβ‡’u PE.refl = tβ‡’u

syntax step-β‡’*-conv-≑ tβ‡’u A≑B = ⟨ A≑B βŸ©β‡’β‰‘ tβ‡’u

-- Conversion using propositional equality.

step-β‡’*-conv-β‰‘Λ˜ : Ξ“ ⊒ t β‡’* u ∷ B β†’ B PE.≑ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-β‡’*-conv-β‰‘Λ˜ tβ‡’u PE.refl = tβ‡’u

syntax step-β‡’*-conv-β‰‘Λ˜ tβ‡’u B≑A = ˘⟨ B≑A βŸ©β‡’β‰‘ tβ‡’u

------------------------------------------------------------------------
-- Conversion combinators for left-to-right reductions with explicit
-- types

infix -2 step-βˆ·β‡’*-conv step-βˆ·β‡’*-conv˘ step-βˆ·β‡’*-conv-≑ step-βˆ·β‡’*-conv-β‰‘Λ˜

-- Conversion.

step-βˆ·β‡’*-conv : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ Ξ“ ⊒ A ≑ B β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡’*-conv _ = step-β‡’*-conv

syntax step-βˆ·β‡’*-conv A tβ‡’u A≑B = ∷ A ⟨ A≑B βŸ©β‡’ tβ‡’u

{-# INLINE step-βˆ·β‡’*-conv #-}

-- Conversion.

step-βˆ·β‡’*-conv˘ : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ Ξ“ ⊒ B ≑ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡’*-conv˘ _ = step-β‡’*-conv˘

syntax step-βˆ·β‡’*-conv˘ A tβ‡’u B≑A = ∷ A ˘⟨ B≑A βŸ©β‡’ tβ‡’u

{-# INLINE step-βˆ·β‡’*-conv˘ #-}

-- Conversion using propositional equality.

step-βˆ·β‡’*-conv-≑ : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ A PE.≑ B β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡’*-conv-≑ _ tβ‡’u PE.refl = tβ‡’u

syntax step-βˆ·β‡’*-conv-≑ A tβ‡’u A≑B = ∷ A ⟨ A≑B βŸ©β‡’β‰‘ tβ‡’u

-- Conversion using propositional equality.

step-βˆ·β‡’*-conv-β‰‘Λ˜ : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ B PE.≑ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡’*-conv-β‰‘Λ˜ _ tβ‡’u PE.refl = tβ‡’u

syntax step-βˆ·β‡’*-conv-β‰‘Λ˜ A tβ‡’u B≑A = ∷ A ˘⟨ B≑A βŸ©β‡’β‰‘ tβ‡’u

------------------------------------------------------------------------
-- Conversion combinators for right-to-left reductions with explicit
-- types

infix -2 step-βˆ·β‡*-conv step-βˆ·β‡*-conv˘ step-βˆ·β‡*-conv-≑ step-βˆ·β‡*-conv-β‰‘Λ˜

-- Conversion.

step-βˆ·β‡*-conv : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ Ξ“ ⊒ A ≑ B β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡*-conv _ = step-β‡’*-conv

syntax step-βˆ·β‡*-conv A tβ‡’u A≑B = ∷ A ⟨ A≑B βŸ©β‡ tβ‡’u

{-# INLINE step-βˆ·β‡*-conv #-}

-- Conversion.

step-βˆ·β‡*-conv˘ : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ Ξ“ ⊒ B ≑ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡*-conv˘ _ = step-β‡’*-conv˘

syntax step-βˆ·β‡*-conv˘ A tβ‡’u B≑A = ∷ A ˘⟨ B≑A βŸ©β‡ tβ‡’u

{-# INLINE step-βˆ·β‡*-conv˘ #-}

-- Conversion using propositional equality.

step-βˆ·β‡*-conv-≑ : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ A PE.≑ B β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡*-conv-≑ _ tβ‡’u PE.refl = tβ‡’u

syntax step-βˆ·β‡*-conv-≑ A tβ‡’u A≑B = ∷ A ⟨ A≑B βŸ©β‡β‰‘ tβ‡’u

-- Conversion using propositional equality.

step-βˆ·β‡*-conv-β‰‘Λ˜ : βˆ€ A β†’ Ξ“ ⊒ t β‡’* u ∷ B β†’ B PE.≑ A β†’ Ξ“ ⊒ t β‡’* u ∷ A
step-βˆ·β‡*-conv-β‰‘Λ˜ _ tβ‡’u PE.refl = tβ‡’u

syntax step-βˆ·β‡*-conv-β‰‘Λ˜ A tβ‡’u B≑A = ∷ A ˘⟨ B≑A βŸ©β‡β‰‘ tβ‡’u