Edge-coloured undirected graphs

module graph-theory.edge-coloured-undirected-graphs where
Imports
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.universe-levels
open import foundation.unordered-pairs

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

Idea

An edge-coloured undirected graph is an undirected graph equipped with a family of maps E p → X from the edges at unordered pairs p into a type C of colours, such that the induced map incident-Undirected-Graph G x → C is injective for each vertex x.

Definition

module _
  {l1 l2 l3 : Level} (C : UU l1) (G : Undirected-Graph l2 l3)
  where

  neighbor-edge-colouring-Undirected-Graph :
    ( (p : unordered-pair-vertices-Undirected-Graph G) 
      edge-Undirected-Graph G p  C) 
    (x : vertex-Undirected-Graph G)  neighbor-Undirected-Graph G x  C
  neighbor-edge-colouring-Undirected-Graph f x (pair y e) =
    f (standard-unordered-pair x y) e

  edge-colouring-Undirected-Graph : UU (lsuc lzero  l1  l2  l3)
  edge-colouring-Undirected-Graph =
    Σ ( (p : unordered-pair-vertices-Undirected-Graph G) 
        edge-Undirected-Graph G p  C)
      ( λ f 
        (x : vertex-Undirected-Graph G) 
        is-emb (neighbor-edge-colouring-Undirected-Graph f x))

Edge-Coloured-Undirected-Graph :
  {l : Level} (l1 l2 : Level) (C : UU l)  UU (l  lsuc l1  lsuc l2)
Edge-Coloured-Undirected-Graph l1 l2 C =
  Σ ( Undirected-Graph l1 l2)
    ( edge-colouring-Undirected-Graph C)

module _
  {l1 l2 l3 : Level} {C : UU l1} (G : Edge-Coloured-Undirected-Graph l2 l3 C)
  where

  undirected-graph-Edge-Coloured-Undirected-Graph : Undirected-Graph l2 l3
  undirected-graph-Edge-Coloured-Undirected-Graph = pr1 G

  vertex-Edge-Coloured-Undirected-Graph : UU l2
  vertex-Edge-Coloured-Undirected-Graph =
    vertex-Undirected-Graph undirected-graph-Edge-Coloured-Undirected-Graph

  unordered-pair-vertices-Edge-Coloured-Undirected-Graph : UU (lsuc lzero  l2)
  unordered-pair-vertices-Edge-Coloured-Undirected-Graph =
    unordered-pair-vertices-Undirected-Graph
      undirected-graph-Edge-Coloured-Undirected-Graph

  edge-Edge-Coloured-Undirected-Graph :
    unordered-pair-vertices-Edge-Coloured-Undirected-Graph  UU l3
  edge-Edge-Coloured-Undirected-Graph =
    edge-Undirected-Graph undirected-graph-Edge-Coloured-Undirected-Graph

  neighbor-Edge-Coloured-Undirected-Graph :
    vertex-Edge-Coloured-Undirected-Graph  UU (l2  l3)
  neighbor-Edge-Coloured-Undirected-Graph =
    neighbor-Undirected-Graph undirected-graph-Edge-Coloured-Undirected-Graph

  colouring-Edge-Coloured-Undirected-Graph :
    (p : unordered-pair-vertices-Edge-Coloured-Undirected-Graph) 
    edge-Edge-Coloured-Undirected-Graph p  C
  colouring-Edge-Coloured-Undirected-Graph =
    pr1 (pr2 G)

  neighbor-colouring-Edge-Coloured-Undirected-Graph :
    (x : vertex-Edge-Coloured-Undirected-Graph) 
    neighbor-Edge-Coloured-Undirected-Graph x  C
  neighbor-colouring-Edge-Coloured-Undirected-Graph =
    neighbor-edge-colouring-Undirected-Graph C
      undirected-graph-Edge-Coloured-Undirected-Graph
      colouring-Edge-Coloured-Undirected-Graph

  is-emb-colouring-Edge-Coloured-Undirected-Graph :
    (x : vertex-Edge-Coloured-Undirected-Graph) 
    is-emb (neighbor-colouring-Edge-Coloured-Undirected-Graph x)
  is-emb-colouring-Edge-Coloured-Undirected-Graph =
    pr2 (pr2 G)

Properties