The image of a map

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

Created on 2022-02-15.
Last modified on 2023-09-06.

module univalent-combinatorics.image-of-maps where

open import foundation.images public
open import foundation.decidable-equality
open import foundation.decidable-types
open import foundation.fibers-of-maps
open import foundation.propositional-truncations
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.universe-levels

open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}
  (K : is-finite A)

    is-finite-codomain :
      is-surjective f  has-decidable-equality B  is-finite B
    is-finite-codomain H d =
        ( is-set-has-decidable-equality d)
        ( H)
        ( is-finite-equiv' (equiv-total-fiber f) K)
        ( λ b  is-finite-Σ K  a  is-finite-eq d))

  is-finite-im :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} (K : is-finite A) 
    has-decidable-equality B  is-finite (im f)
  is-finite-im {f = f} K d =
    is-finite-codomain K
      ( is-surjective-map-unit-im f)
      ( λ x y 
          ( extensionality-type-subtype'  u  trunc-Prop (fiber f u)) x y)
          ( d (pr1 x) (pr1 y)))

Recent changes