# Surjective maps between finite types

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

Created on 2022-02-15.

module univalent-combinatorics.surjective-maps where

open import foundation.surjective-maps public

Imports
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


## Definition

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


## Properties

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

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

  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)