Complements of subtypes

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-09-12.

module foundation.complements-subtypes where

Imports
open import foundation.decidable-propositions
open import foundation.decidable-subtypes
open import foundation.full-subtypes
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.unions-subtypes
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.subtypes


Idea

The complement of a subtype P of A consists of the elements that are not in P.

Definition

Complements of subtypes

complement-subtype :
{l1 l2 : Level} {A : UU l1} → subtype l2 A → subtype l2 A
complement-subtype P x = neg-Prop (P x)


Complements of decidable subtypes

complement-decidable-subtype :
{l1 l2 : Level} {A : UU l1} → decidable-subtype l2 A → decidable-subtype l2 A
complement-decidable-subtype P x = neg-Decidable-Prop (P x)


Properties

The union of a subtype P with its complement is the full subtype if and only if P is a decidable subtype

module _
{l1 l2 : Level} {A : UU l1}
where

is-full-union-subtype-complement-subtype :
(P : subtype l2 A) → is-decidable-subtype P →
is-full-subtype (union-subtype P (complement-subtype P))
is-full-union-subtype-complement-subtype P d x =
unit-trunc-Prop (d x)

is-decidable-subtype-is-full-union-subtype-complement-subtype :
(P : subtype l2 A) →
is-full-subtype (union-subtype P (complement-subtype P)) →
is-decidable-subtype P
is-decidable-subtype-is-full-union-subtype-complement-subtype P H x =
apply-universal-property-trunc-Prop
( H x)
( is-decidable-Prop (P x))
( id)

is-full-union-subtype-complement-decidable-subtype :
(P : decidable-subtype l2 A) →
is-full-decidable-subtype
( union-decidable-subtype P (complement-decidable-subtype P))
is-full-union-subtype-complement-decidable-subtype P =
is-full-union-subtype-complement-subtype
( subtype-decidable-subtype P)
( is-decidable-decidable-subtype P)