← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda-stdlib/wily

« back to all changes in this revision

Viewing changes to src/Relation/Nullary/Negation.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-05-27 19:29:25 UTC
  • mfrom: (8.1.1 experimental)
  • Revision ID: package-import@ubuntu.com-20130527192925-q2tadfousmn0xeav
Tags: 0.7-2
Upload to unstable 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Nullary/Negation.agda
138
138
 
139
139
independence-of-premise
140
140
  : ∀ {p q r} {P : Set p} {Q : Set q} {R : Q → Set r} →
141
 
    Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∶ Q ] (P → R x))
 
141
    Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∈ Q ] (P → R x))
142
142
independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
143
143
  where
144
144
  helper : Dec P → _