# Finite choice

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

Created on 2022-02-13.

module univalent-combinatorics.finite-choice where

Imports
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.well-ordering-principle-standard-finite-types

open import foundation.coproduct-types
open import foundation.decidable-embeddings
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.empty-types
open import foundation.equivalences
open import foundation.fiber-inclusions
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.hilberts-epsilon-operators
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.unit-type
open import foundation.universal-property-coproduct-types
open import foundation.universal-property-unit-type
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.counting-decidable-subtypes
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types


## Idea

Propositional truncations distributes over finite products.

## Theorems

abstract
finite-choice-Fin :
{l1 : Level} (k : ℕ) {Y : Fin k → UU l1} →
((x : Fin k) → type-trunc-Prop (Y x)) → type-trunc-Prop ((x : Fin k) → Y x)
finite-choice-Fin {l1} zero-ℕ {Y} H = unit-trunc-Prop ind-empty
finite-choice-Fin {l1} (succ-ℕ k) {Y} H =
map-inv-equiv-trunc-Prop
( equiv-dependent-universal-property-coproduct Y)
( map-inv-distributive-trunc-product-Prop
( pair
( finite-choice-Fin k (λ x → H (inl x)))
( map-inv-equiv-trunc-Prop
( equiv-dependent-universal-property-unit (Y ∘ inr))
( H (inr star)))))

abstract
finite-choice-count :
{l1 l2 : Level} {X : UU l1} {Y : X → UU l2} → count X →
((x : X) → type-trunc-Prop (Y x)) → type-trunc-Prop ((x : X) → Y x)
finite-choice-count {l1} {l2} {X} {Y} (pair k e) H =
map-inv-equiv-trunc-Prop
( equiv-precomp-Π e Y)
( finite-choice-Fin k (λ x → H (map-equiv e x)))

abstract
finite-choice :
{l1 l2 : Level} {X : UU l1} {Y : X → UU l2} → is-finite X →
((x : X) → type-trunc-Prop (Y x)) → type-trunc-Prop ((x : X) → Y x)
finite-choice {l1} {l2} {X} {Y} is-finite-X H =
apply-universal-property-trunc-Prop is-finite-X
( trunc-Prop ((x : X) → Y x))
( λ e → finite-choice-count e H)

abstract
ε-operator-count :
{l : Level} {A : UU l} → count A → ε-operator-Hilbert A
ε-operator-count (pair zero-ℕ e) t =
ex-falso
( is-empty-type-trunc-Prop
( is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl)
( t))
ε-operator-count (pair (succ-ℕ k) e) t = map-equiv e (zero-Fin k)

abstract
ε-operator-decidable-subtype-count :
{l1 l2 : Level} {A : UU l1} (e : count A) (P : decidable-subtype l2 A) →
ε-operator-Hilbert (type-decidable-subtype P)
ε-operator-decidable-subtype-count e P =
ε-operator-equiv
( equiv-Σ-equiv-base (is-in-decidable-subtype P) (equiv-count e))
( ε-operator-decidable-subtype-Fin
( number-of-elements-count e)
( λ x → P (map-equiv-count e x)))

abstract
ε-operator-emb-count :
{l1 l2 : Level} {A : UU l1} (e : count A) {B : UU l2} →
(f : B ↪ᵈ A) → ε-operator-Hilbert B
ε-operator-emb-count e f t =
map-equiv-total-fiber
( map-decidable-emb f)
( ε-operator-decidable-subtype-count e
( decidable-subtype-decidable-emb f)
( map-trunc-Prop
( map-inv-equiv-total-fiber (map-decidable-emb f))
( t)))

abstract
choice-count-Σ-is-finite-fiber :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
is-set A → count (Σ A B) → ((x : A) → is-finite (B x)) →
((x : A) → type-trunc-Prop (B x)) → (x : A) → B x
choice-count-Σ-is-finite-fiber {l1} {l2} {A} {B} K e g H x =
ε-operator-count
( count-domain-emb-is-finite-domain-emb e
( fiber-inclusion-emb (pair A K) B x)
( g x))
( H x)

abstract
choice-is-finite-Σ-is-finite-fiber :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
is-set A → is-finite (Σ A B) → ((x : A) → is-finite (B x)) →
((x : A) → type-trunc-Prop (B x)) → type-trunc-Prop ((x : A) → B x)
choice-is-finite-Σ-is-finite-fiber {l1} {l2} {A} {B} K f g H =
apply-universal-property-trunc-Prop f
( trunc-Prop ((x : A) → B x))
( λ e → unit-trunc-Prop (choice-count-Σ-is-finite-fiber K e g H))