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
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).