[Agda] false \equiv true
Adam Gundry
adam.gundry at strath.ac.uk
Mon Mar 11 11:28:43 CET 2013
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.
More information about the Agda
mailing list