Properties

Ian Ray. 7th November 2025.

Internal code review and addition by Carlo Angiuli 18th November 2025.

Minor changes and merged into TypeToplogy in June 2026.


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

open import UF.FunExt

module ReflexiveGraphs.Properties (fe : Fun-Ext) where

open import MLTT.Spartan
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.PropIndexedPiSigma
open import ReflexiveGraphs.Constructions
open import ReflexiveGraphs.UnivalentClosureProperties
open import ReflexiveGraphs.Displayed
open import ReflexiveGraphs.DisplayedUnivalent
open import ReflexiveGraphs.Lenses
open import ReflexiveGraphs.Type
open import ReflexiveGraphs.UnbiasedLenses
open import ReflexiveGraphs.Univalent

private
 fe' : FunExt
 fe' 𝓀 π“₯ = fe {𝓀} {π“₯}


In this file we observe that univalence of (displayed) reflexive graphs and the
structure of a lens on a reflexive graph and associated family of reflexive
graphs are properties rather than data. For this, we globally assume function
extensionality, and for the latter, we assume univalence of the reflexive
graphs in question.

We show that univalence for (displayed) reflexive graphs is a proposition.


refl-graph-univalence-is-a-property : (𝓐 : Refl-Graph 𝓀 π“₯)
                                    β†’ is-prop (is-univalent-refl-graph 𝓐)
refl-graph-univalence-is-a-property 𝓐
 = Ξ -is-prop fe (Ξ» - β†’ being-prop-is-prop fe)

displayed-refl-graph-univalence-is-a-property
 : (𝓐 : Refl-Graph 𝓀 π“₯) (𝓑 : Displayed-Refl-Graph 𝓀' π“₯' 𝓐)
 β†’ is-prop (is-displayed-univalent-refl-graph 𝓐 𝓑)
displayed-refl-graph-univalence-is-a-property 𝓐 𝓑
 = Ξ -is-prop fe (Ξ» - β†’ refl-graph-univalence-is-a-property ([ 𝓑 ] -))


We show that the oplax contravariant lens structure is contractible and in fact
a property of the reflexive graph and family of reflexive graphs.


