module ImprHIT.Background.Impredicativity where

open import Cubical.Foundations.Prelude
open import Agda.Primitive using (Level) renaming (Set to Type)

private
  variable
    ℓ : Level
    A : Type ℓ
    B : A → Type ℓ

postulate
  Π : (A : Type ℓ) (B : A → Type₀) → Type₀ -- formation
  Λ : (∀ x → B x) → Π A B                  -- introduction
  ev : Π A B → ∀ x → B x                   -- elimination

postulate
  Π-β : (f : ∀ x → B x) → ev (Λ f) ≡ f
  Π-η : (f : Π A B) → Λ (ev f) ≡ f

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE Π-β Π-η #-}