Size

Martin Escardo, July 2026.

Size notions for setoids.

The point of the setoid view is that the identity type plays no role,
with sameness given by the setoid relation. Accordingly, a setoid is
locally small when its relation, rather than its identity type, is
small-valued. The motivating example is the universe with type
equivalence as its relation. Since X ≃ Y already lives in 𝓤, the
universe setoid is locally small with no univalence assumption,
whereas the identity type X ＝ Y is not small without something such
as univalence.

A setoid is small when it is isomorphic to a setoid whose underlying
type and equivalence relation are both small.


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

module EGroups.Size where

open import MLTT.Spartan
open import UF.Equiv
open import UF.Size

open import EGroups.Setoid


A setoid is locally 𝓦-small if each value of its relation is 𝓦-small.


has-small-valued-relation : (S : Setoid 𝓤 𝓥) (𝓦 : Universe) → 𝓦 ⁺ ⊔ 𝓤 ⊔ 𝓥 ̇
has-small-valued-relation S 𝓦 = (x y : ∣ S ∣) → (x ≈∣ S ∣ y) is 𝓦 small


We regard the universe as a setoid, with type equivalence as its
equivalence relation.


universe-setoid : (𝓤 : Universe) → Setoid (𝓤 ⁺) 𝓤
universe-setoid 𝓤 = (𝓤 ̇)
                  , _≃_
                  , ≃-refl
                  , (λ X Y → ≃-sym)
                  , (λ X Y Z → _●_)


Its relation is natively locally small. For X and Y in 𝓤 ̇, the type
X ≃ Y already lives in 𝓤, and no univalence is used.


universe-setoid-is-locally-small
 : (𝓤 : Universe) → has-small-valued-relation (universe-setoid 𝓤) 𝓤
universe-setoid-is-locally-small 𝓤 X Y = native-size (X ≃ Y)


A setoid is 𝓦-small if it is setoid-isomorphic to a setoid whose
underlying type and relation both live in 𝓦, and large if it is not.


is-small-setoid : (𝓦 : Universe) → Setoid 𝓤 𝓥 → 𝓦 ⁺ ⊔ 𝓤 ⊔ 𝓥 ̇
is-small-setoid 𝓦 S = Σ T ꞉ Setoid 𝓦 𝓦 , (S ≅ˢ T)

is-large-setoid : (𝓦 : Universe) → Setoid 𝓤 𝓥 → 𝓦 ⁺ ⊔ 𝓤 ⊔ 𝓥 ̇
is-large-setoid 𝓦 S = ¬ is-small-setoid 𝓦 S