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

[Thorsten Altenkirch]

There is no information in the left hand side but there is one bit of information on the right. Where should it come from?

Knowing that it cannot be that both A and B are false doesn’t tell you which is not false.

Sent from my iPhone

On 22 Aug 2020, at 22:48, David Banas <capn.freako at gmail.com> wrote:


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
:)

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200822/d2519bcc/attachment.html>