Undirected graph structures on standard finite sets

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

Created on 2022-07-02.
Last modified on 2023-11-09.

module graph-theory.undirected-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 foundation.unordered-pairs

open import univalent-combinatorics.standard-finite-types

Definition

Undirected-Graph-Fin : UU (lsuc lzero)
Undirected-Graph-Fin = Σ ℕ (λ V → unordered-pair (Fin V) → ℕ)

Recent changes