[Agda] Absurd question

[Wolfram Kahl]

Martin,

  since more recently, you wrote:

> But they should have the same type, and this should be enough to
> get blah going.

, I still finish my old attempt at an answer to one aspect of your question:

On Fri, May 24, 2013 at 12:26:51AM +0100, Martin Escardo wrote:
> At the risk of polluting this list with too many messages, I make 
> explicit what I said below, in the previous message:
> 
> I have two closed terms dialogue-tree and dialogue-tree' with 
> (literally) the same closed type. The definition of one term uses \(), 
> and the definition of the other term uses y instead.

module Escardo where

open import Data.Fin using (Fin)
open import Relation.Binary.PropositionalEquality using (_≡_)

-- |dt| and |dt′| have the same closed type:

dt : Set
dt = Fin 1

dt′ : Set
dt′ = Fin 2

> But a certain definition (namely dialogue-tree-correct) type-checks if 
> one of its subterms is dialogue-tree', but doesn't if it is 
> dialogue-tree. But surely, because everything is closed, it shouldn't 
> matter which term we use (even a postulated term should do).

-- |dt-correct| type-checks:
dt-correct : Set
dt-correct = (x : Fin 1) (y : dt) → x ≡ y

-- |dt′-incorrect| does not type-check:
-- dt′-incorrect : Set
-- dt′-incorrect = (x : Fin 1) (y : dt′) → x ≡ y


Wolfram