index ∙ source

open import Cat.Functor.Base
open import Cat.Functor.Equivalence
open import Cat.Functor.FullSubcategory
open import Cat.Functor.Properties
open import Cat.Instances.FinSets
open import Cat.Instances.Sets
open import Cat.Prelude
open import Cat.Skeletal
open import Data.Bool
open import Data.Fin
open import Data.Nat

import Cat.Reasoning

open Functor
open is-precat-iso

module Skeletons where

module Sets {ℓ} = Cat.Reasoning (Sets ℓ)

Formalising parts of this math.SE answer, with finite-dimensional real vector spaces replaced with finite sets; the situation is entirely analogous.

Instead of the skeletal category whose objects are natural numbers representing $ℝⁿ$ and whose morphisms are linear maps, we use the skeletal category whose objects are natural numbers representing the standard finite sets $[n]$ and whose morphisms are functions.

S : Precategory lzero lzero
S = FinSets

S-is-skeletal : is-skeletal S
S-is-skeletal = FinSets-is-skeletal

Instead of the univalent category of finite-dimensional real vector spaces, we use the univalent category of finite sets, here realised as the essential image $C$ of the inclusion of $S$ into sets. Explicitly, an object of $C$ is a set $X$ such that there merely exists a natural number $n$ such that $X ≃ [n]$. Equivalently, an object of $C$ is a set $X$ equipped with a natural number $n$ such that $∥ X ≃ [n] ∥$ (we can extract $n$ from the truncation because the statements $X ≃ [n]$ are mutually exclusive for distinct $n$).

$C$ is a Rezk completion of $S$.

C : Precategory (lsuc lzero) lzero
C = Essential-image Fin→Sets

C-is-category : is-category C
C-is-category = Essential-image-is-category Fin→Sets Sets-is-category

If we remove the truncation (but do not change the morphisms), we get a skeletal category isomorphic to $S$, because we can contract $X$ away. This is entirely analogous to the way that the naïve definition of the image of a function using $Σ$ instead of $∃$ yields the domain of the function.

C' : Precategory (lsuc lzero) lzero
C' = Restrict {C = Sets _} λ X → Σ[ n ∈ Nat ] Fin→Sets .F₀ n Sets.≅ X

S→C' : Functor S C'
S→C' .F₀ n = el! (Fin n) , n , Sets.id-iso
S→C' .F₁ f = f
S→C' .F-id = refl
S→C' .F-∘ _ _ = refl

S≡C' : is-precat-iso S→C'
S≡C' .has-is-ff = id-equiv
S≡C' .has-is-iso = inverse-is-equiv (e .snd) where
  e : (Σ[ X ∈ Set lzero ] Σ[ n ∈ Nat ] Fin→Sets .F₀ n Sets.≅ X) ≃ Nat
  e = Σ-swap₂ ∙e Σ-contr-snd λ n → is-contr-ΣR Sets-is-category

Since $C$ is a Rezk completion of $S$, we should expect to have a fully faithful and essentially surjective functor $S → C$.

S→C : Functor S C
S→C = Essential-inc Fin→Sets

S→C-is-ff : is-fully-faithful S→C
S→C-is-ff = ff→Essential-inc-ff Fin→Sets Fin→Sets-is-ff

S→C-is-eso : is-eso S→C
S→C-is-eso = Essential-inc-eso Fin→Sets

However, this functor is not an equivalence of categories: in order to obtain a functor going the other way, we would have to choose an enumeration of every finite set in a coherent way. This is a form of global choice, which is just false in homotopy type theory.

module _ (S≃C : is-equivalence S→C) where private
  open is-equivalence S≃C renaming (F⁻¹ to C→S)
  module C = Cat.Reasoning C

  module _ (X : Set lzero) (e : ∥ ⌞ X ⌟ ≃ Fin  ∥) where
    c : C.Ob
    c = X , ((λ e →  , equiv→iso (e e⁻¹)) <$> e)

    chosen : ⌞ X ⌟
    chosen with C→S .F₀ c | counit.ε c | counit-iso c
    ... | suc n | ε | _ = ε 
    ... | zero  | ε | ε-inv = absurd (case e of λ e →
      zero≠suc (Fin-injective (iso→equiv (sub-iso→super-iso _ (C.invertible→iso ε ε-inv)) ∙e e)))

  b : Bool
  b = chosen (el! Bool) enumeration

  swap : Bool ≡ Bool
  swap = ua (not , not-is-equiv)

  p : PathP (λ i → swap i) b b
  p = ap₂ chosen (n-ua _) prop!

  ¬S≃C : ⊥
  ¬S≃C = not-no-fixed (from-pathp⁻ p)

Alternatively, an equivalence $S \simeq C$ would imply that $C$ is strict (see SetsCover), but the category of finite sets is of course not gaunt.