Equivalences of reflexive graphs

Content created by Egbert Rijke.

Created on 2024-12-03.
Last modified on 2024-12-03.

module graph-theory.equivalences-reflexive-graphs where

Imports

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels

open import graph-theory.equivalences-directed-graphs
open import graph-theory.morphisms-reflexive-graphs
open import graph-theory.reflexive-graphs

Idea

An equivalence of reflexive graphs^¶ from a reflexive graph (V,E,r) to a reflexive graph (V',E',r') consists of an equivalence (e₀, e₁) of directed graphs from (V,E) to (V',E') equipped with an identification

  e₁ (r x) ＝ r' (e₀ x)

for each x : V. More specifically, an equivalence of reflexive graphs consists of an equivalence e₀ : V ≃ V' of vertices, a family of equivalences e₁ : E x y ≃ E' (e x) (e y) of edges indexed by x y : V, and a family of identifications

  e₁ (r x) ＝ r' (e₀ x)

indexed by x : V.

Definitions

Equivalences of directed graphs between reflexive graphs

module _
  {l1 l2 l3 l4 : Level} (G : Reflexive-Graph l1 l2) (H : Reflexive-Graph l3 l4)
  where

  equiv-directed-graph-Reflexive-Graph : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  equiv-directed-graph-Reflexive-Graph =
    equiv-Directed-Graph
      ( directed-graph-Reflexive-Graph G)
      ( directed-graph-Reflexive-Graph H)

module _
  {l1 l2 l3 l4 : Level} (G : Reflexive-Graph l1 l2) (H : Reflexive-Graph l3 l4)
  (e : equiv-directed-graph-Reflexive-Graph G H)
  where

  vertex-equiv-equiv-directed-graph-Reflexive-Graph :
    vertex-Reflexive-Graph G ≃ vertex-Reflexive-Graph H
  vertex-equiv-equiv-directed-graph-Reflexive-Graph =
    vertex-equiv-equiv-Directed-Graph
      ( directed-graph-Reflexive-Graph G)
      ( directed-graph-Reflexive-Graph H)
      ( e)

  vertex-equiv-directed-graph-Reflexive-Graph :
    vertex-Reflexive-Graph G → vertex-Reflexive-Graph H
  vertex-equiv-directed-graph-Reflexive-Graph =
    vertex-equiv-Directed-Graph
      ( directed-graph-Reflexive-Graph G)
      ( directed-graph-Reflexive-Graph H)
      ( e)

  edge-equiv-equiv-directed-graph-Reflexive-Graph :
    (x x' : vertex-Reflexive-Graph G) →
    edge-Reflexive-Graph G x x' ≃
    edge-Reflexive-Graph H
      ( vertex-equiv-directed-graph-Reflexive-Graph x)
      ( vertex-equiv-directed-graph-Reflexive-Graph x')
  edge-equiv-equiv-directed-graph-Reflexive-Graph =
    edge-equiv-equiv-Directed-Graph
      ( directed-graph-Reflexive-Graph G)
      ( directed-graph-Reflexive-Graph H)
      ( e)

  edge-equiv-directed-graph-Reflexive-Graph :
    {x x' : vertex-Reflexive-Graph G} →
    edge-Reflexive-Graph G x x' →
    edge-Reflexive-Graph H
      ( vertex-equiv-directed-graph-Reflexive-Graph x)
      ( vertex-equiv-directed-graph-Reflexive-Graph x')
  edge-equiv-directed-graph-Reflexive-Graph =
    edge-equiv-Directed-Graph
      ( directed-graph-Reflexive-Graph G)
      ( directed-graph-Reflexive-Graph H)
      ( e)