Ian Ray. 2nd September 2025.

Minor changes and merged into TypeTopology in February 2026.

We provide some equivalent descriptions of univalent reflexive graphs (see
index for references to Sterling, Buchholtz, etc.)

In this file we give some properties about fans (terminology borrowed from
Sterling), which are analogous to singletons up to the edge relation. Then we
provide some equivalent characterizations of univalent reflexive graphs. It is
worth noting that, although Sterling makes no choice for the defintion in his
paper, we are required to. There is good reason to go with the 'propositional
fans' definition as it simplifies many proofs later on.

\begin{code}

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

module ReflexiveGraphs.Univalent where

open import MLTT.Spartan
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.PropIndexedPiSigma
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-Properties
open import ReflexiveGraphs.Type

module _ (𝓐 : Refl-Graph 𝓀 π“₯) where

 fan : ⟨ 𝓐 ⟩ β†’ 𝓀 βŠ” π“₯ Μ‡
 fan x = Ξ£ y κž‰ ⟨ 𝓐 ⟩ , x β‰ˆβŸ¨ 𝓐 ⟩ y

 cofan : ⟨ 𝓐 ⟩ β†’ 𝓀 βŠ” π“₯ Μ‡
 cofan x = Ξ£ y κž‰ ⟨ 𝓐 ⟩ , y β‰ˆβŸ¨ 𝓐 ⟩ x

\end{code}

We show that propositional fans imply propositional cofans and vice versa.
The crux of the proofs is to observe that if (y , s) : cofan x for some x then
(x , s) : fan y, the rest amounts to shuffling data within sigma types.

It is worth noting that the proofs that follow were originally discovered as
a string of equivalences, but to witness the equivalence requires function
extensionality. The underlying maps of the equivalences are sufficient for the
proof to go through and thus we are able to avoid appeals to function
extensionality.

