Martin Escardo 2011. \begin{code} {-# OPTIONS --safe --without-K #-} module NotionsOfDecidability.Complemented where open import MLTT.Spartan open import MLTT.Plus-Properties open import NotionsOfDecidability.Decidable \end{code} We again have a particular case of interest. Complemented subsets, defined below, are often known as decidable subsets. Agda doesn't allow overloading of terminology, and hence we gladly accept the slighly non-universal terminology. \begin{code} is-complemented : {X : ๐ค ฬ } (A : X โ ๐ฅ ฬ ) โ ๐ค โ ๐ฅ ฬ is-complemented A = โ x โ is-decidable (A x) characteristic-function : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } โ is-complemented A โ ฮฃ p ๊ (X โ ๐) , ((x : X) โ (p x ๏ผ โ โ A x) ร (p x ๏ผ โ โ ยฌ (A x))) characteristic-function = indicator co-characteristic-function : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } โ is-complemented A โ ฮฃ p ๊ (X โ ๐) , ((x : X) โ (p x ๏ผ โ โ ยฌ (A x)) ร (p x ๏ผ โ โ A x)) co-characteristic-function d = indicator(ฮป x โ +-commutative(d x)) \end{code} Added by Fredrik Bakke on the 26th of March 2025. We define a complemented map f to be a map such that each fiber is decidable. \begin{code} is-complemented-map : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ (X โ Y) โ ๐ค โ ๐ฅ ฬ is-complemented-map f = each-fiber-of f is-decidable โ-complemented-map : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {Z : ๐ฆ ฬ } (f : X โ Y) (g : Y โ Z) โ left-cancellable g โ is-complemented-map g โ is-complemented-map f โ is-complemented-map (g โ f) โ-complemented-map f g H G F x = cases positive-case negative-case (G x) where positive-case : fiber g x โ is-decidable (fiber (g โ f) x) positive-case (y , q) = decidable-โ ((ฮป (x , p) โ x , (ap g p โ q)) , (ฮป (x , r) โ x , H (r โ q โปยน))) (F y) negative-case : ยฌ (fiber g x) โ is-decidable (fiber (g โ f) x) negative-case nu = inr (ฮป (x , p) โ nu (f x , p)) \end{code}