------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of indexed negation ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Relation.Nullary.Indexed.Negation where open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Function.Bundles using (_↔_) open import Function.Properties using (→-cong-↔) import Function.Construct.Identity as Identity using (↔-id) open import Relation.Nullary.Indexed ------------------------------------------------------------------------ -- ¬_ preserves ↔ (assuming extensionality) ¬-cong : ∀ {a b c} {A : Set a} {B : Set b} → Extensionality a c → Extensionality b c → A ↔ B → (¬ c A) ↔ (¬ c B) ¬-cong extA extB A≈B = →-cong-↔ extA extB A≈B (Identity.↔-id ⊥)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4