[Agda] Question, re: x-dual-U exercise in Negation chapter of PLFA.

[David Banas]

Hi all,

In trying to answer the following question from the *Negation* chapter of
PLFA:

Do we also have the following?

¬ (A × B) ≃ (¬ A) ⊎ (¬ B)

If so, prove; if not, can you give a relation weaker than isomorphism that
relates the two sides?

It seems to me that I ought to be able to define an *embedding*. That is, I
should *not* have to settle for just an *equivalence*:

×-dual-⊎ : ∀ {A B : Set}
    -------------------------
  → ¬ (A × B) ≲ (¬ A) ⊎ (¬ B)
×-dual-⊎ =
  record
    { to      = λ ¬A×B → inj₁ (λ a → ¬A×B (a , _))
    ; from    = λ { (inj₁ ¬A) → λ (a , _) → ¬A a
                  ; (inj₂ ¬B) → λ (_ , b) → ¬B b
                  }
    ; from∘to = λ ¬A×B → extensionality (λ (a , _) → refl
    -- ; to∘from = λ { (inj₁ ¬A) → -- We could write this one.
    --               ; (inj₂ ¬B) →
    --               -- Can't write this, due to choice of `inj₁` for `to`,
above.
    --               }
    }


However, when I try the code above, I get:

Cannot instantiate the metavariable _140 to solution
snd(.patternInTele0) since it contains the variable
snd(.patternInTele0) which is not in scope of the metavariable
when checking that the expression refl has type
(λ { (inj₁ ¬A)
       → λ .patternInTele0 → ¬A (Data.Product.proj₁ .patternInTele0)
   ; (inj₂ ¬B)
       → λ .patternInTele0 → ¬B (Data.Product.proj₂ .patternInTele0)
   })
(inj₁ (λ a → ¬A×B (a , _snd_140 (¬A×B = ¬A×B) (a = a))))
.patternInTele0
≡ ¬A×B .patternInTele0


Any thoughts?

Thanks,
-db
:)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200822/ec7b88a3/attachment.html>