Reflexive graphs
Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.
Created on 2022-02-10.
Last modified on 2023-03-14.
module graph-theory.reflexive-graphs where
Idea
A reflexive graph is a graph such that there is an 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)
Recent changes
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 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).