Reflexive graphs
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-10.
Last modified on 2024-10-16.
module graph-theory.reflexive-graphs where
Imports
open import foundation.dependent-pair-types open import foundation.universe-levels open import graph-theory.directed-graphs
Idea
A reflexive graph¶ is a directed graph equipped with a loop edge at every vertex.
Definition
Reflexive-Graph : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Reflexive-Graph l1 l2 = Σ (UU l1) (λ V → Σ (V → V → UU l2) (λ E → (v : V) → E v v)) module _ {l1 l2 : Level} (G : Reflexive-Graph l1 l2) where vertex-Reflexive-Graph : UU l1 vertex-Reflexive-Graph = pr1 G edge-Reflexive-Graph : vertex-Reflexive-Graph → vertex-Reflexive-Graph → UU l2 edge-Reflexive-Graph = pr1 (pr2 G) refl-Reflexive-Graph : (x : vertex-Reflexive-Graph) → edge-Reflexive-Graph x x refl-Reflexive-Graph = pr2 (pr2 G) graph-Reflexive-Graph : Directed-Graph l1 l2 graph-Reflexive-Graph = vertex-Reflexive-Graph , edge-Reflexive-Graph
See also
External links
- Reflexive graph at Lab
- Graph on Wikidata
- Directed graph at Wikipedia
- Reflexive graph at Wolfram MathWorld
Recent changes
- 2024-10-16. Fredrik Bakke. Some links in elementary number theory (#1199).
- 2024-04-11. Fredrik Bakke. Strict symmetrizations of binary relations (#1025).
- 2024-03-24. Fredrik Bakke. Some notions of graphs (#1091).
- 2023-11-09. Fredrik Bakke. Typeset
nlab
as$n$Lab
(#911). - 2023-10-13. Egbert Rijke. Fix links to wikidata to the recommended links; add concept tags at end of file for testing purposes (#837).