UnivalentFamilies

Ian Ray. 28th August 2025.

Minor changes and merged into TypeToplogy in April 2026.

We define the notion of univalent family in terms of a reflexive graph image.
The terminology here is borrowed from "Reflexive graph lenses in univalent
foundations" by Jon Sterling (see ReflexiveGraphs.index for link).


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

module ReflexiveGraphs.UnivalentFamilies where

open import MLTT.Spartan
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Subsingletons
open import UF.Univalence
open import ReflexiveGraphs.Type
open import ReflexiveGraphs.Univalent


The reflexive graph image with carrier A, on a family B : A → Type, has edges
x ≈ y given by an equivalence between the fibers, that is B(x) ≃ B(y).


refl-graph-image : (A : 𝓤 ̇) → (A → 𝓣 ̇) → Refl-Graph 𝓤 𝓣
refl-graph-image {𝓤} {𝓣} A B = (A , I , II)
 where
  I : A → A → 𝓣 ̇
  I x y = B x ≃ B y
  II : (x : A) → I x x
  II x = ≃-refl (B x)

is-univalent-family : Σ A ꞉ 𝓤 ̇ , (A → 𝓣 ̇)
                    → 𝓤 ⊔ 𝓣 ̇
is-univalent-family (A , B) = is-univalent-refl-graph (refl-graph-image A B)


This definition is intentionally general and offers a robust theoretical
framework for working with universes. Concretely, if one were working directly
with the codes of a Tarski style universe presentation then a univalent family
could be a pair (𝓤 , El) consisting of the universe type and the decoding map
El : 𝓤 → Type. In Agda the user may operate as if universes where presented à
la Russel and thus the pair of interest is simply (𝓤 , id). But there are other
examples of univalent families of interest such as any h-level sub-universe
(e.g. (Prop, pr₁), (Set, pr₁)). Perhaps (ℕ , finset) offers a more non-standard
and interesting example for your consideration. 

We can give some equivalent characterizations of univalent family of types.


id-to-equiv-family : {A : 𝓤 ̇} {B : A → 𝓣 ̇}
                   → (x y : A)
                   → x ＝ y
                   → B x ≃ B y
id-to-equiv-family {_} {_} {A} {B} x y = id-to-edge (refl-graph-image A B) 

is-univalent-family-implies-id-to-equiv
 : {A : 𝓤 ̇} {B : A → 𝓣 ̇}
 → is-univalent-family (A , B)
 → (x y : A)
 → is-equiv (id-to-equiv-family x y)
is-univalent-family-implies-id-to-equiv {𝓤} {𝓣} {A} {B} is-ua-fam
 = prop-fans-implies-id-to-edge-equiv (refl-graph-image A B) is-ua-fam

id-to-equiv-family-implies-univalent-family
 : {A : 𝓤 ̇} {B : A → 𝓣 ̇}
 → ((x y : A) → is-equiv (id-to-equiv-family x y))
 → is-univalent-family (A , B)
id-to-equiv-family-implies-univalent-family {𝓤} {𝓣} {A} {B} is-equiv
 = id-to-edge-equiv-implies-prop-fans (refl-graph-image A B) is-equiv


We conclude by defining a univalent family of univalent reflexive graphs.


univalent-family-of-univalent-refl-graphs
 : {𝓦 𝓣 : Universe}
 → ((U , 𝓔) : Σ U ꞉ 𝓤 ̇ , (U → Univalent-Refl-Graph 𝓦 𝓣))
 → 𝓤 ⊔ 𝓦 ̇
univalent-family-of-univalent-refl-graphs (U , 𝓔)
 = is-univalent-refl-graph (refl-graph-image U (λ A → ⟨ (𝓔 A) ⟩ᵤ))


We observe that a univalent universe is a univalent family and thus a univalent
reflexive graph. 


universe-refl-graph : (𝓤 : Universe)
                    → Refl-Graph (𝓤 ⁺) 𝓤
universe-refl-graph 𝓤 = refl-graph-image (𝓤  ̇) id

module _ (𝓤 : Universe) (ua : is-univalent 𝓤) where

 univalent-universe-is-univalent-family : is-univalent-family ((𝓤  ̇) , id)
 univalent-universe-is-univalent-family X
  = singletons-are-props (equiv-to-singleton (I X)
     (singleton-types-are-singletons X))
  where
   I : (X : 𝓤 ̇) → (Σ Y ꞉ 𝓤 ̇ , X ≃ Y) ≃ (Σ Y ꞉ 𝓤 ̇ , X ＝ Y)
   I X = Σ-cong (λ - → ≃-sym (univalence-≃ ua X -))

 universe-univalent-refl-graph : Univalent-Refl-Graph (𝓤 ⁺) 𝓤
 universe-univalent-refl-graph
  = (universe-refl-graph 𝓤 , univalent-universe-is-univalent-family)