Martin Escardo, 23rd June 2021

The type of finite types is universe invariant.

After a discussion with Ulrik Buchholtz and Peter Lumsdaine.

There is also a proof in Egbert Rijke's book (to appear).

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import Fin.Bishop
open import Fin.Type
open import MLTT.Spartan
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.PairFun
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.UA-FunExt
open import UF.Univalence
open import UF.UniverseEmbedding

module Fin.UniverseInvariance
        (pt : propositional-truncations-exist)
        (ua : Univalence)
       where

fe : Fun-Ext
fe = Univalence-gives-Fun-Ext ua

open PropositionalTruncation pt
open import UF.ImageAndSurjection pt
open finiteness pt

module constructions (Xβ‚€ : 𝓀₀ Μ‡ ) where

  A : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
  A 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , βˆ₯ X ≃ Xβ‚€ βˆ₯

\end{code}

Recall that Lift : (π“₯ : Universe) β†’ 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡ is the unique map with
Lift π“₯ X ≃ X, and that Lift π“₯ is an embedding of the universe 𝓀 into
the universe 𝓀 βŠ” π“₯, meaning that it has subsingleton fibers. This
relies on univalence, which we are assuming in this file.

\begin{code}

  Ξ΄ : (𝓀 : Universe) β†’ (X : 𝓀₀ Μ‡ ) β†’ βˆ₯ X ≃ Xβ‚€ βˆ₯ β†’ βˆ₯ Lift 𝓀 X ≃ Xβ‚€ βˆ₯
  Ξ΄ 𝓀 X = βˆ₯βˆ₯-functor (Ξ» (e : X ≃ Xβ‚€) β†’ Lift-≃ 𝓀 X ● e)

  Ξ΄-is-embedding : (X : 𝓀₀ Μ‡ ) β†’ is-embedding (Ξ΄ 𝓀 X)
  Ξ΄-is-embedding {𝓀} X = maps-of-props-are-embeddings (Ξ΄ 𝓀 X) βˆ₯βˆ₯-is-prop βˆ₯βˆ₯-is-prop

  Ο• : (𝓀 : Universe) β†’ A 𝓀₀ β†’ A 𝓀
  Ο• 𝓀 (X , s) = Lift 𝓀 X , Ξ΄ 𝓀 X s

  Ο•-is-embedding : is-embedding (Ο• 𝓀)
  Ο•-is-embedding {𝓀} = pair-fun-is-embedding
                        (Lift 𝓀) (Ξ΄ 𝓀)
                        (Lift-is-embedding ua) Ξ΄-is-embedding

  Ο•-is-surjection : is-surjection (Ο• 𝓀)
  Ο•-is-surjection {𝓀} (Y , t) = g
   where
    f : Y ≃ Xβ‚€ β†’ Ξ£ (X , s) κž‰ A 𝓀₀ , (Lift 𝓀 X , Ξ΄ 𝓀 X s) ＝ (Y , t)
    f e = (Xβ‚€ , ∣ ≃-refl Xβ‚€ ∣) , q

     where
      d = Lift 𝓀 Xβ‚€ β‰ƒβŸ¨ Lift-≃ 𝓀 Xβ‚€ ⟩
          Xβ‚€        β‰ƒβŸ¨ ≃-sym e ⟩
          Y         β– 

      p : Lift 𝓀 Xβ‚€ ＝ Y
      p = eqtoid (ua 𝓀) _ _ d

      q : (Lift 𝓀 Xβ‚€ , Ξ΄ 𝓀 Xβ‚€ ∣ ≃-refl Xβ‚€ ∣) ＝ (Y , t)
      q = to-subtype-＝ (Ξ» X β†’ βˆ₯βˆ₯-is-prop) p


    g : βˆƒ (X , s) κž‰ A 𝓀₀ , (Lift 𝓀 X , Ξ΄ 𝓀 X s) ＝ (Y , t)
    g = βˆ₯βˆ₯-functor f t

  Ο•-is-equiv : is-equiv (Ο• 𝓀)
  Ο•-is-equiv {𝓀} = surjective-embeddings-are-equivs (Ο• 𝓀) Ο•-is-embedding Ο•-is-surjection

  lemmaβ‚€ : (𝓀 : Universe) β†’ A 𝓀₀ ≃ A 𝓀
  lemmaβ‚€ 𝓀 = Ο• 𝓀 , Ο•-is-equiv

  lemma : A 𝓀 ≃ A π“₯
  lemma {𝓀} {π“₯} = ≃-sym (lemmaβ‚€ 𝓀) ● lemmaβ‚€ π“₯


Finite : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Finite 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , is-finite X

Finite-is-universe-independent : Finite 𝓀 ≃ Finite π“₯
Finite-is-universe-independent {𝓀} {π“₯} =
  (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ n κž‰ β„• , βˆ₯ X ≃ Fin n βˆ₯) β‰ƒβŸ¨ Ξ£-flip ⟩
  (Ξ£ n κž‰ β„• , Ξ£ X κž‰ 𝓀 Μ‡ , βˆ₯ X ≃ Fin n βˆ₯) β‰ƒβŸ¨ Ξ£-cong (Ξ» n β†’ constructions.lemma (Fin n)) ⟩
  (Ξ£ n κž‰ β„• , Ξ£ Y κž‰ π“₯ Μ‡ , βˆ₯ Y ≃ Fin n βˆ₯) β‰ƒβŸ¨ Ξ£-flip ⟩
  (Ξ£ Y κž‰ π“₯ Μ‡ , Ξ£ n κž‰ β„• , βˆ₯ Y ≃ Fin n βˆ₯) β– 

finite-types-are-lifts : (X : 𝓀 Μ‡ ) β†’ is-finite X β†’ Ξ£ Xβ‚€ κž‰ 𝓀₀ Μ‡ , Lift 𝓀 Xβ‚€ ＝ X
finite-types-are-lifts {𝓀} X (n , s) = Xβ‚€ , p
 where
  open constructions (Fin n)

  Xβ‚€ : 𝓀₀ Μ‡
  Xβ‚€ = pr₁ (inverse (Ο• 𝓀) Ο•-is-equiv (X , s))

  p : Lift 𝓀 Xβ‚€ ＝ X
  p = ap pr₁ (inverses-are-sections (Ο• 𝓀) Ο•-is-equiv (X , s))

\end{code}