RawFunctor.agda

{-# OPTIONS --universe-polymorphism #-}

module RawFunctor where

open import Common.Level

postulate RawFunctor : ∀ {ℓ} (F : Set ℓ → Set ℓ) → Set (lsuc ℓ)

-- Broken occurs check for levels made this not infer properly
postulate
  sequence⁻¹ : ∀ {F}{A} {P : A → Set} → RawFunctor F →
                 F (∀ i → P i) → ∀ i → F (P i)