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

Definition

Directed-Graph-Fin : UU lzero
Directed-Graph-Fin = Σ ℕ (λ V → Fin V → Fin V → ℕ)