Injective maps between finite types

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

Created on 2022-02-14.
Last modified on 2023-06-07.

module univalent-combinatorics.injective-maps where

open import foundation.injective-maps public
open import foundation.decidable-types
open import foundation.identity-types
open import foundation.universe-levels

open import univalent-combinatorics.decidable-dependent-function-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types


Injectiveness in the context of finite types enjoys further properties.


is-decidable-is-injective-is-finite' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  is-finite A  is-finite B  is-decidable ((x y : A)  Id (f x) (f y)  Id x y)
is-decidable-is-injective-is-finite' f HA HB =
  is-decidable-Π-is-finite HA
    ( λ x 
      is-decidable-Π-is-finite HA
        ( λ y 
            ( has-decidable-equality-is-finite HB (f x) (f y))
            ( has-decidable-equality-is-finite HA x y)))

is-decidable-is-injective-is-finite :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  is-finite A  is-finite B  is-decidable (is-injective f)
is-decidable-is-injective-is-finite f HA HB =
    ( λ p {x} {y}  p x y)
    ( λ p x y  p)
    ( is-decidable-is-injective-is-finite' f HA HB)

Recent changes