# Fibers of maps between finite types

```agda
module univalent-combinatorics.fibers-of-maps where

open import foundation.fibers-of-maps public
```

<details><summary>Imports</summary>

```agda
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.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sections
open import foundation.torsorial-type-families
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
```

</details>

## 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

```agda
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

```agda
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
```

###

```agda
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-torsorial-Id' 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

```agda
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

```agda
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-iff-is-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))
```