Ian Ray. 28th August 2025.

Minor changes and merged into TypeToplogy in March 2026.

We provide some basic contructions on (displayed) reflexive graphs (see index
for references to Sterling, Buchholtz, etc.)

\begin{code}

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

module ReflexiveGraphs.Constructions where

open import MLTT.Spartan
open import UF.Powerset-MultiUniverse
open import UF.Size
open import UF.UniverseEmbedding
open import ReflexiveGraphs.Displayed
open import ReflexiveGraphs.Type

\end{code}

Given a reflexive graph and a displayed reflexive graph over it we can define
the total reflexive graph as follows.

\begin{code}

total-refl-graph : (𝓐 : Refl-Graph 𝓀 π“₯)
                 β†’ Displayed-Refl-Graph 𝓣 𝓦 𝓐
                 β†’ Refl-Graph (𝓀 βŠ” 𝓣) (π“₯ βŠ” 𝓦)
total-refl-graph {𝓀} {π“₯} {𝓣} {𝓦} 𝓐 𝓑 = ((Ξ£ x κž‰ ⟨ 𝓐 ⟩ , βŸͺ 𝓑 ⟫ x) , I , II)
 where
  I : Ξ£ x κž‰ ⟨ 𝓐 ⟩ , βŸͺ 𝓑 ⟫ x
    β†’ Ξ£ x κž‰ ⟨ 𝓐 ⟩ , βŸͺ 𝓑 ⟫ x
    β†’ π“₯ βŠ” 𝓦 Μ‡
  I (a , b) (a' , b') = Ξ£ p κž‰ a β‰ˆβŸ¨ 𝓐 ⟩ a' , b β‰ˆβŸ¨ 𝓑 βΈ΄ p ⟩ b'
  II : (t : Ξ£ x κž‰ ⟨ 𝓐 ⟩ , βŸͺ 𝓑 ⟫ x)
     β†’ I t t
  II (a , b) = (β‰ˆ-refl 𝓐 a , β‰ˆ-disp-refl 𝓑 b)

syntax total-refl-graph 𝓐 𝓑 = 𝓐 ﹐ 𝓑

\end{code}

We define the projection map from the total reflexive graph to the base
reflexive graph.

\begin{code}

total-refl-graph-projection
 : {𝓐 : Refl-Graph 𝓀 π“₯} (𝓑 : Displayed-Refl-Graph 𝓣 𝓦 𝓐)
 β†’ Refl-Graph-Hom (𝓐 ﹐ 𝓑) 𝓐
