# Trails in directed graphs

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

Created on 2023-01-22.

module graph-theory.trails-directed-graphs where

Imports
open import foundation.dependent-pair-types
open import foundation.injective-maps
open import foundation.universe-levels

open import graph-theory.directed-graphs
open import graph-theory.walks-directed-graphs


## Idea

A trail in a directed graph is a walk that goes through each edge at most once.

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

is-trail-walk-Directed-Graph :
{x y : vertex-Directed-Graph G} → walk-Directed-Graph G x y → UU (l1 ⊔ l2)
is-trail-walk-Directed-Graph w =
is-injective (total-edge-edge-on-walk-Directed-Graph G w)

trail-Directed-Graph : (x y : vertex-Directed-Graph G) → UU (l1 ⊔ l2)
trail-Directed-Graph x y =
Σ (walk-Directed-Graph G x y) (is-trail-walk-Directed-Graph)

walk-trail-Directed-Graph :
{x y : vertex-Directed-Graph G} →
trail-Directed-Graph x y → walk-Directed-Graph G x y
walk-trail-Directed-Graph = pr1

is-trail-trail-Directed-Graph :
{x y : vertex-Directed-Graph G} (t : trail-Directed-Graph x y) →
is-trail-walk-Directed-Graph (walk-trail-Directed-Graph t)
is-trail-trail-Directed-Graph = pr2