This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Directed graph structures on standard finite sets

module graph-theory.directed-graph-structures-on-standard-finite-sets where
Imports 
open import elementary-number-theory.natural-numbers

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

open import univalent-combinatorics.standard-finite-types

Idea

A directed graph structure on a standard finite set Fin n is a binary type-valued relation

  Fin n → Fin n → 𝒰.

Definitions

Directed graph structures on standard finite sets

structure-directed-graph-Fin : (l : Level) (n : ℕ) → UU (lsuc l)
structure-directed-graph-Fin l n = Fin n → Fin n → UU l

Directed graphs on standard finite sets

Directed-Graph-Fin : (l : Level) → UU (lsuc l)
Directed-Graph-Fin l = Σ ℕ (structure-directed-graph-Fin l)

Labeled finite directed graphs on standard finite sets

A labeled finite directed graph consists of a natural number n and a map Fin n → Fin n → ℕ.

Labeled-Finite-Directed-Graph : UU lzero
Labeled-Finite-Directed-Graph = Σ ℕ (λ n → Fin n → Fin n → ℕ)