{"header":{"message":"7. Negation","description":null,"timestamp":"2026-02-17T14:31:41.979715043Z","authors":[{}]},"hash":"T5OZLUEU6FUYDNWCXEGRUEG5PC6SM4GKPF7JBR4RMLFW23437WLAC","authors":[{"login":"tzemanovic","key":"3FpVTsmZthvnKhEGTe7aUW47SMW2aCxSdqSHT4iuQREo"}],"deps":{"hashes":[["T5OZLUEU6FUYDNWCXEGRUEG5PC6SM4GKPF7JBR4RMLFW23437WLAC","7. Negation"],["AA",null],["SHHLAOUJR4YNATSPEACPP56ITB6353COYJGUDEN47747EFPYJNQAC","Bump sass from 1.89.2 to 1.90.0 (#1124)"]],"deps":["SHHLAOUJR4YNATSPEACPP56ITB6353COYJGUDEN47747EFPYJNQAC"],"known":[]},"hunks":[{"Edit":{"inode":{"change":2,"pos":7807321},"path":"src/plfa/part1/Negation.lagda.md","line":195,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7813661}],"down_context":[{"change":2,"pos":7813661}],"flag":"BLOCK","start":1969,"end":2119,"inode":{"change":2,"pos":7807321}}},"contents":[{"Add":""},{"Add":"open Data.Nat using (_<_;s_;z n)"},{"Add":" ⊎ (¬ m < n × m ≡ n × ¬ m > n)"},{"Add":" ⊎ (¬ m < n × ¬ m ≡ n × m > n)"},{"Add":"trichotomy zero zero = inj₂ (inj₁ ⟨ (λ ()) , ⟨ refl , (λ ()) ⟩ ⟩)"},{"Add":"trichotomy zero (suc n) = inj₁ ⟨ (zn ⟩ ⟩ ="},{"Add":" inj₁"},{"Add":" ⟨ sn) → ¬m>n m>n }) ⟩"},{"Add":" ⟩"},{"Add":"...| inj₂ (inj₁ ⟨ ¬mn ⟩ ⟩) ="},{"Add":" inj₂ (inj₁"},{"Add":" ⟨ (λ{ (sn) → ¬m>n m>n }) ⟩"},{"Add":" ⟩)"},{"Add":"...| inj₂ (inj₂ ⟨ ¬mn ⟩ ⟩) ="},{"Add":" inj₂ (inj₂"},{"Add":" ⟨ (λ{ (sn ⟩"},{"Add":" ⟩)"},{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":7807321},"path":"src/plfa/part1/Negation.lagda.md","line":264,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7814346}],"down_context":[{"change":2,"pos":7814346}],"flag":"BLOCK","start":3268,"end":3911,"inode":{"change":2,"pos":7807321}}},"contents":[{"Add":""},{"Add":"open import plfa.part1.Isomorphism using (_∘_)"},{"Add":""},{"Add":"-- Cannot import from Connectives as it's not using stdlib Sum and Product types!"},{"Add":"→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))"},{"Add":"→-distrib-⊎ ="},{"Add":" record"},{"Add":" { to = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }"},{"Add":" ; from = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }"},{"Add":" ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }"},{"Add":" ; to∘from = λ{ _ → refl }"},{"Add":" }"},{"Add":""},{"Add":"⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)"},{"Add":"⊎-dual-× = →-distrib-⊎ {_} {_} {⊥}"},{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":7807321},"path":"src/plfa/part1/Negation.lagda.md","line":290,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7814522}],"down_context":[{"change":2,"pos":7814522}],"flag":"BLOCK","start":3912,"end":3920,"inode":{"change":2,"pos":7807321}}},"contents":[{"Add":"```agda"}]}},{"Edit":{"inode":{"change":2,"pos":7807321},"path":"src/plfa/part1/Negation.lagda.md","line":292,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7814523}],"down_context":[{"change":2,"pos":7814523}],"flag":"BLOCK","start":3921,"end":4263,"inode":{"change":2,"pos":7807321}}},"contents":[{"Add":"-- Cannot do the other way around because `(¬ A) ⊎ (¬ B)` holds only iff ¬ A or"},{"Add":"-- ¬ B exclusively, whereas `¬ (A × B)` may hold when both ¬ A and ¬ B hold"},{"Add":"⊎-implies-× : ∀ {A B : Set} → (¬ A) ⊎ (¬ B) → ¬ (A × B)"},{"Add":"⊎-implies-× = λ"},{"Add":" { (inj₁ ¬a) → ¬a ∘ proj₁"},{"Add":" ; (inj₂ ¬b) → ¬b ∘ proj₂"},{"Add":" }"},{"Add":""},{"Add":"```"},{"Add":""},{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":7807321},"path":"src/plfa/part1/Negation.lagda.md","line":449,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7820754}],"down_context":[{"change":2,"pos":7820754}],"flag":"BLOCK","start":4264,"end":7110,"inode":{"change":2,"pos":7807321}}},"contents":[{"Add":""},{"Add":"em-implies-dne : ∀ {A : Set} → (A ⊎ ¬ A) → ¬ ¬ A → A"},{"Add":"em-implies-dne (inj₁ a) _ = a"},{"Add":"em-implies-dne (inj₂ ¬a) ¬¬a = ⊥-elim (¬¬a ¬a) -- bottom implies anything"},{"Add":""},{"Add":"em-implies-pierce : ∀ {A B : Set} → (A ⊎ ¬ A) → ((A → B) → A) → A"},{"Add":"em-implies-pierce (inj₁ a) _ = a"},{"Add":"em-implies-pierce (inj₂ ¬a) a-b-a = a-b-a λ{ a → ⊥-elim (¬a a) }"},{"Add":""},{"Add":"em-implies-imdis : ∀ {A B : Set} → (A ⊎ ¬ A) → (A → B) → ¬ A ⊎ B"},{"Add":"em-implies-imdis (inj₁ a) a-b = inj₂ (a-b a)"},{"Add":"em-implies-imdis (inj₂ ¬a) _ = inj₁ ¬a"},{"Add":""},{"Add":"em-implies-demorg : ∀ {A B : Set} → (∀ {C : Set} → C ⊎ ¬ C) → ¬ (¬ A × ¬ B) → A ⊎ B"},{"Add":"em-implies-demorg {A} {B} em demorg-dom with em {A} | em {B}"},{"Add":"...| inj₁ a | _ = inj₁ a"},{"Add":"...| inj₂ _ | inj₁ b = inj₂ b"},{"Add":"...| inj₂ ¬a | inj₂ ¬b = ⊥-elim (demorg-dom ⟨ ¬a , ¬b ⟩)"},{"Add":""},{"Add":""},{"Add":"dne-implies-em : ∀ {A : Set} → ¬ ¬ A → A → (A ⊎ ¬ A)"},{"Add":"dne-implies-em _ a = inj₁ a"},{"Add":""},{"Add":"dne-implies-pierce : ∀ {A B : Set} → ¬ ¬ A → A → ((A → B) → A) → A"},{"Add":"dne-implies-pierce _ a = λ _ → a"},{"Add":""},{"Add":"dne-implies-imdis : ∀ {A B : Set} → ¬ ¬ A → A → (A → B) → ¬ A ⊎ B"},{"Add":"dne-implies-imdis _ a = λ a→b → inj₂ (a→b a)"},{"Add":""},{"Add":"dne-implies-demorg : ∀ {A B : Set} → ¬ ¬ A → A → ¬ (¬ A × ¬ B) → A ⊎ B"},{"Add":"dne-implies-demorg _ a = λ _ → inj₁ a"},{"Add":""},{"Add":""},{"Add":"pierce-implies-em : ∀ {A B : Set} → ((A → B) → A) → A → (A ⊎ ¬ A)"},{"Add":"pierce-implies-em _ a = inj₁ a"},{"Add":""},{"Add":"pierce-implies-dne : ∀ {A B : Set} → ((A → B) → A) → A → ¬ ¬ A → A"},{"Add":"pierce-implies-dne _ a _ = a"},{"Add":""},{"Add":"pierce-implies-imdis : ∀ {A B : Set} → ((A → B) → A) → A → (A → B) → ¬ A ⊎ B"},{"Add":"pierce-implies-imdis _ a a→b = inj₂ (a→b a)"},{"Add":""},{"Add":"pierce-implies-demorg : ∀ {A B : Set} → ((A → B) → A) → A → ¬ (¬ A × ¬ B) → A ⊎ B"},{"Add":"pierce-implies-demorg _ a _ = inj₁ a"},{"Add":""},{"Add":""},{"Add":"imdis-implies-em : (∀ {A B : Set} → (A → B) → ¬ A ⊎ B) → ∀ {C : Set} → (C ⊎ ¬ C)"},{"Add":"imdis-implies-em imdis with (imdis λ{ a → a })"},{"Add":"...| (inj₁ ¬a) = inj₂ ¬a"},{"Add":"...| (inj₂ a) = inj₁ a"},{"Add":""},{"Add":"imdis-implies-dne : (∀ {A B : Set} → (A → B) → ¬ A ⊎ B) → ∀ {C : Set} → ¬ ¬ C → C"},{"Add":"imdis-implies-dne imdis ¬¬c with (imdis λ{ a → a })"},{"Add":"...| (inj₁ ¬a) = ⊥-elim (¬¬c ¬a)"},{"Add":"...| (inj₂ a) = a"},{"Add":""},{"Add":"imdis-implies-pierce : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B → ((A → B) → A) → A"},{"Add":"imdis-implies-pierce a→b _ a→b→a = a→b→a a→b"},{"Add":""},{"Add":"imdis-implies-demorg : (∀ {A B : Set} → (A → B) → ¬ A ⊎ B) → ∀ {C D : Set} → ¬ (¬ C × ¬ D) → C ⊎ D"},{"Add":"imdis-implies-demorg imdis {C} {D} demorg-dom with (imdis {C} λ{ a → a }) | (imdis {D} λ{ a → a })"},{"Add":"... | _ | inj₂ d = inj₂ d"},{"Add":"... | inj₂ c | _ = inj₁ c"},{"Add":"... | inj₁ ¬c | inj₁ ¬d = ⊥-elim (demorg-dom ⟨ ¬c , ¬d ⟩)"},{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":7807321},"path":"src/plfa/part1/Negation.lagda.md","line":529,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7821060}],"down_context":[{"change":2,"pos":7821060}],"flag":"BLOCK","start":7111,"end":7415,"inode":{"change":2,"pos":7807321}}},"contents":[{"Add":""},{"Add":"¬-stable : {A : Set} → Stable (¬ A)"},{"Add":"¬-stable = ¬¬¬-elim"},{"Add":""},{"Add":"×-stable : {A B : Set} → Stable A → Stable B → Stable (A × B)"},{"Add":"×-stable a b ¬¬a×b ="},{"Add":" ⟨ (a (λ ¬¬a → ¬¬a×b (λ a×b → ¬¬a (proj₁ a×b))))"},{"Add":" , (b (λ ¬¬b → ¬¬a×b (λ a×b → ¬¬b (proj₂ a×b))))"},{"Add":" ⟩"},{"Add":""}]}}],"owner":"tzemanovic","repo":"plfa","token":"ripvVcNKSCXOaNoT1StPNxrte1tNPv5Lal6SQFYUySE=","login":null}

…

Dependencies

Change contents