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}