# Reflecting maps of undirected graphs

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

Created on 2023-02-09.

module graph-theory.reflecting-maps-undirected-graphs where

Imports
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.symmetric-identity-types
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.unordered-pairs

open import graph-theory.undirected-graphs


## Idea

A reflecting map from an undirected graph (V , E) into a type X consists of a map fV : V → X and a map

  fE : (v : unordered-pair V) → E v → symmetric-Id (map-unordered-pair fV v).


In other words, it maps edges into the symmetric identity type.

## Definitions

### Reflecting maps of undirected graphs

reflecting-map-Undirected-Graph :
{l1 l2 l3 : Level} (G : Undirected-Graph l1 l2) (X : UU l3) →
UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3)
reflecting-map-Undirected-Graph G X =
Σ ( vertex-Undirected-Graph G → X)
( λ f →
(v : unordered-pair-vertices-Undirected-Graph G) →
edge-Undirected-Graph G v → symmetric-Id (map-unordered-pair f v))

module _
{l1 l2 l3 : Level} (G : Undirected-Graph l1 l2) {X : UU l3}
(f : reflecting-map-Undirected-Graph G X)
where

vertex-reflecting-map-Undirected-Graph : vertex-Undirected-Graph G → X
vertex-reflecting-map-Undirected-Graph = pr1 f

unordered-pair-vertices-reflecting-map-Undirected-Graph :
unordered-pair-vertices-Undirected-Graph G → unordered-pair X
unordered-pair-vertices-reflecting-map-Undirected-Graph =
map-unordered-pair vertex-reflecting-map-Undirected-Graph

edge-reflecting-map-Undirected-Graph :
(v : unordered-pair-vertices-Undirected-Graph G) →
edge-Undirected-Graph G v →
symmetric-Id (unordered-pair-vertices-reflecting-map-Undirected-Graph v)
edge-reflecting-map-Undirected-Graph = pr2 f


### Terminal reflecting maps

terminal-reflecting-map-Undirected-Graph :
{l1 l2 : Level} (G : Undirected-Graph l1 l2) →
reflecting-map-Undirected-Graph G unit
pr1 (terminal-reflecting-map-Undirected-Graph G) x = star
pr1 (pr2 (terminal-reflecting-map-Undirected-Graph G) p e) = star
pr2 (pr2 (terminal-reflecting-map-Undirected-Graph G) p e) x =
eq-is-contr is-contr-unit