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