[Agda] Are there unicorns in Agda?

[Nils Anders Danielsson]

On 2011-11-11 10:29, Martin Escardo wrote:
> But what is precisely your answer? For example, although there may not
> be non-constant maps F:Set->X with X:Set, there certainly are
> non-constant maps F':Set->Set.

Given Agda's strange sizing rules there are also non-constant maps of
type Set₁ → Set:

   data _≡_ (A : Set₁) : Set₁ → Set where
     refl : A ≡ A

   data ⊥ : Set₁ where

   Empty : Set₁ → Set
   Empty X = X ≡ ⊥

It is easy to prove that Empty is not constant:

   ¬_ : Set₂ → Set₂
   ¬ X = X → ⊥

   data ⊤ : Set₁ where
     tt : ⊤

   data _≡′_ (A : Set) : Set → Set₁ where
     refl : A ≡′ A

   cast : {A B : Set₁} → A ≡ B → A → B
   cast refl p = p

   cast′ : {A B : Set} → A ≡′ B → A → B
   cast′ refl p = p

   not-constant : ¬ (∀ X Y → Empty X ≡′ Empty Y)
   not-constant hyp = absurd
     where
     ⊥≡⊥≡⊤≡⊥ : (⊥ ≡ ⊥) ≡′ (⊤ ≡ ⊥)
     ⊥≡⊥≡⊤≡⊥ = hyp ⊥ ⊤

     ⊤≡⊥ : ⊤ ≡ ⊥
     ⊤≡⊥ = cast′ ⊥≡⊥≡⊤≡⊥ refl

     absurd : ⊥
     absurd = cast ⊤≡⊥ tt

We should probably disallow definitions like _≡_ above.

-- 
/NAD