# Finite function types

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

Created on 2022-03-31.

module univalent-combinatorics.function-types where

Imports
open import foundation.equivalences
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

count-function-type :
{l1 l2 : Level} {A : UU l1} {B : UU l2} →
count A → count B → count (A → B)
count-function-type e f =
count-Π e (λ x → f)


### 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)

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


### The type of equivalences between finite types is finite

abstract
is-finite-≃ :
{l1 l2 : Level} {A : UU l1} {B : UU l2} →
is-finite A → is-finite B → is-finite (A ≃ B)
is-finite-≃ f g =
is-finite-Σ
( is-finite-function-type f g)
( λ h →
is-finite-prod
( 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} → 𝔽 l1 → 𝔽 l2 → 𝔽 (l1 ⊔ l2)
pr1 (A ≃-𝔽 B) = type-𝔽 A ≃ type-𝔽 B
pr2 (A ≃-𝔽 B) = is-finite-≃ (is-finite-type-𝔽 A) (is-finite-type-𝔽 B)


### The type of automorphisms on a finite type is finite

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