Equivalences of enriched undirected graphs

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-08-14.

module graph-theory.equivalences-enriched-undirected-graphs where

Imports
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import graph-theory.enriched-undirected-graphs
open import graph-theory.equivalences-undirected-graphs
open import graph-theory.neighbors-undirected-graphs


Idea

An equivalence of (A,B)-enriched undirected graphs from an (A,B)-enriched undirected graph G to an (A,B)-enriched undirected graph H consists of an equivalence e of the underlying graphs of G and H such that preserving the labeling and the equivalences on the neighbors.

Definition

Equivalences between enriched undirected graphs

module _
{l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2)
(G : Enriched-Undirected-Graph l3 l4 A B)
(H : Enriched-Undirected-Graph l5 l6 A B)
where

equiv-Enriched-Undirected-Graph :
UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
equiv-Enriched-Undirected-Graph =
Σ ( equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H))
( λ e →
Σ ( ( shape-vertex-Enriched-Undirected-Graph A B G) ~
( ( shape-vertex-Enriched-Undirected-Graph A B H) ∘
( vertex-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( e))))
( λ α →
( x : vertex-Enriched-Undirected-Graph A B G) →
htpy-equiv
( ( equiv-neighbor-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( e)
( x)) ∘e
( equiv-neighbor-Enriched-Undirected-Graph A B G x))
( ( equiv-neighbor-Enriched-Undirected-Graph A B H
( vertex-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( e)
( x))) ∘e
( equiv-tr B (α x)))))

module _
{l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2)
(G : Enriched-Undirected-Graph l3 l4 A B)
(H : Enriched-Undirected-Graph l5 l6 A B)
(e : equiv-Enriched-Undirected-Graph A B G H)
where

equiv-undirected-graph-equiv-Enriched-Undirected-Graph :
equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
equiv-undirected-graph-equiv-Enriched-Undirected-Graph = pr1 e

equiv-vertex-equiv-Enriched-Undirected-Graph :
vertex-Enriched-Undirected-Graph A B G ≃
vertex-Enriched-Undirected-Graph A B H
equiv-vertex-equiv-Enriched-Undirected-Graph =
equiv-vertex-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( equiv-undirected-graph-equiv-Enriched-Undirected-Graph)

vertex-equiv-Enriched-Undirected-Graph :
vertex-Enriched-Undirected-Graph A B G →
vertex-Enriched-Undirected-Graph A B H
vertex-equiv-Enriched-Undirected-Graph =
vertex-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( equiv-undirected-graph-equiv-Enriched-Undirected-Graph)

equiv-unordered-pair-vertices-equiv-Enriched-Undirected-Graph :
unordered-pair-vertices-Enriched-Undirected-Graph A B G ≃
unordered-pair-vertices-Enriched-Undirected-Graph A B H
equiv-unordered-pair-vertices-equiv-Enriched-Undirected-Graph =
equiv-unordered-pair-vertices-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( equiv-undirected-graph-equiv-Enriched-Undirected-Graph)

unordered-pair-vertices-equiv-Enriched-Undirected-Graph :
unordered-pair-vertices-Enriched-Undirected-Graph A B G →
unordered-pair-vertices-Enriched-Undirected-Graph A B H
unordered-pair-vertices-equiv-Enriched-Undirected-Graph =
unordered-pair-vertices-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( equiv-undirected-graph-equiv-Enriched-Undirected-Graph)

equiv-edge-equiv-Enriched-Undirected-Graph :
( p : unordered-pair-vertices-Enriched-Undirected-Graph A B G) →
edge-Enriched-Undirected-Graph A B G p ≃
edge-Enriched-Undirected-Graph A B H
( unordered-pair-vertices-equiv-Enriched-Undirected-Graph p)
equiv-edge-equiv-Enriched-Undirected-Graph =
equiv-edge-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( equiv-undirected-graph-equiv-Enriched-Undirected-Graph)

