{-# OPTIONS --without-K #-}

module agda.postulates where

open import agda.prelude

postulate
  -- Function extensionality
  funext :
    {l l' : Level}
    {A : Set l}
    {B : A → Set l'}
    {f g : (x : A) → B x}
    (_ : (x : A) → f x ≡ g x)
    → -----------------------
    f ≡ g

  -- Uniqueness of identity proofs
  uip :
    {l : Level}
    {A : Set l}
    {x y : A}
    {p q : x ≡ y}
    → -----------
    p ≡ q

  -- The interval
  𝕀   : Set
  O   : 𝕀
  I   : 𝕀
  O≠I : O ≡ I → ⊥

  -- Cofibrant types
  cof  : Set → Set
  cof⊥ : cof ⊥ -- (O ≡ I)