Constructions

Ian Ray. 28th August 2025.

Minor changes and merged into TypeToplogy in March 2026.

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


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

module ReflexiveGraphs.Constructions where

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


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


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 𝓐 𝓑 = 𝓐 ﹐ 𝓑


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


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 𝓑 = π 𝓑


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


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-+ 𝓐 𝓐' = 𝓐 ⊕ 𝓐'


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


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 , 𝓑


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


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 , 𝓑


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


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 , 𝓑


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.


discrete-reflexive-graph : 𝓤 ̇ → Refl-Graph 𝓤 𝓤
discrete-reflexive-graph A = (A , _＝_ , ∼-refl)

Δ : 𝓤 ̇ → Refl-Graph 𝓤 𝓤
Δ = discrete-reflexive-graph

codiscrete-reflexive-graph : 𝓤 ̇ → Refl-Graph 𝓤 𝓤
codiscrete-reflexive-graph A = (A , (λ _ _ → 𝟙) , λ _ → ⋆)

∇ : 𝓤 ̇ → Refl-Graph 𝓤 𝓤
∇ = codiscrete-reflexive-graph


We can give the constant displayed reflexive graph.


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


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


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


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


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


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


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