edge-equiv-Enriched-Undirected-Graph :
( p : unordered-pair-vertices-Enriched-Undirected-Graph A B G) →
edge-Enriched-Undirected-Graph A B G p →
edge-Enriched-Undirected-Graph A B H
( unordered-pair-vertices-equiv-Enriched-Undirected-Graph p)
edge-equiv-Enriched-Undirected-Graph =
edge-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B H)
( equiv-undirected-graph-equiv-Enriched-Undirected-Graph)

shape-equiv-Enriched-Undirected-Graph :
(v : vertex-Enriched-Undirected-Graph A B G) →
( shape-vertex-Enriched-Undirected-Graph A B G v) ＝
( shape-vertex-Enriched-Undirected-Graph A B H
( vertex-equiv-Enriched-Undirected-Graph v))
shape-equiv-Enriched-Undirected-Graph = pr1 (pr2 e)


The identity equivalence of an enriched undirected graph

module _
{l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2)
(G : Enriched-Undirected-Graph l3 l4 A B)
where

id-equiv-Enriched-Undirected-Graph :
equiv-Enriched-Undirected-Graph A B G G
pr1 id-equiv-Enriched-Undirected-Graph =
id-equiv-Undirected-Graph (undirected-graph-Enriched-Undirected-Graph A B G)
pr1 (pr2 id-equiv-Enriched-Undirected-Graph) = refl-htpy
pr2 (pr2 id-equiv-Enriched-Undirected-Graph) x b =
neighbor-id-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( x)
( map-equiv-neighbor-Enriched-Undirected-Graph A B G x b)


Properties

Univalence for enriched undirected graphs

module _
{l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2)
(G : Enriched-Undirected-Graph l3 l4 A B)
where

is-torsorial-equiv-Enriched-Undirected-Graph :
is-torsorial (equiv-Enriched-Undirected-Graph A B G)
is-torsorial-equiv-Enriched-Undirected-Graph =
is-torsorial-Eq-structure
( is-torsorial-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G))
( pair
( undirected-graph-Enriched-Undirected-Graph A B G)
( id-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)))
( is-torsorial-Eq-structure
( is-torsorial-htpy
( shape-vertex-Enriched-Undirected-Graph A B G))
( pair
( shape-vertex-Enriched-Undirected-Graph A B G)
( refl-htpy))
( is-torsorial-Eq-Π
( λ x →
is-torsorial-htpy-equiv
( equiv-neighbor-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G)
( undirected-graph-Enriched-Undirected-Graph A B G)
( id-equiv-Undirected-Graph
( undirected-graph-Enriched-Undirected-Graph A B G))
( x) ∘e
( equiv-neighbor-Enriched-Undirected-Graph A B G x)))))

equiv-eq-Enriched-Undirected-Graph :
(H : Enriched-Undirected-Graph l3 l4 A B) →
(G ＝ H) → equiv-Enriched-Undirected-Graph A B G H
equiv-eq-Enriched-Undirected-Graph H refl =
id-equiv-Enriched-Undirected-Graph A B G

is-equiv-equiv-eq-Enriched-Undirected-Graph :
(H : Enriched-Undirected-Graph l3 l4 A B) →
is-equiv (equiv-eq-Enriched-Undirected-Graph H)
is-equiv-equiv-eq-Enriched-Undirected-Graph =
fundamental-theorem-id
( is-torsorial-equiv-Enriched-Undirected-Graph)
( equiv-eq-Enriched-Undirected-Graph)

extensionality-Enriched-Undirected-Graph :
(H : Enriched-Undirected-Graph l3 l4 A B) →
(G ＝ H) ≃ equiv-Enriched-Undirected-Graph A B G H
pr1 (extensionality-Enriched-Undirected-Graph H) =
equiv-eq-Enriched-Undirected-Graph H
pr2 (extensionality-Enriched-Undirected-Graph H) =
is-equiv-equiv-eq-Enriched-Undirected-Graph H

eq-equiv-Enriched-Undirected-Graph :
(H : Enriched-Undirected-Graph l3 l4 A B) →
equiv-Enriched-Undirected-Graph A B G H → (G ＝ H)
eq-equiv-Enriched-Undirected-Graph H =
map-inv-equiv (extensionality-Enriched-Undirected-Graph H)