# Voltage graphs

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

Created on 2022-04-04.

module graph-theory.voltage-graphs where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import graph-theory.directed-graphs

open import group-theory.groups


## Idea

A voltage graph is a directed graph G equipped with a group Π, which we call the voltage group, and a labelling of the edges of G by elements of Π.

## Definition

Voltage-Graph :
{l1 : Level} (l2 l3 : Level) (Π : Group l1) → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
Voltage-Graph l2 l3 Π =
Σ ( Directed-Graph l2 l3)
( λ G →
{x y : vertex-Directed-Graph G} →
edge-Directed-Graph G x y → type-Group Π)

module _
{l1 l2 l3 : Level} (Π : Group l1) (G : Voltage-Graph l2 l3 Π)
where

graph-Voltage-Graph : Directed-Graph l2 l3
graph-Voltage-Graph = pr1 G

vertex-Voltage-Graph : UU l2
vertex-Voltage-Graph = vertex-Directed-Graph graph-Voltage-Graph

edge-Voltage-Graph : (x y : vertex-Voltage-Graph) → UU l3
edge-Voltage-Graph = edge-Directed-Graph graph-Voltage-Graph

voltage-Voltage-Graph :
{x y : vertex-Voltage-Graph} → edge-Voltage-Graph x y → type-Group Π
voltage-Voltage-Graph = pr2 G