Martin Escardo, 31st March 2023

In collaboration with Marc Bezem, Thierry Coquand, Peter Dybjer.

\begin{code}

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

module UF.SmallnessProperties where

open import MLTT.List
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import MLTT.Two-Properties
open import NotionsOfDecidability.Decidable
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.PropTrunc
open import UF.Size

smallness-closed-under-≃ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                         β†’ X is 𝓦 small
                         β†’ X ≃ Y
                         β†’ Y is 𝓦 small
smallness-closed-under-≃ (X' , 𝕗) π•˜ = X' , (𝕗 ● π•˜)

smallness-closed-under-≃' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                          β†’ X is 𝓦 small
                          β†’ Y ≃ X
                          β†’ Y is 𝓦 small
smallness-closed-under-≃' s π•˜ = smallness-closed-under-≃ s (≃-sym π•˜)

Ξ£-is-small : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
           β†’ X is 𝓀' small
           β†’ ((x : X) β†’ A x is π“₯' small)
           β†’ Ξ£ A is 𝓀' βŠ” π“₯' small
Ξ£-is-small {𝓀} {π“₯} {𝓀'} {π“₯'} {X} {A} (X' , 𝕗) Οƒ = Ξ³
 where
  A' : X β†’ π“₯' Μ‡
  A' x = resized (A x) (Οƒ x)

  π•˜ : (x : X) β†’ A' x ≃ A x
  π•˜ x = resizing-condition (Οƒ x)

  Ξ³ : (Ξ£ A) is 𝓀' βŠ” π“₯' small
  Ξ³ = (Ξ£ (A' ∘ ⌜ 𝕗 ⌝)) , Ξ£-bicong (A' ∘ ⌜ 𝕗 ⌝) A 𝕗 (Ξ» x β†’ π•˜ (⌜ 𝕗 ⌝ x))

Ξ -is-small : FunExt
           β†’ {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
           β†’ X is 𝓀' small
           β†’ ((x : X) β†’ A x is π“₯' small)
           β†’ Ξ  A is 𝓀' βŠ” π“₯' small
Ξ -is-small {𝓀} {π“₯} {𝓀'} {π“₯'} fe {X} {A} (X' , 𝕗) Οƒ = Ξ³
 where
  A' : X β†’ π“₯' Μ‡
  A' x = resized (A x) (Οƒ x)

  π•˜ : (x : X) β†’ A' x ≃ A x
  π•˜ x = resizing-condition (Οƒ x)

  Ξ³ : (Ξ  A) is 𝓀' βŠ” π“₯' small
  Ξ³ = (Ξ  (A' ∘ ⌜ 𝕗 ⌝)) ,
      Ξ -bicong fe (A' ∘ ⌜ 𝕗 ⌝) A 𝕗 (Ξ» x β†’ π•˜ (⌜ 𝕗 ⌝ x))

decidable-embeddings-have-any-size : (𝓦 : Universe)
                                     {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f : X β†’ Y}
                                   β†’ is-embedding f
                                   β†’ each-fiber-of f is-decidable
                                   β†’ f is 𝓦 small-map
decidable-embeddings-have-any-size 𝓦 {X} {Y} {f} e Ξ΄ y =
 decidable-propositions-have-any-size (fiber f y) (e y) (Ξ΄ y)

id-has-any-size : (𝓦 : Universe) {X : 𝓀 Μ‡ } β†’ id {𝓀} {X} is 𝓦 small-map
id-has-any-size 𝓦 {𝓀} = equivs-have-any-size id (id-is-equiv 𝓀)

∘-decidable-embeddings : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                         {f : X β†’ Y} {g : Y β†’ Z}
                       β†’ is-embedding g
                       β†’ each-fiber-of f is-decidable
                       β†’ each-fiber-of g is-decidable
                       β†’ each-fiber-of (g ∘ f) is-decidable
∘-decidable-embeddings {𝓀} {π“₯} {𝓦} {X} {Y} {Z} {f} {g} ge Οƒ Ο„ z = Ξ³
 where
  Ξ΄ : is-decidable (Ξ£ (y , _) κž‰ fiber g z , fiber f y)
  Ξ΄ = decidable-closed-under-Ξ£ (ge z) (Ο„ z) (Ξ» (y , _) β†’ Οƒ y)

  γ : is-decidable (fiber (g ∘ f) z)
  Ξ³ = decidability-is-closed-under-≃ (≃-sym (fiber-of-composite f g z)) Ξ΄

∘-small-maps : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
               {f : X β†’ Y} {g : Y β†’ Z}
             β†’ f is 𝓣 small-map
             β†’ g is 𝓣' small-map
             β†’ (g ∘ f) is 𝓣 βŠ” 𝓣' small-map
∘-small-maps {𝓀} {π“₯} {𝓦} {𝓣} {𝓣'} {X} {Y} {Z} {f} {g} Οƒ Ο„ z = Ξ³
 where
  A : Y β†’ 𝓣 Μ‡
  A y = resized (fiber f y) (Οƒ y)

  Ο† : (y : Y) β†’ A y ≃ fiber f y
  Ο† y = resizing-condition (Οƒ y)

  B : 𝓣' Μ‡
  B = resized (fiber g z) (Ο„ z)

  ψ : B ≃ fiber g z
  ψ = resizing-condition (Ο„ z)

  Ξ΄ = (Ξ£ b κž‰ B , A (pr₁ (⌜ ψ ⌝ b)))       β‰ƒβŸ¨ I ⟩
      (Ξ£ (y , _) κž‰ fiber g z , A y)       β‰ƒβŸ¨ II ⟩
      (Ξ£ (y , _) κž‰ fiber g z , fiber f y) β‰ƒβŸ¨ III ⟩
      fiber (g ∘ f) z                     β– 
      where
       I   = Ξ£-change-of-variable-≃ (A ∘ pr₁) ψ
       II  = Ξ£-cong (Ο† ∘ pr₁)
       III = ≃-sym (fiber-of-composite f g z)

  Ξ³ : fiber (g ∘ f) z is 𝓣 βŠ” 𝓣' small
  γ = domain ⌜ δ ⌝ , δ

NatΞ£-is-small : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
                (Ο„ : Nat A B)
              β†’ ((x : X) β†’ Ο„ x is 𝓣 small-map)
              β†’ NatΞ£ Ο„ is 𝓣 small-map
NatΞ£-is-small {𝓀} {π“₯} {𝓦} {𝓣} {X} {A} {B} Ο„ Ο„-small = Ξ³
 where
  F : (x : X) β†’ B x β†’ 𝓣 Μ‡
  F x b = resized (fiber (Ο„ x) b) (Ο„-small x b)

  Ξ³ : NatΞ£ Ο„ is 𝓣 small-map
  Ξ³ (x , b) = F x b ,
             (F x b                  β‰ƒβŸ¨ resizing-condition (Ο„-small x b) ⟩
              fiber (Ο„ x) b          β‰ƒβŸ¨ NatΞ£-fiber-equiv A B Ο„ x b ⟩
              fiber (NatΞ£ Ο„) (x , b) β– )

inl-has-any-size : (𝓦 : Universe) {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                 β†’ inl {𝓀} {π“₯} {X} {Y} is 𝓦 small-map
inl-has-any-size 𝓦 =
 decidable-embeddings-have-any-size 𝓦 (inl-is-embedding _ _) Ξ³
 where
  Ξ³ : each-fiber-of inl is-decidable
  Ξ³ (inl x) = inl (x , refl)
  Ξ³ (inr y) = inr (Ξ» ((x , p) : fiber inl (inr y)) β†’ +disjoint p)

inr-has-any-size : (𝓦 : Universe) {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                 β†’ inr {𝓀} {π“₯} {X} {Y} is 𝓦 small-map
inr-has-any-size 𝓦 =
 decidable-embeddings-have-any-size 𝓦 (inr-is-embedding _ _) Ξ³
 where
  Ξ³ : each-fiber-of inr is-decidable
  Ξ³ (inl x) = inr (Ξ» ((y , p) : fiber inr (inl x)) β†’ +disjoint' p)
  Ξ³ (inr y) = inl (y , refl)

pairβ‚€ : {X : 𝓀 Μ‡ } β†’ X β†’ 𝟚 Γ— X
pairβ‚€ x = (β‚€ , x)

pairβ‚€-is-embedding : {X : 𝓀 Μ‡ } β†’ is-embedding (pairβ‚€ {𝓀} {X})
pairβ‚€-is-embedding (β‚€ , x) (x , refl) (x , refl) = refl

pairβ‚€-is-decidable : {X : 𝓀 Μ‡ } β†’ each-fiber-of (pairβ‚€ {𝓀} {X}) is-decidable
pairβ‚€-is-decidable (β‚€ , x) = inl (x , refl)
pairβ‚€-is-decidable (₁ , x) = inr (Ξ» (y , p) β†’ zero-is-not-one (ap pr₁ p))

pairβ‚€-has-any-size : (𝓦 : Universe) {X : 𝓀 Μ‡ } β†’ (pairβ‚€ {𝓀} {X}) is 𝓦 small-map
pairβ‚€-has-any-size 𝓦 = decidable-embeddings-have-any-size 𝓦
                         pairβ‚€-is-embedding
                         pairβ‚€-is-decidable

[]-is-embedding : {X : 𝓀 Μ‡ } β†’ is-embedding (Ξ» (x : X) β†’ [ x ])
[]-is-embedding (x ∷ []) (x , refl) (x , refl) = refl

[]-is-decidable : {X : 𝓀 Μ‡ } β†’ each-fiber-of (Ξ» (x : X) β†’ [ x ]) is-decidable
[]-is-decidable {𝓀} {X} [] =
  inr (Ξ» (x , p) β†’ []-is-not-cons x [] (p ⁻¹))
[]-is-decidable {𝓀} {X} (x ∷ []) =
  inl (x , refl)
[]-is-decidable {𝓀} {X} (xβ‚€ ∷ x₁ ∷ xs) =
  inr Ξ» (x , p) β†’ []-is-not-cons x₁ xs (equal-tails p)

[]-has-any-size : (𝓦 : Universe) {X : 𝓀 Μ‡ } β†’ (Ξ» (x : X) β†’ [ x ]) is 𝓦 small-map
[]-has-any-size 𝓦 = decidable-embeddings-have-any-size 𝓦
                      []-is-embedding
                      []-is-decidable


module _ (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt

 βˆ₯βˆ₯-is-small : {X : 𝓀 Μ‡ }
             β†’ X is 𝓦 small
             β†’ βˆ₯ X βˆ₯ is 𝓦 small
 βˆ₯βˆ₯-is-small (X' , 𝕗) = βˆ₯ X' βˆ₯ ,
                       qinveq (βˆ₯βˆ₯-functor ⌜ 𝕗 ⌝)
                        (βˆ₯βˆ₯-functor ⌜ 𝕗 ⌝⁻¹ ,
                         (Ξ» _ β†’ βˆ₯βˆ₯-is-prop _ _) ,
                         (Ξ» _ β†’ βˆ₯βˆ₯-is-prop _ _))

\end{code}

Added by Martin Escardo and Tom de Jong 14th November 2024.

\begin{code}

open import UF.UA-FunExt
open import UF.Univalence

Id-is-small : is-univalent 𝓀
            β†’ funext 𝓀 (𝓀 ⁺)
            β†’ (X : 𝓀 Μ‡ )
            β†’ (Id {𝓀} {X}) is 𝓀 small-map
Id-is-small {𝓀} ua fe⁺ X A =
 (Ξ£ x κž‰ X , (Ξ  y κž‰ X , (x ＝ y) ≃ A y)) ,
 ((Ξ£ x κž‰ X , (Ξ  y κž‰ X , (x ＝ y) ≃ A y))  β‰ƒβŸ¨ I ⟩
  (Ξ£ x κž‰ X , (Ξ  y κž‰ X , (x ＝ y) ＝ A y)) β‰ƒβŸ¨ II ⟩
  fiber Id A                              β– )
   where
    fe : funext 𝓀 𝓀
    fe = univalence-gives-funext ua

    I  = Ξ£-cong (Ξ» x β†’ Ξ -cong fe fe⁺ (Ξ» y β†’ ≃-sym (univalence-≃ ua _ _)))
    II = Ξ£-cong (Ξ» x β†’ ≃-sym (≃-funext fe⁺ _ _))

\end{code}