# Fibers of maps between finite types

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

Created on 2022-03-31.

module univalent-combinatorics.fibers-of-maps where

open import foundation.fibers-of-maps public

Imports
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.sums-of-natural-numbers

open import foundation.contractible-types
open import foundation.decidable-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sections
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.counting-dependent-pair-types
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.double-counting
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types


## Idea

The fibers of maps between finite types are finite.

## Properties

### If A and B can be counted, then the fibers of a map f : A → B can be counted

count-fiber :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
count A → count B → (y : B) → count (fiber f y)
count-fiber f count-A count-B =
count-fiber-count-Σ-count-base
( count-B)
( count-equiv' (equiv-total-fiber f) count-A)

abstract
sum-number-of-elements-count-fiber :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
(count-A : count A) (count-B : count B) →
Id
( sum-count-ℕ count-B
( λ x → number-of-elements-count (count-fiber f count-A count-B x)))
( number-of-elements-count count-A)
sum-number-of-elements-count-fiber f count-A count-B =
sum-number-of-elements-count-fiber-count-Σ count-B
( count-equiv' (equiv-total-fiber f) count-A)

abstract
double-counting-fiber :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (count-A : count A) →
(count-B : count B) (count-fiber-f : (y : B) → count (fiber f y)) (y : B) →
Id
( number-of-elements-count (count-fiber-f y))
( number-of-elements-count (count-fiber f count-A count-B y))
double-counting-fiber f count-A count-B count-fiber-f y =
double-counting (count-fiber-f y) (count-fiber f count-A count-B y)


### Fibers of maps between finite types are finite

abstract
is-finite-fiber :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y) →
is-finite X → is-finite Y → (y : Y) → is-finite (fiber f y)
is-finite-fiber f is-finite-X is-finite-Y y =
apply-universal-property-trunc-Prop
( is-finite-X)
( is-finite-Prop (fiber f y))
( λ H →
apply-universal-property-trunc-Prop
( is-finite-Y)
( is-finite-Prop (fiber f y))
( λ K → unit-trunc-Prop (count-fiber f H K y)))

fiber-𝔽 :
{l1 l2 : Level} (X : 𝔽 l1) (Y : 𝔽 l2) (f : type-𝔽 X → type-𝔽 Y) →
type-𝔽 Y → 𝔽 (l1 ⊔ l2)
pr1 (fiber-𝔽 X Y f y) = fiber f y
pr2 (fiber-𝔽 X Y f y) =
is-finite-fiber f (is-finite-type-𝔽 X) (is-finite-type-𝔽 Y) y

abstract
is-finite-fiber-map-section-family :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} (b : (x : A) → B x) →
is-finite (Σ A B) → ((x : A) → is-finite (B x)) →
(t : Σ A B) → is-finite (fiber (map-section-family b) t)
is-finite-fiber-map-section-family {l1} {l2} {A} {B} b f g (pair y z) =
is-finite-equiv'
( ( ( left-unit-law-Σ-is-contr
( is-contr-total-path' y)
( pair y refl)) ∘e
( inv-associative-Σ A
( λ x → Id x y)
( λ t → Id (tr B (pr2 t) (b (pr1 t))) z))) ∘e
( equiv-tot (λ x → equiv-pair-eq-Σ (pair x (b x)) (pair y z))))
( is-finite-eq (has-decidable-equality-is-finite (g y)))


### The fibers of maps between finite types are decidable

is-decidable-fiber-count :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
count A → count B → (y : B) → is-decidable (fiber f y)
is-decidable-fiber-count f count-A count-B y =
is-decidable-count (count-fiber f count-A count-B y)

is-decidable-fiber-Fin :
{k l : ℕ} (f : Fin k → Fin l) → (y : Fin l) → is-decidable (fiber f y)
is-decidable-fiber-Fin {k} {l} f y =
is-decidable-fiber-count f (count-Fin k) (count-Fin l) y


### If f : A → B and B is finite, then A is finite if and only if the fibers of f are finite

equiv-is-finite-domain-is-finite-fiber :
{l1 l2 : Level} {A : UU l1} →
(B : 𝔽 l2) (f : A → (type-𝔽 B)) →
((b : type-𝔽 B) → is-finite (fiber f b)) ≃ is-finite A
equiv-is-finite-domain-is-finite-fiber {A = A} B f =
equiv-prop
( is-prop-Π (λ b → is-prop-is-finite (fiber f b)))
( is-prop-is-finite A)
( λ P →
is-finite-equiv
( equiv-total-fiber f)
( is-finite-Σ (is-finite-type-𝔽 B) P))
( λ P → is-finite-fiber f P ( is-finite-type-𝔽 B))