\begin{code}

 prop-fan-to-cofan : ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))
                   β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-prop (cofan x))
 prop-fan-to-cofan fan-prop = I ∼-refl
  where
   I =
    ((x : ⟨ 𝓐 ⟩) β†’ is-prop (cofan x))                                   β†βŸ¨ id ⟩
    ((x : ⟨ 𝓐 ⟩) β†’ ((y , s) (y' , t) : cofan x) β†’ (y , s) ＝ (y' , t))  β†βŸ¨ II ⟩
    ((x y : ⟨ 𝓐 ⟩) (s : y β‰ˆβŸ¨ 𝓐 ⟩ x) (y' : ⟨ 𝓐 ⟩) (t : y' β‰ˆβŸ¨ 𝓐 ⟩ x)
      β†’ (y , s) ＝ (y' , t))                                            β†βŸ¨ III ⟩
    ((y x : ⟨ 𝓐 ⟩) (s : y β‰ˆβŸ¨ 𝓐 ⟩ x) (y' : ⟨ 𝓐 ⟩) (t : y' β‰ˆβŸ¨ 𝓐 ⟩ x)
      β†’ (y , s) ＝ (y' , t))                                            β†βŸ¨ IV ⟩
    ((y : ⟨ 𝓐 ⟩) ((x , s) : fan y) (y' : ⟨ 𝓐 ⟩) (t : y' β‰ˆβŸ¨ 𝓐 ⟩ x)
      β†’ (y , s) ＝ (y' , t))                                            β†βŸ¨ V ⟩
    ((y y' : ⟨ 𝓐 ⟩) (t : y' β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ (y , β‰ˆ-refl 𝓐 y) ＝ (y' , t))   β†βŸ¨ VI ⟩
    ((y' y : ⟨ 𝓐 ⟩) (t : y' β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ (y , β‰ˆ-refl 𝓐 y) ＝ (y' , t))   β†βŸ¨ VII ⟩
    ((y' : ⟨ 𝓐 ⟩) ((y , t) : fan y') β†’ (y , β‰ˆ-refl 𝓐 y) ＝ (y' , t))    β†βŸ¨ VIII ⟩
    ((y' : ⟨ 𝓐 ⟩) β†’ (y' , β‰ˆ-refl 𝓐 y') ＝[ fan y' ] (y' , β‰ˆ-refl 𝓐 y')) β–’
    where
     II   = (Ξ» f x (y , s) (y' , t) β†’ f x y s y' t)
     III  = (Ξ» f x y β†’ f y x)
     IV   = (Ξ» f y x s y' t β†’ f y (x , s) y' t)
     V    = (Ξ» f y β†’ Ξ -proj⁻¹ (y , β‰ˆ-refl 𝓐 y) (fan-prop y) (f y))
     VI   = (Ξ» f y' y β†’ f y y')
     VII  = (Ξ» f y' y t β†’ f y' (y , t))
     VIII = (Ξ» _ y' β†’ Ξ -proj⁻¹ (y' , β‰ˆ-refl 𝓐 y') (fan-prop y') refl)

 prop-cofan-to-fan : ((x : ⟨ 𝓐 ⟩) β†’ is-prop (cofan x))
                   β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))
 prop-cofan-to-fan co-prop = I ∼-refl
  where
   I =
    ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))                                     β†βŸ¨ id ⟩
    ((x : ⟨ 𝓐 ⟩) β†’ ((y , s) (y' , t) : fan x) β†’ (y , s) ＝ (y' , t))    β†βŸ¨ II ⟩
    ((x y : ⟨ 𝓐 ⟩) (s : x β‰ˆβŸ¨ 𝓐 ⟩ y) (y' : ⟨ 𝓐 ⟩) (t : x β‰ˆβŸ¨ 𝓐 ⟩ y')
      β†’ (y , s) ＝ (y' , t))                                            β†βŸ¨ III ⟩
    ((y x : ⟨ 𝓐 ⟩) (s : x β‰ˆβŸ¨ 𝓐 ⟩ y) (y' : ⟨ 𝓐 ⟩) (t : x β‰ˆβŸ¨ 𝓐 ⟩ y')
      β†’ (y , s) ＝ (y' , t))                                            β†βŸ¨ IV ⟩
    ((y : ⟨ 𝓐 ⟩) ((x , s) : cofan y) (y' : ⟨ 𝓐 ⟩) (t : x β‰ˆβŸ¨ 𝓐 ⟩ y')
      β†’ (y , s) ＝ (y' , t))                                            β†βŸ¨ V ⟩
    ((y y' : ⟨ 𝓐 ⟩) (t : y β‰ˆβŸ¨ 𝓐 ⟩ y') β†’ (y , β‰ˆ-refl 𝓐 y) ＝ (y' , t))   β†βŸ¨ VI ⟩
    ((y' y : ⟨ 𝓐 ⟩) (t : y β‰ˆβŸ¨ 𝓐 ⟩ y') β†’ (y , β‰ˆ-refl 𝓐 y) ＝ (y' , t))   β†βŸ¨ VII ⟩
    ((y' : ⟨ 𝓐 ⟩) ((y , t) : cofan y') β†’ (y , β‰ˆ-refl 𝓐 y) ＝ (y' , t))  β†βŸ¨ VIII ⟩
    ((y' : ⟨ 𝓐 ⟩) β†’ (y' , β‰ˆ-refl 𝓐 y') ＝[ fan y' ] (y' , β‰ˆ-refl 𝓐 y')) β–’
    where
     II   = (Ξ» f x (y , s) (y' , t) β†’ f x y s y' t)
     III  = (Ξ» f x y β†’ f y x)
     IV   = (Ξ» f y x s y' t β†’ f y (x , s) y' t)
     V    = (Ξ» f y β†’ Ξ -proj⁻¹ (y , β‰ˆ-refl 𝓐 y) (co-prop y) (f y))
     VI   = (Ξ» f y y' β†’ f y' y)
     VII  = (Ξ» f y' y t β†’ f y' (y , t))
     VIII = (Ξ» _ y' β†’ Ξ -proj⁻¹ (y' , β‰ˆ-refl 𝓐 y') (co-prop y') refl)

 contr-fan-to-prop : ((x : ⟨ 𝓐 ⟩) β†’ is-contr (fan x))
                   β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))
 contr-fan-to-prop fan-contr x = singletons-are-props (fan-contr x)

 prop-fan-to-contr : ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))
                   β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-contr (fan x))
 prop-fan-to-contr fan-prop x
  = pointed-props-are-singletons (x , β‰ˆ-refl 𝓐 x) (fan-prop x)

 contr-fan-to-cofan : ((x : ⟨ 𝓐 ⟩) β†’ is-contr (fan x))
                    β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-contr (cofan x))
 contr-fan-to-cofan contr-fan x
  = pointed-props-are-singletons (x , β‰ˆ-refl 𝓐 x)
     (prop-fan-to-cofan (Ξ» - β†’ singletons-are-props (contr-fan -)) x)

 prop-fan-to-contr-cofan : ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))
                         β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-contr (cofan x))
 prop-fan-to-contr-cofan fan-prop x
  = contr-fan-to-cofan (prop-fan-to-contr fan-prop) x

 contr-cofan-to-fan : ((x : ⟨ 𝓐 ⟩) β†’ is-contr (cofan x))
                    β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-contr (fan x))
 contr-cofan-to-fan contr-cofan x
  = pointed-props-are-singletons (x , β‰ˆ-refl 𝓐 x)
     (prop-cofan-to-fan (Ξ» - β†’ singletons-are-props (contr-cofan -)) x)

\end{code}

We give the canonical function from an identification to an edge.

\begin{code}

 id-to-edge : {x y : ⟨ 𝓐 ⟩} β†’ x ＝ y β†’ x β‰ˆβŸ¨ 𝓐 ⟩ y
 id-to-edge {x} {x} refl = β‰ˆ-refl 𝓐 x

\end{code}

If each fan is propositional then id-to-edge is an equivalence.

\begin{code}

 private
  helper-edge-to-id : {x y : ⟨ 𝓐 ⟩}
                    β†’ (p : x β‰ˆβŸ¨ 𝓐 ⟩ y)
                    β†’ (x , β‰ˆ-refl 𝓐 x) ＝ (y , p)
                    β†’ x ＝ y
  helper-edge-to-id _ refl = refl

 module _
         (prop-fans : ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x)))
         (x y : ⟨ 𝓐 ⟩)
        where

  prop-fans-edge-to-id : x β‰ˆβŸ¨ 𝓐 ⟩ y β†’ x ＝ y
  prop-fans-edge-to-id p
   = helper-edge-to-id p (prop-fans x (x , β‰ˆ-refl 𝓐 x) (y , p))

  prop-fans-gives-retraction : has-retraction id-to-edge
  prop-fans-gives-retraction = (prop-fans-edge-to-id , II)
   where
    I : prop-fans x (x , β‰ˆ-refl 𝓐 x) (x , β‰ˆ-refl 𝓐 x) ＝ refl
    I = props-are-sets (prop-fans x)
         (prop-fans x (x , β‰ˆ-refl 𝓐 x) (x , β‰ˆ-refl 𝓐 x)) refl
    II : (p : x ＝ y)
       β†’ prop-fans-edge-to-id (id-to-edge p) ＝ p
    II refl = ap (helper-edge-to-id (β‰ˆ-refl 𝓐 x)) I

  id-are-retracts-of-edges : retract (x ＝ y) of (x β‰ˆβŸ¨ 𝓐 ⟩ y)
  id-are-retracts-of-edges
   = (prop-fans-edge-to-id , id-to-edge ,
      retraction-equation id-to-edge prop-fans-gives-retraction)

  prop-fans-gives-section : has-section id-to-edge
  prop-fans-gives-section
   = (prop-fans-edge-to-id , II)
   where
    I : (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) (Ο• : (x , β‰ˆ-refl 𝓐 x) ＝ (y , p))
      β†’ id-to-edge (helper-edge-to-id p Ο•) ＝ p
    I p refl = refl
    II : (p : x β‰ˆβŸ¨ 𝓐 ⟩ y)
       β†’ id-to-edge (prop-fans-edge-to-id p) ＝ p
    II p = I p (prop-fans x (x , β‰ˆ-refl 𝓐 x) (y , p))

  edges-are-retracts-of-id : retract (x β‰ˆβŸ¨ 𝓐 ⟩ y) of (x ＝ y)
  edges-are-retracts-of-id
   = (id-to-edge , prop-fans-gives-section)

 id-to-edge-equiv-implies-prop-fans : ((x y : ⟨ 𝓐 ⟩) β†’ is-equiv id-to-edge)
                                    β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))
 id-to-edge-equiv-implies-prop-fans e
  = contr-fan-to-prop fan-is-contr
  where
   fan-is-contr : (x : ⟨ 𝓐 ⟩) β†’ is-contr (fan x)
   fan-is-contr x = equiv-to-singleton' (Ξ£-cong (Ξ» y β†’ id-to-edge , e x y))
                     (singleton-types-are-singletons x)

 prop-fans-implies-id-to-edge-equiv
  : ((x : ⟨ 𝓐 ⟩) β†’ is-prop (fan x))
  β†’ ((x y : ⟨ 𝓐 ⟩) β†’ is-equiv id-to-edge)
 prop-fans-implies-id-to-edge-equiv prop-fans x y
  = (prop-fans-gives-section prop-fans x y ,
      prop-fans-gives-retraction prop-fans x y)

\end{code}

We now define univalent reflexive graphs in terms of propositional fans, but
one could use any of the equivalent characterizations.

\begin{code}

is-univalent-refl-graph : (𝓐 : Refl-Graph 𝓀 π“₯) β†’ 𝓀 βŠ” π“₯ Μ‡
is-univalent-refl-graph 𝓐 = (x : ⟨ 𝓐 ⟩) β†’ is-prop (fan 𝓐 x)

Univalent-Refl-Graph : (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
Univalent-Refl-Graph 𝓀 π“₯ = Ξ£ 𝓐 κž‰ (Refl-Graph 𝓀 π“₯) , is-univalent-refl-graph 𝓐

\end{code}

We will now record some boiler plate code for univalent reflexive graphs.

\begin{code}

⟨_⟩ᡀ : Univalent-Refl-Graph 𝓀 π“₯ β†’ 𝓀 Μ‡
⟨ (𝓐 , _) ⟩ᡀ = ⟨ 𝓐 ⟩

edge-relα΅€ : (𝓐 : Univalent-Refl-Graph 𝓀 π“₯) β†’ ⟨ 𝓐 ⟩ᡀ β†’ ⟨ 𝓐 ⟩ᡀ β†’ π“₯ Μ‡
edge-relα΅€ (𝓐 , _) = edge-rel 𝓐

syntax edge-relα΅€ 𝓐 x y = x β‰ˆα΅€βŸ¨ 𝓐 ⟩ y

β‰ˆ-reflα΅€ : (𝓐 : Univalent-Refl-Graph 𝓀 π“₯) β†’ (x : ⟨ 𝓐 ⟩ᡀ) β†’ x β‰ˆα΅€βŸ¨ 𝓐 ⟩ x
β‰ˆ-reflα΅€ (𝓐 , _) x = β‰ˆ-refl 𝓐 x

underlying-refl-graph : (𝓐 : Univalent-Refl-Graph 𝓀 π“₯)
                      β†’ Refl-Graph 𝓀 π“₯
underlying-refl-graph (𝓐 , _) = 𝓐

syntax underlying-refl-graph 𝓐 = 𝓐 /α΅€

underlying-refl-graph-is-univalent : (𝓐 : Univalent-Refl-Graph 𝓀 π“₯)
                                   β†’ is-univalent-refl-graph (𝓐 /α΅€)
underlying-refl-graph-is-univalent (𝓐 , is-ua) = is-ua

id-equiv-edge : (𝓐 : Univalent-Refl-Graph 𝓀 π“₯)
              β†’ (x y : ⟨ 𝓐 ⟩ᡀ)
              β†’ (x ＝ y) ≃ (x β‰ˆα΅€βŸ¨ 𝓐 ⟩ y)
id-equiv-edge 𝓐 x y
 = (id-to-edge (𝓐 /α΅€)
   , prop-fans-implies-id-to-edge-equiv (underlying-refl-graph 𝓐)
      (underlying-refl-graph-is-univalent 𝓐) x y)

edge-to-id : (𝓐 : Univalent-Refl-Graph 𝓀 π“₯) {x y : ⟨ 𝓐 ⟩ᡀ}
           β†’ x β‰ˆα΅€βŸ¨ 𝓐 ⟩ y
           β†’ x ＝ y
edge-to-id 𝓐 {x} {y} = ⌜ id-equiv-edge 𝓐 x y ⌝⁻¹

edge-to-id-preserves-refl : (𝓐 : Univalent-Refl-Graph 𝓀 π“₯) {x : ⟨ 𝓐 ⟩ᡀ}
                          β†’ edge-to-id 𝓐 (β‰ˆ-refl (𝓐 /α΅€) x) ＝ refl
edge-to-id-preserves-refl 𝓐 {x}
 = inverses-are-retractions (id-to-edge (𝓐 /α΅€))
    (prop-fans-implies-id-to-edge-equiv (underlying-refl-graph 𝓐)
     (underlying-refl-graph-is-univalent 𝓐) x x) refl

\end{code}

We show univalence implies edge induction.

TODO: show they are also equivalent.

\begin{code}

module _ (𝓐 : Refl-Graph 𝓀 π“₯) where

 edge-induction : 𝓀ω
 edge-induction = {𝓣 : Universe} (P : (x y : ⟨ 𝓐 ⟩) β†’ (x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ 𝓣 Μ‡)
                β†’ ((x : ⟨ 𝓐 ⟩) β†’ P x x (β‰ˆ-refl 𝓐 x))
                β†’ (x y : ⟨ 𝓐 ⟩)
                β†’ (p : x β‰ˆβŸ¨ 𝓐 ⟩ y)
                β†’ P x y p

 univalence-implies-edge-induction : is-univalent-refl-graph 𝓐
                                   β†’ edge-induction
 univalence-implies-edge-induction ua P R x y p
  = I (ua x (x , β‰ˆ-refl 𝓐 x) (y , p))
  where
   I : (x , β‰ˆ-refl 𝓐 x) ＝ (y , p) β†’ P x y p
   I refl = R x

\end{code}