{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import 1-equality

infixl  _∘'_
_∘'_ :
  {ℓ₁ ℓ₂ ℓ₃ : Level}                     →
  {A : Set ℓ₁}                           →
  {B : A → Set ℓ₂}                       →
  {C : (a : A) → B a → Set ℓ₃}           →
  (f : Π A λ a → Π (B a) λ b → C a b)    →
  (g : Π A B)                            →
  (a : A)                                →
  C a (g a)

(f ∘' g) x = f x (g x)

S = _∘'_

K : {ℓ₁ ℓ₂ ℓ₃ : Level} →
    {A : Set ℓ₁}       →
    {B : Set ℓ₂}       →
    (x : A)            →
    (y : B)            →
    A

K x y = x

I :
  {ℓ : Level} →
  {X : Set ℓ} →
  (X → X)

I x = x

modus·ponens : {ℓ₁ ℓ₂ ℓ₃ : Level} →
  {A : Set ℓ₁}       →
  {B : Set ℓ₂}       →
  (x : A)            →
  (y : A → B)        →
  B

modus·ponens x y = y x