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}