Complements of type families

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

Created on 2022-02-13.
Last modified on 2023-08-23.

module foundation.complements where
open import foundation.dependent-pair-types
open import foundation.universe-levels

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


The complement of a type family B over A consists of the type of points in A at which B x is empty.

complement :
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2)  UU (l1  l2)
complement {l1} {l2} {A} B = Σ A (is-empty  B)

Recent changes