This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Large reflexive graphs

module graph-theory.large-reflexive-graphs where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

Idea

A large reflexive graph is a large directed graph equipped with a loop edge at every vertex.

Definition

record
  Large-Reflexive-Graph
  (α : Level → Level) (β : Level → Level → Level) : UUω
  where

  field
    vertex-Large-Reflexive-Graph : (l : Level) → UU (α l)

    edge-Large-Reflexive-Graph :
      {l1 l2 : Level} →
      vertex-Large-Reflexive-Graph l1 →
      vertex-Large-Reflexive-Graph l2 → UU (β l1 l2)

    refl-Large-Reflexive-Graph :
      {l : Level} (x : vertex-Large-Reflexive-Graph l) →
      edge-Large-Reflexive-Graph x x

open Large-Reflexive-Graph public

See also