# Reflexive graphs

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

Created on 2022-02-10.

module graph-theory.reflexive-graphs where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import graph-theory.directed-graphs


## Idea

A reflexive graph is a directed graph equipped with a loop edge at every vertex.

## Definition

Reflexive-Graph : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Reflexive-Graph l1 l2 =
Σ (UU l1) (λ V → Σ (V → V → UU l2) (λ E → (v : V) → E v v))

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

vertex-Reflexive-Graph : UU l1
vertex-Reflexive-Graph = pr1 G

edge-Reflexive-Graph : vertex-Reflexive-Graph → vertex-Reflexive-Graph → UU l2
edge-Reflexive-Graph = pr1 (pr2 G)

refl-Reflexive-Graph : (x : vertex-Reflexive-Graph) → edge-Reflexive-Graph x x
refl-Reflexive-Graph = pr2 (pr2 G)

graph-Reflexive-Graph : Directed-Graph l1 l2
graph-Reflexive-Graph = vertex-Reflexive-Graph , edge-Reflexive-Graph