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).

\begin{code}

{-# 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

\end{code}

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).

\begin{code}

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)

\end{code}

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.

\begin{code}

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

\end{code}

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

\begin{code}

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) ⟩ᵤ))

\end{code}

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

\begin{code}

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)

\end{code}