open import Data.Product

open import Stoughton.Var

module Normalizing {𝒞 𝒱 : Set} (enum : Enum 𝒱) (𝒜 : 𝒞 → 𝒞 → Set) (ℛ : 𝒞 → 𝒞 → 𝒞 → Set) where

  open Enum enum
  
  open import Stoughton.Syntax 𝒞 𝒱 _≟_

  open import BetaReduction 𝒞 enum
  open import PTSs enum 𝒜 ℛ
  
  open import NormalForm enum 𝒜 ℛ
  
  wn : Λ → Set
  wn M = ∃ λ N → nf N × M →β*₀ N

  Normalizing : Set
  Normalizing = ∀ {Γ M A} → Γ ⊢ₛ M ∶ A → wn M × wn A