Search code examples
agda

Agda: prove that ¬Any≃All¬, FromTo base case

following the PLFA I'm trying to prove that

¬Any≃All¬ : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs

My problem is with

FromTo : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (v : (¬_ ∘ Any P) xs) → ((from xs) ∘ (to xs)) v ≡ v

If xs ≡ [], then I am not sure if ¬ Any P [] is unhabited or not. I think it is unhabited, but when I try

FromTo [] ()

I get an error:

(¬_ ∘ Any P) [] should be empty, but that's not obvious to me
when checking the clause left hand side
FromTo [] ()
Solution

  • There is only one lambda from the empty type to the empty type, the empty lambda. We can use extensionality to prove the two lambdas are equal. And since there is no element in the empty type, the lambda inside the extensionality is the empty lambda.

    FromTo [] t = extensionality (λ {()})