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

infixl 50 _∘'_
_∘'_ :
  {ℓ₁ ℓ₂ ℓ₃ : 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