Logic
Content created by Fredrik Bakke.
Created on 2025-01-07.
Last modified on 2025-08-14.
Modules in the logic namespace
module logic where open import logic.complements-de-morgan-subtypes public open import logic.complements-decidable-subtypes public open import logic.complements-double-negation-stable-subtypes public open import logic.de-morgan-embeddings public open import logic.de-morgan-maps public open import logic.de-morgan-propositions public open import logic.de-morgan-subtypes public open import logic.de-morgan-types public open import logic.de-morgans-law public open import logic.dirk-gentlys-principle public open import logic.double-negation-dense-maps public open import logic.double-negation-dense-subtypes public open import logic.double-negation-eliminating-maps public open import logic.double-negation-elimination public open import logic.double-negation-stable-embeddings public open import logic.double-negation-stable-subtypes public open import logic.functoriality-existential-quantification public open import logic.irrefutable-types public open import logic.markovian-types public open import logic.markovs-principle public open import logic.propositional-double-negation-elimination public open import logic.propositionally-decidable-maps public open import logic.propositionally-decidable-types public open import logic.propositionally-double-negation-eliminating-maps public
Recent changes
- 2025-08-14. Fredrik Bakke. More logic (#1387).
- 2025-02-08. Fredrik Bakke. Functorial action of existential quantifications, and applications in
real-numbers
(#1298). - 2025-01-07. Fredrik Bakke. Logic (#1226).