Equivalences between finite types

module univalent-combinatorics.equivalences where

open import foundation.equivalences public

open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import univalent-combinatorics.embeddings
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.surjective-maps

Properties

For a map between finite types, being an equivalence is decidable

is-decidable-is-equiv-is-finite :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  is-finite A → is-finite B → is-decidable (is-equiv f)
is-decidable-is-equiv-is-finite f HA HB =
  is-decidable-iff
    ( λ p → is-equiv-is-emb-is-surjective (pr1 p) (pr2 p))
    ( λ K → pair (is-surjective-is-equiv K) (is-emb-is-equiv K))
    ( is-decidable-prod
      ( is-decidable-is-surjective-is-finite f HA HB)
      ( is-decidable-is-emb-is-finite f HA HB))