Directed graph structures on standard finite sets

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

Created on 2022-07-02.
Last modified on 2023-03-10.

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 → ℕ)

Recent changes