total-refl-graph-projection 𝓑 = (pr₁ , (Ξ» t t' β†’ pr₁) , ∼-refl)

syntax total-refl-graph-projection 𝓑 = Ο€ 𝓑

\end{code}

We define the binary product and binary sums of reflexive graphs.

\begin{code}

refl-graph-Γ— : Refl-Graph 𝓀 π“₯
             β†’ Refl-Graph 𝓀' π“₯'
             β†’ Refl-Graph (𝓀 βŠ” 𝓀') (π“₯ βŠ” π“₯')
refl-graph-Γ— {𝓀} {π“₯} {𝓀'} {π“₯'} 𝓐 𝓐' = ((⟨ 𝓐 ⟩ Γ— ⟨ 𝓐' ⟩) , I , II)
 where
  I : ⟨ 𝓐 ⟩ Γ— ⟨ 𝓐' ⟩ β†’ ⟨ 𝓐 ⟩ Γ— ⟨ 𝓐' ⟩ β†’ π“₯ βŠ” π“₯' Μ‡
  I (x , x') (y , y') = (x β‰ˆβŸ¨ 𝓐 ⟩ y) Γ— (x' β‰ˆβŸ¨ 𝓐' ⟩ y')
  II : (t : ⟨ 𝓐 ⟩ Γ— ⟨ 𝓐' ⟩) β†’ I t t
  II (x , x') = (β‰ˆ-refl 𝓐 x , β‰ˆ-refl 𝓐' x')

syntax refl-graph-Γ— 𝓐 𝓐' = 𝓐 βŠ— 𝓐'

refl-graph-+ : Refl-Graph 𝓀 π“₯
             β†’ Refl-Graph 𝓀' π“₯'
             β†’ Refl-Graph (𝓀 βŠ” 𝓀') (π“₯ βŠ” π“₯')
refl-graph-+ {𝓀} {π“₯} {𝓀'} {π“₯'} 𝓐 𝓐' = ((⟨ 𝓐 ⟩ + ⟨ 𝓐' ⟩) , I , II)
 where
  I : ⟨ 𝓐 ⟩ + ⟨ 𝓐' ⟩ β†’ ⟨ 𝓐 ⟩ + ⟨ 𝓐' ⟩ β†’ π“₯ βŠ” π“₯' Μ‡
  I (inl x) (inl y) = Lift π“₯' (x β‰ˆβŸ¨ 𝓐 ⟩ y)
  I (inl x) (inr y) = 𝟘
  I (inr x) (inl y) = 𝟘
  I (inr x) (inr y) = Lift π“₯ (x β‰ˆβŸ¨ 𝓐' ⟩ y)
  II : (t : ⟨ 𝓐 ⟩ + ⟨ 𝓐' ⟩) β†’ I t t
  II (inl x) = lift π“₯' (β‰ˆ-refl 𝓐 x)
  II (inr x) = lift π“₯ (β‰ˆ-refl 𝓐' x)

syntax refl-graph-+ 𝓐 𝓐' = 𝓐 βŠ• 𝓐'

\end{code}

Of course, we can generalize to products of reflexive graphs as follows.

\begin{code}

refl-graph-Ξ  : (A : 𝓀' Μ‡)
             β†’ (A β†’ Refl-Graph 𝓀 π“₯)
             β†’ Refl-Graph (𝓀' βŠ” 𝓀) (𝓀' βŠ” π“₯)
refl-graph-Ξ  {𝓀'} {𝓀} {π“₯} A 𝓑
 = (((x : A) β†’ ⟨ 𝓑 x ⟩) , I , II)
 where
  I : ((x : A) β†’ ⟨ 𝓑 x ⟩)
    β†’ ((x : A) β†’ ⟨ 𝓑 x ⟩)
    β†’ 𝓀' βŠ” π“₯ Μ‡
  I f f' = (x : A) β†’ f x β‰ˆβŸ¨ 𝓑 x ⟩ f' x
  II : (f : (x : A) β†’ ⟨ 𝓑 x ⟩) β†’ I f f
  II f x = β‰ˆ-refl (𝓑 x) (f x)

syntax refl-graph-Ξ  A (Ξ» x β†’ 𝓑) = ∏ x ΛΈ A , 𝓑

\end{code}

We define the coproduct of reflexive graphs in terms of sigma types.

\begin{code}

refl-graph-Ξ£ : (A : 𝓀' Μ‡)
             β†’ (A β†’ Refl-Graph 𝓀 π“₯)
             β†’ Refl-Graph (𝓀' βŠ” 𝓀) (𝓀' βŠ” π“₯)
refl-graph-Ξ£ {𝓀'} {𝓀} {π“₯} A 𝓑
 = ((Ξ£ x κž‰ A , ⟨ 𝓑 x ⟩) , I , II)
 where
  I : Ξ£ x κž‰ A , ⟨ 𝓑 x ⟩
    β†’ Ξ£ x κž‰ A , ⟨ 𝓑 x ⟩
    β†’ 𝓀' βŠ” π“₯ Μ‡
  I (a , b) (a' , b')
   = Ξ£ p κž‰ a ＝ a' , transport (Ξ» - β†’ ⟨ 𝓑 - ⟩) p b β‰ˆβŸ¨ 𝓑 a' ⟩ b'
  II : (t : Ξ£ x κž‰ A , ⟨ 𝓑 x ⟩) β†’ I t t
  II (a , b) = (refl , β‰ˆ-refl (𝓑 a) b)

syntax refl-graph-Ξ£ A (Ξ» x β†’ 𝓑) = ∐ x ΛΈ A , 𝓑

\end{code}

The tensor and cotensor of reflexive graphs can be defined in terms of product
and coproduct. 

\begin{code}

cotensor-refl-graph : 𝓀' Μ‡
                    β†’ Refl-Graph 𝓀 π“₯
                    β†’ Refl-Graph (𝓀' βŠ” 𝓀) (𝓀' βŠ” π“₯)
cotensor-refl-graph A 𝓑 = ∏ _ ΛΈ A , 𝓑

syntax cotensor-refl-graph A 𝓑 = A βž™ 𝓑  

tensor-refl-graph : 𝓀' Μ‡
                  β†’ Refl-Graph 𝓀 π“₯
                  β†’ Refl-Graph (𝓀' βŠ” 𝓀) (𝓀' βŠ” π“₯)
tensor-refl-graph A 𝓑 = ∐ _ ΛΈ A , 𝓑

\end{code}

We have a canonical discrete reflexive graph given by the identity type.
On the other end of the extreme we have the codiscrete reflexive graph.

\begin{code}

discrete-reflexive-graph : 𝓀 Μ‡ β†’ Refl-Graph 𝓀 𝓀
discrete-reflexive-graph A = (A , _＝_ , ∼-refl)

syntax discrete-reflexive-graph A = Ξ” A

codiscrete-reflexive-graph : 𝓀 Μ‡ β†’ Refl-Graph 𝓀 𝓀
codiscrete-reflexive-graph A = (A , (Ξ» _ _ β†’ πŸ™) , Ξ» _ β†’ ⋆)

\end{code}

We can give the constant displayed reflexive graph.

\begin{code}

constant-displayed-reflexive-graph : (𝓐 : Refl-Graph 𝓀 π“₯)
                                   β†’ Refl-Graph 𝓀' π“₯'
                                   β†’ Displayed-Refl-Graph 𝓀' π“₯' 𝓐
constant-displayed-reflexive-graph {𝓀} {π“₯} {𝓀'} {π“₯'} 𝓐 𝓑 = (I , II , β‰ˆ-refl 𝓑)
 where
  I : ⟨ 𝓐 ⟩ β†’ 𝓀' Μ‡
  I x = ⟨ 𝓑 ⟩
  II : {x y : ⟨ 𝓐 ⟩} β†’ x β‰ˆβŸ¨ 𝓐 ⟩ y β†’ ⟨ 𝓑 ⟩ β†’ ⟨ 𝓑 ⟩ β†’ π“₯' Μ‡
  II _ u v = u β‰ˆβŸ¨ 𝓑 ⟩ v

syntax constant-displayed-reflexive-graph 𝓐 𝓑 = 𝓐 * 𝓑

private
 observation₁ : (𝓐 : Refl-Graph 𝓀 π“₯) (𝓑 : Refl-Graph 𝓀' π“₯')
              β†’ (x : ⟨ 𝓐 ⟩)
              β†’ [ 𝓐 * 𝓑 ] x ＝ 𝓑 
 observation₁ 𝓐 𝓑 x = refl

 observationβ‚‚ : (𝓐 : Refl-Graph 𝓀 π“₯) (𝓑 : Refl-Graph 𝓀' π“₯')
              β†’ 𝓐 ﹐ (𝓐 * 𝓑) ＝ 𝓐 βŠ— 𝓑
 observationβ‚‚ 𝓐 𝓑 = refl

\end{code}

We can retstrict a reflexive graph structure to a subset of the carrier of a
reflexive graph.

\begin{code}

refl-graph-βŠ† : (𝓐 : Refl-Graph 𝓀 π“₯) 
             β†’ π“Ÿ {𝓣} ⟨ 𝓐 ⟩
             β†’ Refl-Graph (𝓀 βŠ” 𝓣) π“₯
refl-graph-βŠ† {𝓀} {π“₯} {𝓣} 𝓐 S = (𝕋 S , I , II)
 where
  I : 𝕋 S β†’ 𝕋 S β†’ π“₯ Μ‡
  I (x , _) (y , _) = x β‰ˆβŸ¨ 𝓐 ⟩ y
  II : (p : 𝕋 S) β†’ I p p
  II (x , _) = β‰ˆ-refl 𝓐 x

syntax refl-graph-βŠ† 𝓐 S = x ∢ 𝓐 ∣ S x

\end{code}

We can give opposite constructions for (displayed) reflexive graphs.

\begin{code}

opposite-refl-graph : Refl-Graph 𝓀 π“₯ β†’ Refl-Graph 𝓀 π“₯
opposite-refl-graph {𝓀} {π“₯} 𝓐 = (⟨ 𝓐 ⟩ , I , β‰ˆ-refl 𝓐)
 where
  I : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓐 ⟩ β†’ π“₯ Μ‡
  I x y = y β‰ˆβŸ¨ 𝓐 ⟩ x

syntax opposite-refl-graph 𝓐 = 𝓐 α΅’α΅–

private
 observation₃ : (𝓐 : Refl-Graph 𝓀 π“₯)
              β†’ (𝓐 α΅’α΅–) α΅’α΅– ＝ 𝓐
 observation₃ 𝓐 = refl

opposite-displayed-refl-graph
 : (𝓐 : Refl-Graph 𝓀 π“₯)
 β†’ Displayed-Refl-Graph 𝓣 𝓦 𝓐
 β†’ Displayed-Refl-Graph 𝓣 𝓦 (𝓐 α΅’α΅–)
opposite-displayed-refl-graph {_} {_} {_} {𝓦} 𝓐 𝓑 = (βŸͺ 𝓑 ⟫ , I , β‰ˆ-disp-refl 𝓑)
 where
  I : {x y : ⟨ 𝓐 ⟩} (p : x β‰ˆβŸ¨ 𝓐 α΅’α΅– ⟩ y)
    β†’ βŸͺ 𝓑 ⟫ x β†’ βŸͺ 𝓑 ⟫ y β†’ 𝓦 Μ‡
  I p u v = v β‰ˆβŸ¨ 𝓑 βΈ΄ p ⟩ u

syntax opposite-displayed-refl-graph 𝓐 𝓑 = 𝓑 α΅’α΅– at 𝓐

private
 observationβ‚„
  : (𝓐 : Refl-Graph 𝓀 π“₯) (𝓑 : Displayed-Refl-Graph 𝓣 𝓦 𝓐)
  β†’ (𝓑 α΅’α΅– at 𝓐) α΅’α΅– at (𝓐 α΅’α΅–) ＝ 𝓑
 observationβ‚„ 𝓐 𝓑 = refl

\end{code}

We can define the resrtiction of an iterated displayed reflexive graphs.

\begin{code}

restriction-iterated-displayed-refl-graph
 : {𝓐 : Refl-Graph 𝓀 π“₯} (𝓑 : Displayed-Refl-Graph 𝓣 𝓦 𝓐)
 β†’ Displayed-Refl-Graph 𝓣 𝓦 (𝓐 ﹐ 𝓑)
 β†’ (x : ⟨ 𝓐 ⟩)
 β†’ Displayed-Refl-Graph 𝓣 𝓦 ([ 𝓑 ] x)
restriction-iterated-displayed-refl-graph {𝓀} {π“₯} {𝓣} {𝓦} {𝓐} 𝓑 𝓒 x
 = (I , II , III)
 where
  I : βŸͺ 𝓑 ⟫ x β†’ 𝓣 Μ‡
  I u = βŸͺ 𝓒 ⟫ (x , u)
  II : {u v : βŸͺ 𝓑 ⟫ x} (p : u β‰ˆβŸ¨ 𝓑 βΈ΄ β‰ˆ-refl 𝓐 x ⟩ v)
     β†’ βŸͺ 𝓒 ⟫ (x , u) β†’ βŸͺ 𝓒 ⟫ (x , v) β†’ 𝓦 Μ‡
  II p c c' = c β‰ˆβŸ¨ 𝓒 βΈ΄ (β‰ˆ-refl 𝓐 x , p) ⟩ c'
  III : {u : βŸͺ 𝓑 ⟫ x} (c : I u)
      β†’ c β‰ˆβŸ¨ 𝓒 βΈ΄ (β‰ˆ-refl 𝓐 x , β‰ˆ-disp-refl 𝓑 u) ⟩ c
  III c = β‰ˆ-disp-refl 𝓒 c

syntax restriction-iterated-displayed-refl-graph 𝓑 𝓒 x = 𝓒 ∣ 𝓑 , x 

\end{code}