Equivalences of enriched undirected graphs

module graph-theory.equivalences-enriched-undirected-graphs where
Imports
open import foundation.contractible-types
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.functions
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.structure-identity-principle
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 G to 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-contr-total-equiv-Enriched-Undirected-Graph :
    is-contr
      ( Σ ( Enriched-Undirected-Graph l3 l4 A B)
          ( equiv-Enriched-Undirected-Graph A B G))
  is-contr-total-equiv-Enriched-Undirected-Graph =
    is-contr-total-Eq-structure
      ( λ H fn e 
        Σ ( ( shape-vertex-Enriched-Undirected-Graph A B G) ~
            ( ( shape-vertex-Enriched-Undirected-Graph A B (H , fn)) 
              ( vertex-equiv-Undirected-Graph
                ( undirected-graph-Enriched-Undirected-Graph A B G)
                ( undirected-graph-Enriched-Undirected-Graph A B (H , fn)) 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 , fn))
                  ( e)
                  ( x)) ∘e
                ( equiv-neighbor-Enriched-Undirected-Graph A B G x))
              ( ( equiv-neighbor-Enriched-Undirected-Graph A B (H , fn)
                  ( vertex-equiv-Undirected-Graph
                    ( undirected-graph-Enriched-Undirected-Graph A B G)
                    ( undirected-graph-Enriched-Undirected-Graph A B (H , fn))
                    ( e)
                    ( x))) ∘e
                ( equiv-tr B (α x)))))
      ( is-contr-total-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-contr-total-Eq-structure
        ( λ f α K 
          ( 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
                  ( undirected-graph-Enriched-Undirected-Graph A B G , f , α))
                ( id-equiv-Undirected-Graph
                  ( undirected-graph-Enriched-Undirected-Graph A B G))
                ( x)) ∘e
              ( equiv-neighbor-Enriched-Undirected-Graph A B G x))
            ( equiv-neighbor-Enriched-Undirected-Graph A B
              ( undirected-graph-Enriched-Undirected-Graph A B G , f , α)
              ( vertex-equiv-Undirected-Graph
                ( undirected-graph-Enriched-Undirected-Graph A B G)
                ( undirected-graph-Enriched-Undirected-Graph A B
                  ( undirected-graph-Enriched-Undirected-Graph A B G , f , α))
                  ( id-equiv-Undirected-Graph
                    ( undirected-graph-Enriched-Undirected-Graph A B G))
                ( x)) ∘e
              ( equiv-tr B (K x))))
        ( is-contr-total-htpy
          ( shape-vertex-Enriched-Undirected-Graph A B G))
        ( pair
          ( shape-vertex-Enriched-Undirected-Graph A B G)
          ( refl-htpy))
        ( is-contr-total-Eq-Π
          ( λ x 
            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)))
          ( λ x 
            is-contr-total-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-contr-total-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)