# Surjective maps between finite types

```agda
module univalent-combinatorics.surjective-maps where

open import foundation.surjective-maps public
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.decidable-embeddings
open import foundation.decidable-equality
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.counting-decidable-subtypes
open import univalent-combinatorics.counting-dependent-pair-types
open import univalent-combinatorics.decidable-dependent-function-types
open import univalent-combinatorics.embeddings
open import univalent-combinatorics.fibers-of-maps
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types
```

</details>

## Definition

```agda
Surjection-𝔽 :
  {l1 : Level} (l2 : Level) → 𝔽 l1 → UU (l1 ⊔ lsuc l2)
Surjection-𝔽 l2 A =
  Σ (𝔽 l2) (λ B → (type-𝔽 A) ↠ (type-𝔽 B))
```

## Properties

```agda
is-decidable-is-surjective-is-finite :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  is-finite A → is-finite B → is-decidable (is-surjective f)
is-decidable-is-surjective-is-finite f HA HB =
  is-decidable-Π-is-finite HB
    ( λ y → is-decidable-type-trunc-Prop-is-finite (is-finite-fiber f HA HB y))
```

### If `X` has decidable equality and there exist a surjection `Fin-n ↠ X` then `X` has a counting

```agda
module _
  {l1 : Level} {X : UU l1}
  where

  count-surjection-has-decidable-equality :
    (n : ℕ) → (has-decidable-equality X) → (Fin n ↠ X) →
    count (X)
  count-surjection-has-decidable-equality n dec-X f =
    count-decidable-emb
      ( ( map-equiv
          ( equiv-precomp-decidable-emb-equiv
            ( inv-equiv
              ( right-unit-law-Σ-is-contr
                ( λ x →
                  is-proof-irrelevant-is-prop
                    ( is-prop-type-trunc-Prop)
                    ( is-surjective-map-surjection f x))))
            (Σ _ (fiber (pr1 f))))
          ( decidable-emb-tot-trunc-Prop-count
            { P = fiber (map-surjection f)}
            ( count-fiber-count-Σ
              dec-X
              ( count-equiv
                ( inv-equiv-total-fiber (map-surjection f)) (count-Fin n))))))
      ( count-equiv (inv-equiv-total-fiber (map-surjection f)) (count-Fin n))
```

### A type `X` is finite if and only if it has decidable equality and there exists a surjection from a finite type to `X`

```agda
  is-finite-if-∃-surjection-has-decidable-equality :
    is-finite X →
    ( has-decidable-equality X × type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X)))
  is-finite-if-∃-surjection-has-decidable-equality fin-X =
    apply-universal-property-trunc-Prop
      ( fin-X)
      ( product-Prop (has-decidable-equality-Prop X) (trunc-Prop _))
      ( λ count-X →
        ( has-decidable-equality-count count-X ,
          unit-trunc-Prop
          ( pr1 count-X ,
            ( map-equiv (pr2 count-X)) ,
            ( is-surjective-map-equiv (pr2 count-X)))))

  ∃-surjection-has-decidable-equality-if-is-finite :
    ( has-decidable-equality X × type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X))) →
    is-finite X
  ∃-surjection-has-decidable-equality-if-is-finite dec-X-surj =
    apply-universal-property-trunc-Prop
          ( pr2 dec-X-surj)
          ( is-finite-Prop X)
          ( λ n-surj →
            unit-trunc-Prop
              ( count-surjection-has-decidable-equality
                ( pr1 n-surj)
                ( pr1 dec-X-surj)
                ( pr2 n-surj)))

  is-finite-iff-∃-surjection-has-decidable-equality :
    is-finite X ≃
    ( has-decidable-equality X × type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X)))
  is-finite-iff-∃-surjection-has-decidable-equality =
    equiv-iff-is-prop
      ( is-prop-is-finite X)
      ( is-prop-product is-prop-has-decidable-equality is-prop-type-trunc-Prop)
      ( λ fin-X → is-finite-if-∃-surjection-has-decidable-equality fin-X)
      ( λ dec-X-surj →
        ∃-surjection-has-decidable-equality-if-is-finite dec-X-surj)
```