Vertex covers

Content created by Jonathan Prieto-Cubides, Fredrik Bakke, Egbert Rijke and Eléonore Mangel.

Created on 2022-03-31.
Last modified on 2023-10-13.

module graph-theory.vertex-covers where
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.unordered-pairs

open import graph-theory.undirected-graphs

open import univalent-combinatorics.standard-finite-types


A vertex cover on a undirect graph is a set of vertices that includes at least one extremity of each edge of the graph.


vertex-cover :
  {l1 l2 : Level}  Undirected-Graph l1 l2  UU (lsuc lzero  l1  l2)
vertex-cover G =
  Σ ( vertex-Undirected-Graph G  Fin 2)
    ( λ c 
      (p : unordered-pair-vertices-Undirected-Graph G) 
      edge-Undirected-Graph G p 
          ( Σ (vertex-Undirected-Graph G)
            ( λ x  is-in-unordered-pair p x × Id (c x) (inr star))))

Recent changes