Regular undirected graph

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

Created on 2022-03-23.

module graph-theory.regular-undirected-graphs where

Imports
open import foundation.mere-equivalences
open import foundation.propositions
open import foundation.universe-levels

open import graph-theory.neighbors-undirected-graphs
open import graph-theory.undirected-graphs


Idea

A regular undirected graph is an undirected graph of which each vertex has the same number of incident edges.

Definition

is-regular-undirected-graph-Prop :
{l1 l2 l3 : Level} (X : UU l1)
(G : Undirected-Graph l2 l3) → Prop (l1 ⊔ l2 ⊔ l3)
is-regular-undirected-graph-Prop X G =
Π-Prop
( vertex-Undirected-Graph G)
( λ x → mere-equiv-Prop X (neighbor-Undirected-Graph G x))

is-regular-Undirected-Graph :
{l1 l2 l3 : Level} (X : UU l1) (G : Undirected-Graph l2 l3) →
UU (l1 ⊔ l2 ⊔ l3)
is-regular-Undirected-Graph X G =
type-Prop (is-regular-undirected-graph-Prop X G)

is-prop-is-regular-Undirected-Graph :
{l1 l2 l3 : Level} (X : UU l1) (G : Undirected-Graph l2 l3) →
is-prop (is-regular-Undirected-Graph X G)
is-prop-is-regular-Undirected-Graph X G =
is-prop-type-Prop (is-regular-undirected-graph-Prop X G)