Simple undirected graphs

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

Created on 2022-03-18.
Last modified on 2024-02-06.

module graph-theory.simple-undirected-graphs where
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.negation
open import foundation.propositions
open import foundation.universe-levels
open import foundation.unordered-pairs

open import graph-theory.undirected-graphs

open import univalent-combinatorics.finite-types


An undirected graph is said to be simple if it only contains edges between distinct points, and there is at most one edge between any two vertices.


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

  is-simple-Undirected-Graph-Prop : Prop (lsuc lzero  l1  l2)
  is-simple-Undirected-Graph-Prop =
      ( Π-Prop
        ( unordered-pair-vertices-Undirected-Graph G)
        ( λ p 
            ( edge-Undirected-Graph G p)
            ( is-emb-Prop
              ( element-unordered-pair-vertices-Undirected-Graph G p))))
      ( Π-Prop
        ( unordered-pair-vertices-Undirected-Graph G)
        ( λ p  is-prop-Prop (edge-Undirected-Graph G p)))

  is-simple-Undirected-Graph : UU (lsuc lzero  l1  l2)
  is-simple-Undirected-Graph = type-Prop is-simple-Undirected-Graph-Prop

  is-prop-is-simple-Undirected-Graph : is-prop is-simple-Undirected-Graph
  is-prop-is-simple-Undirected-Graph =
    is-prop-type-Prop is-simple-Undirected-Graph-Prop

Simple-Undirected-Graph : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Simple-Undirected-Graph l1 l2 =
  Σ ( UU l1)
    ( λ V 
      Σ ( unordered-pair V  Prop l2)
        ( λ E 
          (x : V)  ¬ (type-Prop (E (pair (Fin-UU-Fin' 2)  y  x))))))

Recent changes