Finite function types

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

Created on 2022-03-31.
Last modified on 2025-02-11.

module univalent-combinatorics.function-types where
Imports 
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.universe-levels

open import univalent-combinatorics.cartesian-product-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types

Properties

The type of functions between types equipped with a counting can be equipped with a counting

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  (c : count A) (d : count B)
  where

  count-function-type : count (A → B)
  count-function-type = count-Π c (λ _ → d)

  number-of-elements-count-function-type :
    number-of-elements-count count-function-type ＝
    exp-ℕ (number-of-elements-count d) (number-of-elements-count c)
  number-of-elements-count-function-type =
    number-of-elements-count-Π c (λ _ → d) ∙
    compute-constant-product-ℕ
      ( number-of-elements-count d)
      ( number-of-elements-count c)

The type of functions between finite types is finite

abstract
  is-finite-function-type :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-finite A → is-finite B → is-finite (A → B)
  is-finite-function-type f g = is-finite-Π f (λ x → g)

  number-of-elements-function-type :
    {l1 l2 : Level} {A : UU l1} {B : UU l2}
    (H : is-finite A) (K : is-finite B) →
    number-of-elements-is-finite (is-finite-function-type H K) ＝
    exp-ℕ (number-of-elements-is-finite K) (number-of-elements-is-finite H)
  number-of-elements-function-type H K =
    apply-twice-universal-property-trunc-Prop H K
      ( Id-Prop ℕ-Set _ _)
      ( λ c d →
        inv
          ( compute-number-of-elements-is-finite
            ( count-function-type c d)
            ( is-finite-function-type H K)) ∙
        number-of-elements-count-function-type c d ∙
        ap-binary
          ( exp-ℕ)
          ( compute-number-of-elements-is-finite d K)
          ( compute-number-of-elements-is-finite c H))

_→𝔽_ : {l1 l2 : Level} → Finite-Type l1 → Finite-Type l2 → Finite-Type (l1 ⊔ l2)
pr1 (A →𝔽 B) = type-Finite-Type A → type-Finite-Type B
pr2 (A →𝔽 B) =
  is-finite-function-type
    ( is-finite-type-Finite-Type A)
    ( is-finite-type-Finite-Type B)

The type of equivalences between finite types is finite

abstract
  is-finite-type-equiv :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-finite A → is-finite B → is-finite (A ≃ B)
  is-finite-type-equiv f g =
    is-finite-Σ
      ( is-finite-function-type f g)
      ( λ h →
        is-finite-product
          ( is-finite-Σ
            ( is-finite-function-type g f)
            ( λ k →
              is-finite-Π g
                ( λ y → is-finite-eq (has-decidable-equality-is-finite g))))
          ( is-finite-Σ
            ( is-finite-function-type g f)
            ( λ k →
              is-finite-Π f
                ( λ x → is-finite-eq (has-decidable-equality-is-finite f)))))

infix 6 _≃𝔽_
_≃𝔽_ : {l1 l2 : Level} → Finite-Type l1 → Finite-Type l2 → Finite-Type (l1 ⊔ l2)
pr1 (A ≃𝔽 B) = type-Finite-Type A ≃ type-Finite-Type B
pr2 (A ≃𝔽 B) =
  is-finite-type-equiv
    ( is-finite-type-Finite-Type A)
    ( is-finite-type-Finite-Type B)

The type of automorphisms on a finite type is finite

Aut-Finite-Type : {l : Level} → Finite-Type l → Finite-Type l
Aut-Finite-Type A = A ≃𝔽 A

Recent changes