module _ (𝓀' π“₯' : Universe)
         (𝓐 : Refl-Graph 𝓀 π“₯)
         (𝓑 : ⟨ 𝓐 ⟩ β†’ Refl-Graph 𝓀' π“₯')
       where

 oplax-lens-structure-is-contr
  : is-univalent-refl-graph 𝓐
  β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-univalent-refl-graph (𝓑 x))
  β†’ is-contr (oplax-covariant-lens-structure 𝓀' π“₯' 𝓐 𝓑)
 oplax-lens-structure-is-contr is-ua-𝓐 is-ua-𝓑 =
  equiv-to-singleton I
   (Ξ -is-singleton fe (Ξ» x β†’ equiv-to-singleton (II x) (III x)))
  where
   open oplax-covariant-lens-structure 
   I : oplax-covariant-lens-structure 𝓀' π“₯' 𝓐 𝓑
     ≃ ((x : ⟨ 𝓐 ⟩)
        β†’ Ξ£ Ο• κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝓑 x ⟩ β†’ ⟨ 𝓑 y ⟩)
          , ((u : ⟨ 𝓑 x ⟩) β†’ Ο• x (β‰ˆ-refl 𝓐 x) u β‰ˆβŸ¨ 𝓑 x ⟩ u))
   I = qinveq (Ξ» 𝓛 x β†’ ((Ξ» _ β†’ push 𝓛) , push-refl 𝓛))
        ((Ξ» f β†’ record
          {push = Ξ» {x y} β†’ (pr₁ (f x)) y ; push-refl = Ξ» {x} β†’ prβ‚‚ (f x)})
         , ∼-refl , ∼-refl)
   II : (x : ⟨ 𝓐 ⟩) β†’ _ ≃ (cofan (⟨ 𝓑 x ⟩ βž™ 𝓑 x) id)
   II x = (Ξ£ Ο• κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝓑 x ⟩ β†’ ⟨ 𝓑 y ⟩) ,
            ((u : ⟨ 𝓑 x ⟩) β†’ Ο• x (β‰ˆ-refl 𝓐 x) u β‰ˆβŸ¨ 𝓑 x ⟩ u))
           β‰ƒβŸ¨ Ξ£-change-of-variable-≃ _ (≃-sym (curry-uncurry fe')) ⟩
          (Ξ£ Ο• κž‰ (((y , p) : fan 𝓐 x) β†’ ⟨ 𝓑 x ⟩ β†’ ⟨ 𝓑 y ⟩) ,
            ((u : ⟨ 𝓑 x ⟩) β†’ Ο• (x , (β‰ˆ-refl 𝓐 x)) u β‰ˆβŸ¨ 𝓑 x ⟩ u))
           β‰ƒβŸ¨ Ξ£-change-of-variable-≃ _
               (prop-indexed-product (x , β‰ˆ-refl 𝓐 x) fe (is-ua-𝓐 x)) ⟩
          (Ξ£ Ο• κž‰ (⟨ 𝓑 x ⟩ β†’ ⟨ 𝓑 x ⟩) , ((u : ⟨ 𝓑 x ⟩) β†’ Ο• u β‰ˆβŸ¨ 𝓑 x ⟩ u))
           β‰ƒβŸ¨by-definition⟩
          cofan (⟨ 𝓑 x ⟩ βž™ 𝓑 x) id β– 
   III : (x : ⟨ 𝓐 ⟩) β†’ is-contr (cofan (⟨ 𝓑 x ⟩ βž™ 𝓑 x) id)
   III x = prop-fan-to-contr-cofan (⟨ 𝓑 x ⟩ βž™ 𝓑 x)
            (univalence-closed-under-cotensor fe _ (𝓑 x) (is-ua-𝓑 x))
            id

 oplax-lens-structure-is-a-property
  : is-univalent-refl-graph 𝓐
  β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-univalent-refl-graph (𝓑 x))
  β†’ is-prop (oplax-covariant-lens-structure 𝓀' π“₯' 𝓐 𝓑)
 oplax-lens-structure-is-a-property is-ua-𝓐 is-ua-𝓑
  = singletons-are-props (oplax-lens-structure-is-contr is-ua-𝓐 is-ua-𝓑)


Similarly, a lax covariant lens structure is contractible and thus a property.


 lax-lens-structure-is-contr
  : is-univalent-refl-graph 𝓐
  β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-univalent-refl-graph (𝓑 x))
  β†’ is-contr (lax-contravariant-lens-structure 𝓀' π“₯' 𝓐 𝓑)
 lax-lens-structure-is-contr is-ua-𝓐 is-ua-𝓑 =
  equiv-to-singleton I
   (Ξ -is-singleton fe (Ξ» x β†’ equiv-to-singleton (III x) (II x)))
  where
   open lax-contravariant-lens-structure 
   I : lax-contravariant-lens-structure 𝓀' π“₯' 𝓐 𝓑
     ≃ ((x : ⟨ 𝓐 ⟩)
        β†’ Ξ£ Ο• κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝓑 y ⟩ β†’ ⟨ 𝓑 x ⟩)
          , ((u : ⟨ 𝓑 x ⟩) β†’ u β‰ˆβŸ¨ 𝓑 x ⟩ Ο• x (β‰ˆ-refl 𝓐 x) u))
   I = qinveq (Ξ» 𝓛 x β†’ ((Ξ» _ β†’ pull 𝓛) , pull-refl 𝓛))
        ((Ξ» f β†’ record
          {pull = Ξ» {x y} β†’ (pr₁ (f x)) y ; pull-refl = Ξ» {x} β†’ prβ‚‚ (f x)})
         , ∼-refl , ∼-refl)
   II : (x : ⟨ 𝓐 ⟩) β†’ is-contr (fan (⟨ 𝓑 x ⟩ βž™ 𝓑 x) id)
   II x = prop-fan-to-contr (⟨ 𝓑 x ⟩ βž™ 𝓑 x)
           (univalence-closed-under-cotensor fe _ (𝓑 x) (is-ua-𝓑 x)) id
   III : (x : ⟨ 𝓐 ⟩) β†’ _ ≃ fan (⟨ 𝓑 x ⟩ βž™ 𝓑 x) id
   III x = (Ξ£ Ο• κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝓑 y ⟩ β†’ ⟨ 𝓑 x ⟩) ,
             ((u : ⟨ 𝓑 x ⟩) β†’ u β‰ˆβŸ¨ 𝓑 x ⟩ Ο• x (β‰ˆ-refl 𝓐 x) u))
             β‰ƒβŸ¨ Ξ£-change-of-variable-≃ _ (≃-sym (curry-uncurry fe')) ⟩
           (Ξ£ Ο• κž‰ (((y , p) : fan 𝓐 x) β†’ ⟨ 𝓑 y ⟩ β†’ ⟨ 𝓑 x ⟩) ,
             ((u : ⟨ 𝓑 x ⟩) β†’ u β‰ˆβŸ¨ 𝓑 x ⟩ Ο• (x , (β‰ˆ-refl 𝓐 x)) u))
             β‰ƒβŸ¨ Ξ£-change-of-variable-≃ _
                 (prop-indexed-product (x , β‰ˆ-refl 𝓐 x) fe (is-ua-𝓐 x)) ⟩
           (Ξ£ Ο• κž‰ (⟨ 𝓑 x ⟩ β†’ ⟨ 𝓑 x ⟩) , ((u : ⟨ 𝓑 x ⟩) β†’ u β‰ˆβŸ¨ 𝓑 x ⟩ Ο• u))
             β‰ƒβŸ¨by-definition⟩
           fan (⟨ 𝓑 x ⟩ βž™ 𝓑 x) id β– 

 lax-lens-structure-is-a-property
  : is-univalent-refl-graph 𝓐
  β†’ ((x : ⟨ 𝓐 ⟩) β†’ is-univalent-refl-graph (𝓑 x))
  β†’ is-prop (lax-contravariant-lens-structure 𝓀' π“₯' 𝓐 𝓑)
 lax-lens-structure-is-a-property is-ua-𝓐 is-ua-𝓑
  = singletons-are-props (lax-lens-structure-is-contr is-ua-𝓐 is-ua-𝓑)


Finally, an unbiased lens structure is contractible and thus a property.


module _ (𝓀' π“₯' : Universe)
         (𝓐 : Refl-Graph 𝓀 π“₯)
         (𝓑 : {x y : ⟨ 𝓐 ⟩} β†’ (x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ Refl-Graph 𝓀' π“₯')
       where

 unbiased-lens-structure-is-contr
  : is-univalent-refl-graph 𝓐
  β†’ ((x y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ is-univalent-refl-graph (𝓑 p))
  β†’ is-contr (unbiased-lens-structure 𝓀' π“₯' 𝓐 𝓑)
 unbiased-lens-structure-is-contr is-ua-𝓐 is-ua-𝓑
  = equiv-to-singleton I
     (Ξ -is-singleton fe (Ξ» x β†’ equiv-to-singleton (III x) (II x id)))
  where
   open unbiased-lens-structure
   I : unbiased-lens-structure 𝓀' π“₯' 𝓐 𝓑
     ≃ ((x : ⟨ 𝓐 ⟩)
     β†’ Ξ£ Ο• κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩ β†’ ⟨ 𝓑 p ⟩)
     , Ξ£ ψ κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝓑 (β‰ˆ-refl 𝓐 y) ⟩ β†’ ⟨ 𝓑 p ⟩)
     , ((u : ⟨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩)
         β†’ Ο• x (β‰ˆ-refl 𝓐 x) u β‰ˆβŸ¨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩ ψ x (β‰ˆ-refl 𝓐 x) u)
     Γ— ((u : ⟨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩) β†’ u β‰ˆβŸ¨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩ ψ x (β‰ˆ-refl 𝓐 x) u))
   I = qinveq
        (Ξ» 𝓛 x β†’ ((Ξ» _ β†’ lext 𝓛) , (Ξ» _ β†’ rext 𝓛) , ext-refl 𝓛 , rext-refl 𝓛))
        ((Ξ» f β†’ record {lext = Ξ» {x y} β†’ (pr₁ (f x)) y
                        ; rext = Ξ» {x y} β†’ (pr₁ (prβ‚‚ (f x))) y
                        ; ext-refl = Ξ» {x} β†’ pr₁ (prβ‚‚ (prβ‚‚ (f x)))
                        ; rext-refl = Ξ» {x} β†’ prβ‚‚ (prβ‚‚ (prβ‚‚ (f x)))})
         , ∼-refl , ∼-refl)
   II : (x : ⟨ 𝓐 ⟩) (Ο• : ⟨ ⟨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩ βž™ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩)
       β†’ is-contr (fan (⟨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩ βž™ 𝓑 (β‰ˆ-refl 𝓐 x)) Ο•)
   II x Ο• = prop-fan-to-contr
             (⟨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩ βž™ 𝓑 (β‰ˆ-refl 𝓐 x))
              (univalence-closed-under-cotensor fe _ (𝓑 (β‰ˆ-refl 𝓐 x))
               (is-ua-𝓑 x x (β‰ˆ-refl 𝓐 x))) Ο•
   III : (x : ⟨ 𝓐 ⟩) β†’ _ ≃ fan (⟨ 𝓑 (β‰ˆ-refl 𝓐 x) ⟩ βž™ 𝓑 (β‰ˆ-refl 𝓐 x)) id
   III x =
    (Ξ£ Ο• κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝔹 ⟩ β†’ ⟨ 𝓑 p ⟩)
     , Ξ£ ψ κž‰ ((y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ ⟨ 𝓑 (β‰ˆ-refl 𝓐 y) ⟩ β†’ ⟨ 𝓑 p ⟩)
     , ((u : B) β†’ Ο• x r u β‰ˆβŸ¨ 𝔹 ⟩ ψ x r u) Γ— ((u : B) β†’ u β‰ˆβŸ¨ 𝔹 ⟩ ψ x r u))
                                                              β‰ƒβŸ¨ IV ⟩
    (Ξ£ Ο• κž‰ (((y , p) : fan 𝓐 x) β†’ ⟨ 𝔹 ⟩ β†’ ⟨ 𝓑 p ⟩)
     , Ξ£ ψ κž‰ (((y , p) : fan 𝓐 x) β†’ ⟨ 𝓑 (β‰ˆ-refl 𝓐 y) ⟩ β†’ ⟨ 𝓑 p ⟩)
     , ((u : B) β†’ Ο• (x , r) u β‰ˆβŸ¨ 𝔹 ⟩ ψ (x , r) u)
     Γ— ((u : B) β†’ u β‰ˆβŸ¨ 𝔹 ⟩ ψ (x , r) u))
                                                              β‰ƒβŸ¨ V ⟩
    (Ξ£ Ο• κž‰ (B β†’ B) , Ξ£ ψ κž‰ (B β†’ B)
     , ((u : B) β†’ Ο• u β‰ˆβŸ¨ 𝔹 ⟩ ψ u) Γ— ((u : B) β†’ u β‰ˆβŸ¨ 𝔹 ⟩ ψ u))
                                                              β‰ƒβŸ¨by-definition⟩
    (Ξ£ Ο• κž‰ (B β†’ B) , Ξ£ ψ κž‰ (B β†’ B) , (Ο• β‰ˆβŸ¨ B βž™ 𝔹 ⟩ ψ) Γ— (id β‰ˆβŸ¨ B βž™ 𝔹 ⟩ ψ))
                                                              β‰ƒβŸ¨ VI ⟩
    (Ξ£ Ο• κž‰ (B β†’ B) , Ξ£ (ψ , _) κž‰ fan (B βž™ 𝔹) Ο• , (id β‰ˆβŸ¨ B βž™ 𝔹 ⟩ ψ))
                                                              β‰ƒβŸ¨ VII ⟩
    ((Ξ£ Ο• κž‰ (B β†’ B) , (id β‰ˆβŸ¨ B βž™ 𝔹 ⟩ Ο•)))
                                                              β‰ƒβŸ¨by-definition⟩
    fan (B βž™ 𝔹) id                                            β– 
     where
      r = β‰ˆ-refl 𝓐 x
      𝔹 = 𝓑 r
      B = ⟨ 𝔹 ⟩
      IV = Ξ£-bicong _ _ (≃-sym (curry-uncurry fe'))
            (Ξ» _ β†’ Ξ£-change-of-variable-≃ _ (≃-sym (curry-uncurry fe')))
      V = Ξ£-bicong _ _ (prop-indexed-product (x , β‰ˆ-refl 𝓐 x) fe (is-ua-𝓐 x))
           (Ξ» _ β†’ Ξ£-change-of-variable-≃ _
            (prop-indexed-product (x , β‰ˆ-refl 𝓐 x) fe (is-ua-𝓐 x)))
      VI = Ξ£-cong (Ξ» _ β†’ ≃-sym Ξ£-assoc)
      VII = Ξ£-cong (Ξ» - β†’ prop-indexed-sum (center (II x -))
             (singletons-are-props (II x -)))

 unbiased-lens-structure-is-a-property
  : is-univalent-refl-graph 𝓐
  β†’ ((x y : ⟨ 𝓐 ⟩) (p : x β‰ˆβŸ¨ 𝓐 ⟩ y) β†’ is-univalent-refl-graph (𝓑 p))
  β†’ is-prop (unbiased-lens-structure 𝓀' π“₯' 𝓐 𝓑)
 unbiased-lens-structure-is-a-property is-ua-𝓐 is-ua-𝓑
  = singletons-are-props
     (unbiased-lens-structure-is-contr is-ua-𝓐 is-ua-𝓑)