module Combinatory.Equality where
open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive
open import Combinatory.Signature
open import Combinatory.Syntax
open import SOAS.Metatheory.SecondOrder.Metasubstitution CL:Syn
open import SOAS.Metatheory.SecondOrder.Equality CL:Syn
private
variable
α β γ τ : *T
Γ Δ Π : Ctx
infix 1 _▹_⊢_≋ₐ_
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ CL) α Γ → (𝔐 ▷ CL) α Γ → Set where
IA : ⁅ * ⁆̣ ▹ ∅ ⊢ I $ 𝔞 ≋ₐ 𝔞
KA : ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (K $ 𝔞) $ 𝔟 ≋ₐ 𝔞
SA : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ ((S $ 𝔞) $ 𝔟) $ 𝔠 ≋ₐ (𝔞 $ 𝔠) $ (𝔟 $ 𝔠)
open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning