{-# OPTIONS --without-K #-}
module Class.Core where

open import Class.Prelude

Type[_↝_] : ∀ ℓ ℓ′ → Type (lsuc ℓ ⊔ lsuc ℓ′)
Type[ ℓ ↝ ℓ′ ] = Type ℓ → Type ℓ′

Type↑ : Typeω
Type↑ = ∀ {ℓ} → Type[ ℓ ↝ ℓ ]

module _ (M : Type↑) where
  _¹ : (A → Type ℓ) → Type _
  _¹ P = ∀ {x} → M (P x)

  _² : (A → B → Type ℓ) → Type _
  _² _~_ = ∀ {x y} → M (x ~ y)

  _³ : (A → B → C → Type ℓ) → Type _
  _³ _~_~_ = ∀ {x y z} → M (x ~ y ~ z)

variable
  M F : Type↑