Stereoisomerism for enriched undirected graphs

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

Imports

open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.homotopies
open import foundation.universe-levels

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

Idea

A stereoisomerism between two (A,B)-enriched undirected graphs is an equivalence between their underlying undirected graphs preserving the shape of the vertices. This concept is derived from the concept of stereoisomerism of chemical compounds.

Note: It could be that we only want the shapes to be merely preserved.

Definition

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

  stereoisomerism-Enriched-Undirected-Graph :
    UU (lsuc lzero ⊔ l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
  stereoisomerism-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))))