{-# OPTIONS --without-K #-} {- The above line turns off the axiom K. The Axiom K is equivalent to UIP and would turn our identification types into "identification types with UIP". We do not want that. -} postulate magic : ∀ {i} {X : Set i} → X {- REMOVE THIS LINE when submitting your homework! -} Type : Set₁ Type = Set₀ -- a better name for Set₀ record Σ (A : Type) (B : A → Type) : Type where constructor _,_ field fst : A snd : B fst open Σ public infixr 60 _,_ data _⊔_ (A : Type) (B : Type) : Type where inl : A → A ⊔ B inr : B → A ⊔ B infixr 4 _⊔_ data ℕ : Type where zero : ℕ suc : (n : ℕ) → ℕ {-# BUILTIN NATURAL ℕ #-} data _<_ : ℕ → ℕ → Type where lt-suc : ∀ {n : ℕ} → n < suc n lt-suc-rec : ∀ {n m : ℕ} → n < m → n < suc m data _≡_ {A : Type} (x : A) : A → Type where refl : x ≡ x ap : ∀ {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y ap f refl = refl 0