Cycles in undirected graphs

Content created by Jonathan Prieto-Cubides, Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2022-06-15.
Last modified on 2024-10-16.

module graph-theory.cycles-undirected-graphs where
Imports 
open import elementary-number-theory.natural-numbers

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

open import graph-theory.embeddings-undirected-graphs
open import graph-theory.polygons
open import graph-theory.undirected-graphs

Idea

A cycle in an undirected graph G consists of a k-gon H equipped with an embedding of graphs from H into G.

Definition

module _
  {l1 l2 : Level} (k : ℕ) (G : Undirected-Graph l1 l2)
  where

  cycle-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2)
  cycle-Undirected-Graph =
    Σ (Polygon k) (λ H → emb-Undirected-Graph (undirected-graph-Polygon k H) G)

Recent changes