# Matchings

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

Created on 2022-03-28.

module graph-theory.matchings where

Imports
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
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


## Idea

A matching in a undirected graph is a type of edges without common vertices.

## Definitions

module _
{l1 l2 : Level}
where

selected-edges-vertex-Undirected-Graph :
( G : Undirected-Graph l1 l2) →
( (p : unordered-pair-vertices-Undirected-Graph G) →
edge-Undirected-Graph G p → Fin 2) →
vertex-Undirected-Graph G → UU (l1 ⊔ l2)
selected-edges-vertex-Undirected-Graph G c x =
Σ ( vertex-Undirected-Graph G)
( λ y →
Σ ( edge-Undirected-Graph G (standard-unordered-pair x y))
( λ e → Id (c (standard-unordered-pair x y) e) (inr star)))

matching : Undirected-Graph l1 l2 → UU (lsuc lzero ⊔ l1 ⊔ l2)
matching G =
Σ ( (p : unordered-pair-vertices-Undirected-Graph G) →
edge-Undirected-Graph G p → Fin 2)
( λ c →
( x : vertex-Undirected-Graph G) →
is-prop (selected-edges-vertex-Undirected-Graph G c x))

perfect-matching : Undirected-Graph l1 l2 → UU (lsuc lzero ⊔ l1 ⊔ l2)
perfect-matching G =
Σ ( (p : unordered-pair-vertices-Undirected-Graph G) →
edge-Undirected-Graph G p → Fin 2)
( λ c →
( x : vertex-Undirected-Graph G) →
is-contr (selected-edges-vertex-Undirected-Graph G c x))