Directed graph structures on standard finite sets

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

Created on 2022-07-02.
Last modified on 2024-01-28.

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  )

Recent changes