[Agda] false \equiv true

[Adam Gundry]

Hi Sergei,

On 11/03/13 10:12, Serge D. Mechveliani wrote:
> Please, can you explain things about the following code?
> 
>   postulate negMem-i : memberC? i ≡ true -> ⊥  
> 
>   fromEmpty : ⊥ -> false ≡ true
>   fromEmpty = λ()
> 
>   reject : memberC? i ≡ true -> false ≡ true
>   reject = fromEmpty ∘ negMem-i
> 
> Its goal is as follows. Given a 
>   the type  foo ≡ true   normalized to  false ≡ true, 
>   negation   negMem-i  for  memberC? i ≡ true 
>   build the negation map to  foo ≡ true.
> 
> 1. I have discovered that  false ≡ true  is not normalized further to ⊥.
>    Probably, there exist many  normal type expressions  which types 
>    have not any value (?).
>    Is this all right?

Yes, there are many uninhabited types, which do not necessarily
normalise to ⊥. It is not decidable whether a given type is inhabited,
but Agda allows you to write () if it is sufficiently obvious that the
type is uninhabited (e.g. in the case of false ≡ true).


> Hence, I need to apply  negMem-i  and convert further from  ⊥  to  
> false ≡ true.
> 
> 2. "reject = λ() ∘ negMem-i"  
>    is not parsed.
>    So I need to define an additional function  fromEmpty.
>    Right?
>
> 3. Can the whole example be written in a simpler way?

Adding parentheses to give

(λ()) ∘ negMem-i

would parse, but fail to typecheck. The type of dependent composition is
quite complicated, and Agda cannot infer all the implicit arguments in
this case. It will work if you use non-dependent composition, defined
thus in the standard library:

_∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
       (B → C) → (A → B) → (A → C)
f ∘′ g = _∘_ f g

Also, your fromEmpty function is a special case of the usual eliminator
for ⊥, defined in the standard library by:

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()


Hope this helps,

Adam


-- 
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.